The Shœstring Foundation Weblog

The Shœstring Foundation Weblog, Miscellaneous Byproducts

Matthias Bauer
bauerm (at) shoestringfoundation · org
reop pubkey
Vignettes by George Herriman and a small program

Subscribe to a syndicated feed of my weblog, brought to you by the wonders of RSS.

Blosxom Logo

Wed, 31 Oct 2018

Le Type et le Néant

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)

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.
  intros X.

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.
So by the transitivity 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.

[/projects] permanent link