重新连接自己的Vect但遇到问题

Question

我试图重新实现Vect数据类型以更加熟悉相关类型。这是我写的：

data Vect : (len : Nat) -> (elem : Type) -> Type where
  Nil : Vect Z elem
  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem

append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] y = y
append (x :: xs) y = x :: append xs y

例如，我也可以定义Vect 4 Nat和其他。但是，如果我尝试append (Vect 4 Nat) (Vect 3 Nat)，则会收到无法解析的错误：

When checking an application of function Main.append:
        Type mismatch between
                Type (Type of Vect len elem)
        and
                Vect n elem (Expected type)

很显然，我的想法有问题。

有任何建议吗？

[当我尝试创建Vect 4 [1,2,3,4]时也出现错误：

When checking argument elem to type constructor Main.Vect:
        Can't disambiguate since no name has a suitable type: 
                Prelude.List.::, Main.::, Prelude.Stream.::

所以我想我很迷路...

Answer 1

您正在将类型构造器Vect与数据构造器Nil和::混合在一起。您可以通过调用Vect len elem和Nil创建::类型的值。

特别是Vect 4 Nat是一种类型，但是append需要该类型的值，例如1 :: 2 :: 3 :: 4 :: Nil

并且Vect 4 [1,2,3,4]是不可能的，因为[1,2,3,4]是一个值，而不是Type