lambda 演算中 2 个列表的串联

Question

我已经定义了多态列表的类型及其构造函数，现在尝试 编写一个连接 2 个列表的函数，但我的函数 concat 不起作用

Definition listA A :Set :=
    forall T :Set, T -> (A -> T -> T) -> T.
    
Definition pnil (A :Set) : listA A := 
      fun T: Set => fun (x : T ) => fun (c : A -> T -> T) => x.
     
Definition pcons (A :Set): A -> (listA A) -> (listA A):=
    fun (a : A) (q : listA A) => fun T : Set => fun (x : T ) => fun (c : A -> T -> T) => c a (q T x c).
Definition concat (A :Set ) (a b:listA A): listA A :=
    a A b ( pcons A a b). 

我收到函数 concat 的错误

In environment
A : Set
a : listeA A
b : listeA A
The term "b" has type "listeA A" while it is expected to have type "A".

Answer 1

您的函数有两个问题：首先，您使用 a 构建一些 listA A 而不是一些 A，因此它的第一个参数应该是listA A 而不是 A。其次，它的第三个参数也是不正确的：在 cons 情况下，您只是想再次重用 cons，而不是使用 b，所以这第三个参数应该是 pcons A 而不是 pcons A a b。

最后，

Definition concat (A :Set) (a b:listA A): listA A :=
    a (listA A) b (pcons A).

如果您想测试它并说服自己它做了正确的事情，您可能想尝试

Definition tolist (A : Set) (l : listA A) : list A :=
  l (list A) nil cons.

Fixpoint fromlist (A : Set) (l : list A) : listA A :=
  match l with
  | nil => pnil A
  | cons h t => pcons A h (fromlist A t)
  end.

从命令式编码到常用数据类型的转换，然后再转换回来。
例如，您可以执行

Eval compute in tolist nat (concat nat (fromlist nat [0 ; 1]) (fromlist nat [2;3])).

并看到结果确实是[0;1;2;3]。