Number of element in a list in lambd-calculus?

Question

I am coding polymorphe lists in coq and I have defined the type as

Definition listA A :Set :=
    forall T :Set, T -> (A -> T -> T) -> T.
(* empty list*)
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).

but when I try to count how many element are in a list I get an error:

Unknown constructor: pcons.

this is the code I wrote for counting the elements.

Fixpoint nb_elements (A :Set ) (l :listA A): nat :=
    match l with 
        | pnil => 0
        |pcons A e t => 1 + (nb_elements A t)
    end.

Answer 1

Your definition of listA is the encoding of lists in System F, the polymorphic lambda calculus. To work with these lists, you need to use them as functions rather than resorting to Coq's match statement. For example:

Definition nb_elements (A : Set) (l : listA A) : nat :=
  l nat 0 (fun (x : A) (count : nat) => S count).

Intuitively, the second argument of a listA specifies what to return on the base case, whereas the third argument specifies what to do with a non-empty list. Here, if the list is empty, the number of elements is 0. If the list is non-empty, suppose that we have already computed the number of elements of its tail, which we'll call count. Then, to compute the number of elements of the entire list, we just need to add one to count.

In practice, it is very rare to work with encoded data types such as listA in Coq. Usually, we use inductively defined types, which allow us to work with match statements. Here is a version of your example using an inductive list type:

Inductive list A : Set :=
| nil : list A
| cons : A -> list A -> list A.
Arguments nil {A}.
Arguments cons {A}.

Fixpoint nb_elements (A : Set) (l : list A) : nat :=
  match l with
  | nil => 0
  | cons x l' => S (nb_elements A l')
  end.