Le Type et le Neánt

Is the absence of bananas the same as the absence of anchovis (up to isomorphism)? This and similar hole-istic questions drove me to this:

First, let's define lists and their length (in Coq):

Inductive list' (X:Type): Type :=
  nil : list' X
  cons : X -> list' X -> list' X.

Arguments nil {X}.
Arguments cons {X} _ _.
Notation "x :: y" := (cons x y).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]"  := (cons x .. (cons y []) ..).
Check list'.

Fixpoint length' {X  : Type } (l : list' X) : nat :=
  match l with
   nil  => O
   cons h t  => 1 + (length' t)
  end.

Example test_length'1 : length' ([1;2;3]) = 3.                                                           
Proof. reflexivity. Qed.                                                                                 

It seems obvious that for any Type X the length of an empty list of Type X elements is zero. And indeed this is provable in Coq:

Theorem length_type_invar: forall (X: Type), 
  length (@nil X) = 0.
Proof.
  intros X.
  simpl.
  reflexivity.
Qed.

But without the quantified Type, Coq cannot check the length of an empty list:

Example test_length'1 : length' ([]) = 0.                                                                
Error: Cannot infer the implicit parameter X of nil

Holey Schlamoney!

Two empty lists, one not containing natural numbers, the other not containing booleans, cannot be compared:

Check @nil nat = @nil bool.
Error: The term "[ ]" has type "list bool" \
  while it is expected to have type "list nat".

Coq can infer the Type of an empty list:

Example test_nil_nat: [] = @nil nat.                                                                    
  Proof. reflexivity. Qed.

Example test_nil_bool: [] = @nil bool.                                                                    
  Proof. reflexivity. Qed.

By the reflexivity axiom of equality one would expect that [] = []
But an untyped nothingness cannot be compared to itself:

Example test_nil: [] = [].                                                                    
Error: Cannot infer the implicit parameter X of nil \
  whose type is "Type".

It is no wonder that philosophers concern themselves with the concept of holes.

Wed, 31 Oct 2018
[/projects] permanent link