[Agda] Autophagia

[Nils Anders Danielsson]

On 2014-03-08 01:27, Martin Escardo wrote:
>
> I would like to advertise a concise approach to get type theory to eat
> itself, by Chuangjie Xu and myself, written in Agda, in which type
> theory is formulated without definitional equalities:
>
> http://www.cs.bham.ac.uk/~mhe/TT-perhaps-eating-itself/TT-perhaps-eating-itself.html

I noticed the following comment:

   "The funny order in the patterns in the definition of the
   interpretation of terms comes from Agda's whim (if we reorder them
   according to our taste, the file fails to typecheck)."

Agda reduces earlier clauses /of the same definition/ when checking
later clauses. This means that, when you check the clause with left-hand
side term⟦ T₂ v ⟧ (say), then term⟦ T₁ t ⟧ is treated as being
judgementally equal to term⟦ t ⟧. However, if you move the clause for T₁
down below the clause for T₂, then this no longer applies.

Previously Agda did not reduce earlier clauses. Back then one could
(sometimes?) work around this issue by defining "pointless" identity
functions, similar to your T constructors, mutually with the main
definition.

The following code works:

   F : Bool → Set

   G : (x : Bool) → F x

   F true  = ℕ
   F false = Fin (G true)

   G true  = suc zero
   G false = zero

If we swap the last two clauses of G, then the code is rejected:

   F : Bool → Set

   G : (x : Bool) → F x

   F true  = ℕ
   F false = Fin (G true)

   G false = zero
   G true  = suc zero

However, we can make the code work again by using an identity function:

   F : Bool → Set

   G : (x : Bool) → F x

   F true  = ℕ
   F false = Fin (G true)

   T : Fin (suc zero) → Fin (G true)

   G false = T zero
   G true  = suc zero

   T i = i

-- 
/NAD