14 views

Skip to first unread message

Sep 28, 2009, 4:56:39 PM9/28/09

to caml...@inria.fr

I'm pleased to announce the initial release of pa_polyrec, a syntax extension

for polymorphic recursion in OCaml.

for polymorphic recursion in OCaml.

https://forge.ocamlcore.org/projects/pa-polyrec/

There are several methods for encoding polymorphic-recursive functions in OCaml;

this extension allows them to be written directly, using a natural syntax. For

example, given the following type of perfectly-balanced 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 polymorphic-recursive 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".

_______________________________________________

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

Sep 29, 2009, 10:20:30 AM9/29/09

to caml...@inria.fr

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 real-life 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 pa-polyrec 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

2009-09-29

En r�ponse au message

de : Jeremy Yallop

du : 2009-09-28 22:56:32

� : caml...@inria.fr

CC :

Sujet : [Caml-list] ANN: pa_polyrec: syntax for polymorphic recursion

Sep 29, 2009, 6:41:55 PM9/29/09

to Damien Guichard, caml...@inria.fr

Thanks for the comments, Damien.

Damien Guichard wrote:

> Problems are :

> 1. functions are harder to type

> 2. type errors are quite hard to interpret and to locate

> (although *pa-polyrec* certainly helps in this department)

> 3. benchmarks show you pay a certain (small) price for the added type

> expressivity

I think that the arguments you make against polymorphic recursion could also be

made against other features of OCaml, such as structurally-typed objects and

polymorphic variants: they make type errors more complex and can be less

efficient than the alternatives. Still, I'm glad that OCaml has those features

because they make it possible to write programs that would otherwise be impossible.

I'm glad you raised these points, though, because they highlight the fact that

there is a tradeoff involved. If you use nested data types and polymorphic

recursion then you may have to work harder to satisfy the compiler. However, in

return the compiler will guarantee the absence of certain errors that would

otherwise remain undetected until runtime, and perhaps forever.

> 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.

Here is one example: the following paper shows how to use OCaml extended with

GADTs to give a precise type to the output of a parser generator:

Towards efficient, typed LR parsers

Fran�ois Pottier and Yann R�gis-Gianas

ACM Workshop on ML, 2006

http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gianas-typed-lr.pdf

The run and gotoE procedures, which form a central part of the implementation

described in that paper, are inherently polymorphic-recursive, just like most

other non-trivial functions over GADTs. OCaml doesn't have GADTs, of course,

but Oleg recently described a technique that can be used to translate many

programs that use GADTs into OCaml:

http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html

Polymorphic recursion is an important element of that technique.

> In my opinion, when wants the added type expressivity he actually wants

> dependant types.

That may be true, but since OCaml doesn't support dependent types I think that

it's useful to know what can be accomplished without them.

There is an ancillary benefit to pa_polyrec (besides polymorphic recursion): it

provides a clear way of ensuring that a function is polymorphic, giving a

solution to the problem described in this blog post by Stephen Weeks:

http://ocaml.janestreet.com/?q=node/29

For example, suppose that you have a function

let f = fun x -> 13 :: x

and you want to tell the compiler that it has type 'a list -> 'a list, for any

type 'a. (Since it actually does *not* have that type, we want the compiler to

complain.) This is surprisingly difficult to write straightforwardly in OCaml!

You can't write the following

let f : 'a list -> 'a list = fun x -> 13 :: x

since OCaml will simply unify the variable 'a with the element type of the list,

and type-checking will succeed.

That blog post shows how to use an uninhabited type to guarantee polymorphism:

you can write something like the following

type a

let f = fun x -> 13 :: x

let (_ : a list -> a list) = f

and the compiler will duly complain that 'a' and 'int' cannot be unified. This

is certainly a useful trick; still, it would be nice to be able to ascribe the

polymorphic signature directly. Using pa_polyrec one can write

let rec f : 'a. 'a list -> 'a list = fun x -> 13 :: x

and the compiler will complain that the type of the right hand side is

insufficiently general. (Of course, it would be better to be able to omit the

'rec'; perhaps a future release will permit that.)

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu