[Agda] Defining large numbers without recursion, with short programs

[Martin Escardo]

On 11/03/15 00:49, effectfully wrote:
> you can avoid these giant implicit arguments by
> wrapping the N into a record

I will keep this technique in mind for possible future use!

M.


> (my emacs doesn't want to display 𝟘 𝟙
> 𝟚 𝟛 properly):
>
> {-# OPTIONS --no-pattern-matching #-}
>
> U = Set
>
> data ℕ : U where
>   zero : ℕ
>   succ : ℕ → ℕ
>
> record N X : U where
>    constructor #
>    field el : (X → X) → (X → X)
> open N
>
> b0 b1 b2 b3 : {X : U} → N X
> b0 = # λ s z → z
> b1 = # λ s z → s z
> b2 = # λ s z → s(s z)
> b3 = # λ s z → s(s(s z))
>
> suc : {X : U} → N X → N X
> suc n = # λ s z → s (el n s z)
>
> add : {X : U} → N X → N X → N X
> add m n = # λ s z → el m s (el n s z)
>
> N-rec : {X : U} → (X → X) → X → (N X → X)
> N-rec s z m = el m s z
>
>
> mul : {X : U} → N X → N(N X) → N X
> mul m = N-rec (add m) b0
>
> exp : {X : U} → N(N X) → N(N X) → N X
> exp n = N-rec (λ m → mul m n) b1
>
> decode : N ℕ → ℕ
> decode = N-rec succ zero
>
> large : ℕ
> large = decode
>   (exp b2
>   (exp b2
>   (exp b2
>   (exp b2
>   (exp b2
>   (exp b2
>   (exp b2
>   (exp b2
>   (exp {?} b2
>        b2)))))))))
>
> Then Agda infers
>
>      N (N (N (N (N (N (N (N ℕ)))))))
>
> in the hole above.
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe