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:

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

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:

So by the transitivity axiom of equality one would expect that`Example test_nil_nat: [] = @nil nat. Proof. reflexivity. Qed. Example test_nil_bool: [] = @nil bool. Proof. reflexivity. Qed.`

`[] = []`

But an untyped nothingness cannot be compared to itself:

It is no wonder that philosophers concern themselves with the concept of holes.`Example test_nil: [] = []. Error: Cannot infer the implicit parameter X of nil \ whose type is "Type".`

*Wed, 31 Oct 2018 [/projects]
permanent link*