Re: Polymorphic recursion in modules  impossible?
 Pierre Weis
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Pierre Weis <Pierre.Weis@i...> 
Subject:  Re: Polymorphic recursion in modules  impossible? 
> 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/camllist/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 typechecker 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 assignonce 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 typechecker, 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.wuwien.ac.at, http://miss.wuwien.ac.at/~mottl Best regards, Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/