**Next message:**Francois Pessaux: "Re: tk scale"**Previous message:**David McClain: "New RealWorld App in OCAML"**In reply to:**Markus Mottl: "Polymorphic recursion in modules - impossible?"**Next in thread:**Jacques GARRIGUE: "Re: Polymorphic recursion in modules - impossible?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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

Message-Id: <199902031540.QAA21649@pauillac.inria.fr>

Subject: Re: Polymorphic recursion in modules - impossible?

To: mottl@miss.wu-wien.ac.at (Markus Mottl)

Date: Wed, 3 Feb 1999 16:40:39 +0100 (MET)

In-Reply-To: <199902012058.VAA20331@miss.wu-wien.ac.at> from "Markus Mottl" at Feb 1, 99 09:58:13 pm

*> Hello,
*

*>
*

*> once again I have come across a problem concerning modules and recursion.
*

*> This time my question is how to get polymorphic recursion in functions
*

*> of modules.
*

*>
*

*> Although I have read the FAQs about this topic and looked into the
*

*> archive of the mailing list, I couldn't find any solution to the problem -
*

*> I fear there is none.
*

I fear too.

*> Code example:
*

*> ---------------------------------------------------------------------------
*

*> module RA_List =
*

*> struct
*

*> type 'a ra_list = Nil
*

*> | Zero of ('a * 'a) ra_list
*

*> | One of 'a * ('a * 'a) ra_list
*

*>
*

*> let rec cons x = function
*

*> Nil -> One (x, Nil)
*

*> | Zero ps -> One (x, ps)
*

*> | One (y,b) -> Zero (cons (x, y) ps)
*

*> end
*

*> ---------------------------------------------------------------------------
*

*>
*

*> It is clear that this piece of code cannot compile because of the
*

*> polymorphic recursion found in the last match of "cons".
*

*>
*

*> The only trick applicable to this problem would be the one with references
*

*> to the function(s) that introduces polymorphic recursion.
*

*>
*

*> The (unsolvable?) problem with this possibility is that one cannot
*

*> initialize the reference(s). This would have to happen after definition
*

*> and before application, but since modules are just a static means of
*

*> abstraction, one cannot do so - as opposed to the trick in the FAQs,
*

*> where there are no modules.
*

In fact the problem here is not related to modules in my mind. It's

just a problem of polymorphic typechecking of recursively defined

identifiers. As you mentioned, the trick(s) describe in the FAQ cannot

resolved the polymorphic recursion problem in its full generality (as

mentioned in this paragraph of the FAQ). It is just a trick to get rid

of basic cases, where recursive calls are not polymorphic uses of the

recursively defined identifier, and unfortunately your example belongs

to this category. In this case, the reference trick is not applicable

since references cannot have polymorphic contents. Anyway, the

reference trick is just a trick, not a nice solution.

*> It would be nice if there were a solution to this, because this would
*

*> allow me the translation of the final two chapters of Okasaki's book to
*

*> OCAML. He uses (even if just as demonstration - SML also doesn't have
*

*> this feature) the technique of polymorphic recursion quite often there.
*

Since I've been working for a long time on the subject, I summarize

here what I did and what I know.

I Related works:

----------------

A) Weak form of polymorphic recursion type inference:

-----------------------------------------------------

As mentioned earlier in this mailing list, we worked hard on this

problem long time ago, thus we had a (weak) form of polymorphic

recursion in Caml as soon as early 1990 (Caml V3.0). Just for fun, I

have cut and past your example in this antique but still working

version of Caml, and got exactly what you expected (having corrected

the ``unbound variable ps'' error of the last clause of your program):

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

#type 'a ra_list = Nil

# | Zero of ('a * 'a) ra_list

# | One of 'a * ('a * 'a) ra_list;;

Type ra_list is defined

#let rec cons x = function

# Nil -> One (x, Nil)

# | Zero ps -> One (x, ps)

# | One (y,b) -> Zero (cons (x, y) b);;

Value cons is <fun> : 'a -> 'a ra_list -> 'a ra_list

B) Type verification:

---------------------

i) Via type constraints:

------------------------

Another attempt to deal with the problem, is to tell in advance the

typechecker what is the expected polymorphic scheme of the identifier

that is recursively defined. This is the trick used in Haskel, and the

trick we could use in Caml if type constraints had the ``mandatory

semantics'' I once proposed here

http://pauillac.inria.fr/caml/caml-list/0703.html.

ii) Via forward definitions:

----------------------------

Along these lines, I added once a ``forward'' definition feature that

in fact implemented the mandatory semantics of type constraints, and

thus allowed ``full'' polymorphic recursion, when the ``weak'' form of

polymorphic recursion was not able to reconstruct the expected type

scheme.

#forward cons : 'a -> 'a ra_list -> 'a ra_list;;

Forward cons : 'a -> 'a ra_list -> 'a ra_list

#let cons x = function

# Nil -> One (x, Nil)

# | Zero ps -> One (x, ps)

# | One (y,b) -> Zero (cons (x, y) b);;

Value cons is <fun> : 'a -> 'a ra_list -> 'a ra_list

However, we could argue that this is not as convenient as type

reconstruction, since the user must find the correct type assignements

by himself, instead of letting the compiler to automatically discover

the most general type of his program.

iii) To circonvent the limits of type reconstruction:

-----------------------------------------------------

On the other hand, we know that the ``full'' polymorphic recursion

discipline is undecidable, hence we definitively need a way to help

the type-checker in some cases, if we do not want it to fail or if we

do not want to add some strange restrictions for polymorphic recursive

definitions. So ``forward'' definitions can serve this purpose.

(More generally, ``forward'' definitions provide a useful assign-once

feature. So, they provide a clean way to accomodate recursion across

modules boundaries (instead of being obliged to define a spurious

reference on a dummy function in one module, and to assign this

reference afterwards with the definition of the function in another

module; moreover forward definitions properly handle the case of

polymorphic functions, as opposed to the reference hack that simply

fails in this case)).

II Work in progress:

--------------------

Recently, the polymorphic recursion problem gets back into the scene

with the work of François Pessaux and Xavier Leroy on static analysis

of uncaught exceptions (see their POPL'99 article for details), since

in this framework polymorphic treatment of recursion allows more

accurate detection of uncaught exceptions. So, François Pessaux and I

are working on the problem, and we already included polymorphic

recursion in the working exceptions analyzer. We are now writing the

detailed theory and proofs for this treatment of polymorphic

recursion.

III Future work:

----------------

If we succeed at proving the desired properties, and publish on the

subject, the new scheme may possibly be incorporated in the O'Caml

type-checker, and it would be the end of your problems. Furthermore, I

would be glad to delete the corresponding embarassed paragraph of the

FAQ!

*> Best regards,
*

*> Markus Mottl
*

*>
*

*> --
*

*> Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl
*

Best regards,

Pierre Weis

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

**Next message:**Francois Pessaux: "Re: tk scale"**Previous message:**David McClain: "New RealWorld App in OCAML"**In reply to:**Markus Mottl: "Polymorphic recursion in modules - impossible?"**Next in thread:**Jacques GARRIGUE: "Re: Polymorphic recursion in modules - impossible?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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