[MLton-devel] monomorphisation and the opus

[Matthew Fluet]

> The main question is whether
> we should provide something a bit more formal that proves
> its correctness and/or the suitability of this approach even in
> the presence of polymorphic recursion by transforming type
> information into runtime value information.   What is your opinion?

I'm not sure I understand what you are getting at.  My understanding was
that the monomorphiser only worked in the presence of non-linear (I've
also seen them termed non-regular) datatypes because of the absence of
polymorphic recursion.  That is, the proof of correctness of the
monomorphiser relies critically on the absence of polymorphic recursion.

It then becomes an orthogonal issue as to whether or not every program
with non-regular datatypes and polymorphic recursion can be rewritten to
an equivalent program with regular datatypes and no polymorphic recursion,
presumably at the expense of some runtime data.  (What the latter "gives"
you is that the utility of monomorphisation as a compilation strategy can
be "stretched"  further than might be immediately apparent.)

Certainly for MLton and the opus, the proof of correctness of the
monomorphiser (ie., monomorphisation of Standard ML programs) would seem
to be important.  (But, then again, I'm not totally up to speed on how the
monomorphiser works, so I'm not sure how clean and simple a proof of that
could be.)

As for whether or not there is a translation from poly-rec to
non-poly-rec, I think that is an interesting problem in it's own right
(ie., potentially worth a paper of its own).  Chris Okasaki (in _Purely
Functional Datastructures_) claims: "It is always possible to convert a
non-uniform type into a uniform type by introducing a new datatype to
collapse the different instances into a single type."  However, I've never
seen a general description of how this is to be done, nor how to rewrite
functions over the non-uniform datatype.

(Note, this issue came up on the MLton list around Nov. 10 2000 in a
discussion with the developers of the Haskell debugger Buddha; at that
time they couldn't support polymorphic recursion; I'm not sure about now.)

Some time ago I had been playing with that problem (mostly, because I
wanted to know exactly how to implement Okasaki's datastructures in SML),
and I worked through a number of examples and couldn't put together a
general scheme, but I'm sure its out there.




-------------------------------------------------------
Enterprise Linux Forum Conference & Expo, June 4-6, 2003, Santa Clara
The only event dedicated to issues related to Linux enterprise solutions
www.enterpriselinuxforum.com

_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel