functions' recursive construction

[Damien Lefortier]

Hi,

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 ?

--
Damien `Dam' Lefortier
The most important thing in the programming
language is the name      -- D. Knuth

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Jon Harrop]

On Wednesday 23 May 2007 00:17:08 Damien Lefortier wrote:
> But it does not work, any idea ?

What would the type of "f" be?

--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
The F#.NET Journal
http://www.ffconsultancy.com/products/fsharp_journal/?e

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Lukasz Stafiniak]

On 5/23/07, Jon Harrop <jon@...> wrote:
> On Wednesday 23 May 2007 00:17:08 Damien Lefortier wrote:
> > But it does not work, any idea ?
>
> What would the type of "f" be?
>
In OCaml,

 'a -> 'a as 'a

;-)

Would this function (or some approximation) be possible in Coq?

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Lukasz Stafiniak]

On 5/23/07, Lukasz Stafiniak <lukstafi@...> wrote:
> On 5/23/07, Jon Harrop <jon@...> wrote:
> > What would the type of "f" be?
> >
>  'a -> 'a as 'a
>
I'm sorry, I meant:
#     val f : int -> ('a -> 'a as 'a) = <fun>

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Jon Harrop]

On Wednesday 23 May 2007 00:32:58 you wrote:
> On 5/23/07, Lukasz Stafiniak <lukstafi@...> wrote:
> > On 5/23/07, Jon Harrop <jon@...> wrote:
> > > What would the type of "f" be?
> >
> >  'a -> 'a as 'a
>
> I'm sorry, I meant:
> #     val f : int -> ('a -> 'a as 'a) = <fun>

Not this then:

# let rec f n x = if n=0 then x else f (n-1) (x x);;
val f : int -> ('a -> 'a as 'a) -> 'a = <fun>

--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
The F#.NET Journal
http://www.ffconsultancy.com/products/fsharp_journal/?e

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Jean-Christophe Filliatre]

Damien Lefortier 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 ;;

Lukasz Stafiniak wrote:
 > Would this function (or some approximation) be possible in Coq?

Yes, and here it is (0-based instead of 1-based as above):

======================================================================
Fixpoint t (n:nat) : Type := match n with
  | O => forall (A:Set), A -> A
  | S p => forall (A:Set), A -> t p
end.

Fixpoint f  (n:nat) : t n :=
  match n return t n with
  | O => (fun (A:Set) (x:A) => x)
  | S p => (fun (A:Set) (x:A) => f p)
end.

Eval compute in f 2.
= fun (A : Set) (_ : A) (A0 : Set) (_ : A0) (A1 : Set) (x1 : A1) => x1
     : t 2
======================================================================


--
Jean-Christophe

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Fabrice Marchant]

On Wed, 23 May 2007 01:17:08 +0200
"Damien Lefortier" <damien.lefortier@...> wrote:

> Hi,
>
> 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 ?

  Hi List,

  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 ?

Thanks,

Fabrice

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Fabrice Marchant]

On Mon, 7 Jul 2008 15:04:17 -0500
"William Neumann" <wneumann@...> wrote:

> For a quick hint as to why you cannot write such a function, ask
> yourself what the type of f would be.
>
> Consider just the two cases of the type of (f 1) and (f 2).

Thanks for your swift answer,

So it's 'No', as I guessed, because the types of your two cases are different.

After Coq, maybe could we program this in Lisp ?

Regards,

Fabrice

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Fabrice Marchant]

On Mon, 7 Jul 2008 22:18:45 +0200
Christian Lindig <lindig@...> wrote:

>
> On Jul 7, 2008, at 8:01 PM, Fabrice Marchant wrote:
> > (I think the answer is 'No') Could you shed light on this ?
>
> Farbrice,
>
> I think you are right I but can't give a formal argument, only some  
> intuition: you can't provide a static type for the function you want.  
> The type of the function would depend on the integer value you only  
> know at runtime. Such value-dependent types are not supported by  
> OCaml's type system.

  Thanks a lot Christian for these clear explanations. So they confirm William's answer.

Regards,

Fabrice

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Fabrice Marchant]

Jeremy Yallop <jeremy.yallop@...> 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

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Jeremy Yallop-2]

Fabrice Marchant wrote:

> On Wed, 23 May 2007 01:17:08 +0200 "Damien Lefortier"
> <damien.lefortier@...> 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.

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Jeremy Yallop-2]

Fabrice Marchant wrote:
> After Coq, maybe could we program this in Lisp ?

Yes, although this is rather off-topic.  Here are two solutions in
(rather rusty) Scheme, both zero-based again.  A curried version:

   (define (f n)
     (cond
      ((zero? n) (lambda (x) x))
      (#t        (lambda (_) (f (- n 1))))))

Now

   > ((f 0) 1)
   1
   > (((((f 3) 1) 2) 3) 4)
   4

An uncurried version:

   (define (f n)
     (lambda args (list-ref args n)))

Now

   > ((f 0) 1)
   1
   > ((f 3) 1 2 3 4)
   4

Jeremy.

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Dominique Martinet]

Hello,

I am not sure I remember what was said exactly, and I'm quite too lazy
to check, but I remember that someone gave a possible implementation
with Obj.magic ?
This also is about the same as the Printf functions which can take a
variable amount of arguments and need a bit of tinkering, and I
remember a function 'eat", taking an integer n, which would ignore the
n first arguments given to the function. Now, if you have this,
getting the first argument should be possible after looking at the
printf source :) (although I could not find it searching in my mails,
sorry)

Actually, I've just glanced at the source and there _is_ a "get_arg"
function, taking a single integer and returning an Obj.magic'ed item
which would most likely be the nth argument of a function - however I
can't separate the function from the rest of the code properly in just
a minute, but it definitly is a place to look at if you need such a
function... Although it might be quite dangerous. But as it was said,
the type is impossible to represent and magic is probably necessary
without typing multiple calls to functions manually; but Jeremy's
solution could be enough :)

Good luck,
Dominique Martinet

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Bünzli Daniel]

Le 7 juil. 08 à 21:11, Fabrice Marchant a écrit :

>  That is really nice ! I discover this original way of thinking.

A good reference for these kind of tricks can be found here :

http://mlton.org/Fold

Best,

Daniel

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs