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

[Aaron Stump]

Hello, Martin.

It is very interesting to see this example in Agda, and I enjoyed 
reading your explanation.

You mentioned you are not sure if iteration of N is a new technique.  I 
believe you can find this (presented quite a bit more densely!) in some 
papers by Daniel Leivant, exploring the computational power of 
predicative polymorphism.  See his CMU tech report "Finitely stratified 
polymorphism" (there is also a LICS '89 paper on the topic):

http://repository.cmu.edu/compsci/1962/

Cheers,
Aaron

On 03/10/2015 07:49 PM, effectfully wrote:
> Neat trick. BTW, you can avoid these giant implicit arguments by
> wrapping the N into a record (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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda