ANN: pa_polyrec: syntax for polymorphic recursion

Jeremy Yallop
 Damien Guichard
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20090929 (14:20) 
From:  Damien Guichard <alphablock@o...> 
Subject:  Re: [Camllist] ANN: pa_polyrec: syntax for polymorphic recursion 
Hi Jeremy, Your syntax extension is nice and simple enough. It will really help in demystifying polymorphic recursion. The provided examples are particularly usefull in understanding where polymorphic recursion matters. My opinion is that polymorphic recursion is largeley overestimated and has little reallife use in a ML context. Basically there are two usage patterns : the Okasaki/Paterson style the J.J.Hallett & A.J.Kfoury style The J.J.Hallett & A.J.Kfoury style is just plain misuse of the rec keyword. That is instead of a wrong rec scope : let rec double : 'a . ('a > 'a) > 'a > 'a = fun f y > f (f y) and foo : 'x . int > int = fun v > double (fun x > x + 1) v and goo : 'y . float > float = fun w > double sqrt w in (foo 3, goo 16.0) One shoud use a correct rec scope : let rec double f y = f (f y) in let foo v = double (fun x > x + 1) v and goo w = double sqrt w in (foo 3, goo 16.0) Especially, OCaml beginner should be warned that polymorphic recursion is not a solution to their typing problems. The Okasaki/Paterson style is more insteresting. Basically it's a poor man's dependant types. Instead of : type 'a perfect = Leaf of 'a  Node of 'a perfect * 'a perfect One does write : type 'a perfect = Zero of 'a  Succ of ('a * 'a) perfect Then the compiler can statically check that the tree is always complete (perfectly balanced). Problems are : functions are harder to type type errors are quite hard to interpret and to locate (although papolyrec certainly helps in this department) benchmarks show you pay a certain (small) price for the added type expressivity In my opinion, when wants the added type expressivity he actually wants dependant types. I mean one should prefer the following Coq code, that is dependant types rather than nested data types : Variable A : Set. Inductive perfect : nat > Set :=  Leaf : perfect O  Node : forall n, A > perfect n > perfect n > perfect (S n). The de Bruijn exemple is representative enough : either you seek after efficiency then nested data type will just hinder interpreter performance either you seek after interpreter validation then dependant types is the way to go May be polymorphic recursion is actually a tool for the working ML programmer. Yet i am still waiting to see the exemple that is more than a nice trick for the ML hacker. Hoping i have made the matter less esoteric to OCaml beginners, Regards,  damien Damien Guichard 20090929 En réponse au message de : Jeremy Yallop du : 20090928 22:56:32 À : camllist@inria.fr CC : Sujet : [Camllist] ANN: pa_polyrec: syntax for polymorphic recursion I'm pleased to announce the initial release of pa_polyrec, a syntax extension for polymorphic recursion in OCaml. https://forge.ocamlcore.org/projects/papolyrec/ There are several methods for encoding polymorphicrecursive functions in OCaml; this extension allows them to be written directly, using a natural syntax. For example, given the following type of perfectlybalanced trees we might wish to write a function for summing the leaves. type 'a perfect = Zero of 'a  Succ of ('a * 'a) perfect In standard OCaml such a function can be written as follows: let sump f = (object (o) method sump : 'a. ('a  > int)  > 'a perfect  > int = fun f  > function  Zero x  > f x  Succ x  > o#sump (fun (a, b)  > f a + f b) x end)#sump f let sum_perfect = sump id Using pa_polyrec one can write the function in the following less obfuscated style: let rec sump : 'a. ('a  > int)  > 'a perfect  > int = fun f  > function  Zero x  > f x  Succ x  > sump (fun (a, b)  > f a + f b) x let sum_perfect = sump id Note that the type variable 'a in the type of the function is quantified: this is what differentiates polymorphicrecursive functions from standard OCaml recursive function definitions. More complex usage is supported, including mutual recursion. A number of examples are included in the distribution, including several modules from Chris Okasaki's thesis "Purely Functional Data Structures" and code from Richard Bird and Ross Paterson's paper "de Bruijn notation as a nested datatype". _______________________________________________ Camllist mailing list. Subscription management: http://yquem.inria.fr/cgibin/mailman/listinfo/camllist Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/camlbugs