I have defined the type of a polymorphic list and its constructors, and now trying to write a fonction that concatenate 2 lists but my function concat does not work
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).
error I get for the function 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".
There are two issues with your function: first, you use a to build some listA A and not some A, so its first argument should be listA A and not A. Second, its third argument is also incorrect: in the cons case, you simply want to reuse cons again, rather than using b, so this third argument should be pcons A instead of pcons A a b.
In the end, you get
Definition concat (A :Set) (a b:listA A): listA A :=
a (listA A) b (pcons A).
If you want to test it and convince yourself it does the right thing, you might want to play with
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.
that convert from your impredicative encoding to the usual datatype and back. For instance, you can do
Eval compute in tolist nat (concat nat (fromlist nat [0 ; 1]) (fromlist nat [2;3])).
and see that the result is indeed [0;1;2;3].