From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: weis Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA26852 for caml-redistribution; Tue, 22 Sep 1998 11:22:58 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA05498 for ; Tue, 22 Sep 1998 11:22:44 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id LAA12111; Tue, 22 Sep 1998 11:22:39 +0200 (MET DST) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA11296; Tue, 22 Sep 1998 11:22:38 +0200 (MET DST) From: Pierre Weis 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) Cc: caml-list@inria.fr In-Reply-To: <19980922113340M.garrigue@kurims.kyoto-u.ac.jp> from "Jacques GARRIGUE" at Sep 22, 98 11:33:40 am X-Mailer: ELM [version 2.4 PL24 ME8] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: weis > 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 = Or : let (f : 'a -> b) = function x -> x + 1;; val f : int -> int = Or even the most puzzling: let (f : 'a) = function x -> x + 1;; val f : int -> int = 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 : '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/