Re: polymorphic recursion

From: Pierre Weis (Pierre.Weis@inria.fr)
Date: Tue Sep 22 1998 - 11:22:38 MET DST


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/



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