[Agda] Erasable vs. irrelevant

[jleivent at comcast.net]

Hi Adam,

The weakening of the normal discrimination to "weak-disc" is exactly what I did that I think makes this erasable.  In other words - yes of course, with the normal discrimination axiom "disc : {n : N} → 1+ n ≡ Ø → ⊥", the resulting type (the standard naturals) has computational content, and is not erasable.  My point was that by doing just that one weakening, you end up with something that is very structurally similar to naturals, and very useful, but is erasable.  I made that "weak-disc" axiom as strong as I could think of doing yet still leave the resulting type erasable.  Mostly, this just amazes me - I don't know if it is at all useful as a way to complement compilation techniques that remove erasable code.  It's as if the theory of the naturals, on which so much is built, is "barely there" - meaning there isn't very much at all (just the difference between the normal discrimination axiom and the weakened one) keeping it from disappearing into nothingness.

----- Original Message -----
From: Adam Gundry <adam.gundry at strath.ac.uk>
To: jleivent at comcast.net
Cc: agda at lists.chalmers.se
Sent: Thu, 19 Jan 2012 20:43:27 -0000 (UTC)
Subject: Re: [Agda] Erasable vs. irrelevant

Hi Jonathan,
On 19/01/12 19:21, jleivent at comcast.net wrote:
> See the enclosed module.  So, even with induction and cases, it still
> looks to me like it is erasable - or, as you say, that there is no
> computational content in N.  It is surprising to me that so much
> about the naturals could be devoid of computational content.  I have
> a hard time believing that this is correct - but I don't see anything
> wrong with it.

The only thing wrong with it is that you haven't axiomatised the natural
numbers. You have this:

> record N-Erasable : Set₁ where
>   field
>     N         : Set
>     Ø         : N
>     1+        : N → N
>     1+inject  : ∀{n₁ n₂ : N} → 1+ n₁ ≡ 1+ n₂ → n₁ ≡ n₂
>     Ø1+choice : ∀(n : N) → n ≡ Ø ⊎ ∃ λ n' → n ≡ 1+ n'
>     induction : ∀(P : N → Set) → P Ø → (∀{n : N} → P n → P (1+ n)) → ∀(n' : N) → P n'
>     weak-disc : ∀{n : N} → 1+ n ≡ Ø → ∀(n₁ n₂ : N) → n₁ ≡ n₂

which is modelled by the unit type, as you demonstrate. But you are
missing an axiom to say that one is not equal to zero:

disc : {n : N} → 1+ n ≡ Ø → ⊥

With this axiom (even though it has no "computational content" in some
sense), the unit type is no longer a model. Your weak-disc is too weak,
precisely because it is satisfied by the unit type as well as the naturals.

Hope this helps,

Adam