Fabrice Marchant wrote:
> On Wed, 23 May 2007 01:17:08 +0200 "Damien Lefortier"
> <damien.lefortier@gmail.com> wrote:
> 
>> I try to do a function f which takes one integer argument and
>> returns a function g which returns its nth arguments.
>> 
>> For example f 3 gives g with let g = fun x -> fun y -> fun z -> z
>> ;;
>> 
>> I tried to do that kind of f function.
>> 
>> let rec f = function 1 -> fun x -> x | n -> fun _ -> f (n-1) ;;
>> 
>> But it does not work, any idea ?
> 
> Sometimes, trying to learn a bit more about OCaml, I dig into old
> List topics. But here, outside Coq answer, I'm not sure to understand
> the explanations about the original OCaml question. Please, is it
> possible to write an OCaml function that would behave the way Damien
> Lefortier wish ? (I think the answer is 'No') Could you shed light on
> this ?

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.

Jeremy.