Jeremy Yallop <jeremy.yallop@ed.ac.uk> wrote:

> Here's a rather simple way to do it by encoding all the mechanics in the
> integer argument rather than in "f".  Like Jean-Christophe Filliatre in 
> the original thread, I'll use a zero-based rather than a one-based encoding.
> 
>     let z v = v
>     let s n _ = n
>     let f n = n
> 
> Now
> 
>      f z 0
>   => 0
> 
> and
> 
>      f (s (s (s z))) 0 1 2 3
>   => 3
> 
> and so on.

  Thanks Jeremy,

That is really nice ! I discover this original way of thinking.
's' nesting level remains however frozen at runtime.

A cool thing is that parameters types can be freely mixed :
f (s (s z)) '0' "1" (fun x -> 2*x) 3

=> 6

Regards,

Fabrice