**Next message:**Basile STARYNKEVITCH: "micro wish: ocamlfat"**Previous message:**Jacques GARRIGUE: "Re: polymorphic recursion"**In reply to:**Jacques GARRIGUE: "Re: polymorphic recursion"**Next in thread:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Mark Andrew: "OCaml 2.0 Binary for the Mac ?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

From: Pierre Weis <Pierre.Weis@inria.fr>

Message-Id: <199809220922.LAA11296@pauillac.inria.fr>

Subject: Re: polymorphic recursion

To: garrigue@kurims.kyoto-u.ac.jp (Jacques GARRIGUE)

Date: Tue, 22 Sep 1998 11:22:38 +0200 (MET DST)

In-Reply-To: <19980922113340M.garrigue@kurims.kyoto-u.ac.jp> from "Jacques GARRIGUE" at Sep 22, 98 11:33:40 am

*> To my knowledge, there is no direct way to do this. Part of the reason
*

*> is that type signatures have a different role in Haskell and ML: in
*

[...]

*> This does not matter very much in ML, since you explicitely decide
*

*> which functions recurse with which (in Haskell all definitions in a
*

*> module are a priori recursive), and there are only few examples really
*

*> needing polymorphic recursion.
*

Yes, and for the excellent reason that you cannot use polymorphic

recursion in ML: this way it would be very surprising to find good

examples of its use, since nobody can write programs based on

polymorphic recursion!

*> To be complete on this point, in Objective Label method calls can be
*

*> polymorphically recursive:
*

*>
*

*> # class r = object (self)
*

*> method virtual m : 'a. 'a -> 'a
*

*> method m x =
*

*> let q = self#m true in
*

*> let r = self#m 0 in
*

*> x
*

*> end;;
*

*> class r : object method m : 'a. 'a -> 'a end
*

*>
*

*> Thanks to the mechanisms use for this inference, it would be easy to
*

*> provide polymorphic recursion for functions also, but we go back to
*

*> the ML problem: where do we write the signature ?
*

Sintactically, it is easy: just the regular type constraint mechanism, writing:

let rec (f : 'a -> 'a) x =

let q = f true in

let r = f 0 in

x;;

Unfortunately, the problem here is the semantics of type constraints

in ML: type constraints are not mandatory type assigment declarations,

but just annotations which should be compatible with the type infered

for the given expression. This means that a type constraint has to be

more general than the principal type of the annotated expression. For

instance, you can write:

let (f : 'a -> int) = function x -> x + 1;;

val f : int -> int = <fun>

Or :

let (f : 'a -> b) = function x -> x + 1;;

val f : int -> int = <fun>

Or even the most puzzling:

let (f : 'a) = function x -> x + 1;;

val f : int -> int = <fun>

This has many drawbacks, the most important being that no type

annotation in a program is reliable to the reader (except if the type

annotation does not posses any type variable at all).

If type constraints were mandatory, then the annotations will easily

give room to polymorphic recursion (the typechecker just acknowledges

the type annotation as the infered type and verifies the remaining

constraints). In my mind mandatory type annotations will be clearer

and more useful than the strange and almost useless semantics we have

now.

Polymorphic recursion via type annotations, while pratical and simple,

is not completely satisfactory: type inference of polymorphic

recursion would be much more in the spirit of ML. Unfortunately, this

problem, well-known as the ``mu-rule'' problem, has been proved

undecidable in general. However, a restricted kind of polymorphic

recursion inference is tractable (via semi-unification for

instance). Once upon a time, there were an old and wise Caml compiler

featuring such a restricted mechanism:

CAML (sun4) (V3.1) by INRIA Fri Oct 1

#let rec f x =

# let q = f true in

# let r = f 0 in

# x;;

Value f is <fun> : 'a -> 'a

We still like this feature and we are still looking for a

tractable generalisation of this restricted polymorphic recursion

inference to add it to our new and strong compilers. Wait and see!

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

**Next message:**Basile STARYNKEVITCH: "micro wish: ocamlfat"**Previous message:**Jacques GARRIGUE: "Re: polymorphic recursion"**In reply to:**Jacques GARRIGUE: "Re: polymorphic recursion"**Next in thread:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Simon Helsen: "Re: polymorphic recursion"**Reply:**Mark Andrew: "OCaml 2.0 Binary for the Mac ?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b29
: Sun Jan 02 2000 - 11:58:16 MET
*