[mercury-users] literature polymorphic recursive calls
brogoff
brogoff at speakeasy.net
Thu Jun 23 03:01:53 AEST 2005
On Wed, 22 Jun 2005, Ralph Becket wrote:
> Tom Schrijvers, Wednesday, 22 June 2005:
> >
> > I guess Mercury takes a third
> > approach: it does multiple iterations to handle some non-problematic
> > recursive definitions. What happens if the limit is reached? I should try
> > it :)
>
> Well, even HM checkers can take an exponential amount of time in the
> worst case!
In case there's someone who hasn't seen it, here's a nasty example, in
OCaml syntax, where the size of the type scheme blows up.
let f0 x y z = z x y;;
let f1 x = f0 x x;;
let f2 x = f1 (f1 x);;
let f3 x = f2 (f2 x);;
let f4 x = f3 (f3 x);;
etc..., but by f4 the size of the type is HUGE
I've never seen anything like this in "real life" ML either.
> In practice this problem just doesn't arise (at least, not
> in my experience).
I'm glad to hear that the iterative approach taken in Mercury to do inference
for polymorphic recursion works out in practice, but it still seems that
requiring explicit types for these cases, as in Haskell, is a good solution. Is
there a rationale for why the Mercury developers chose to do it the way they
did?
As long as we're on the subject, allow me to digress slightly. One of the
issues some people bring up with allowing non-uniform data types and
polymorphically recursive functions on them, is that it would preclude certain
optimizations, in particular, the monomorphization approach taken by certain
whole program optimizing compilers (Stalin for Scheme and MLton for SML).
However, Okasaki states in his "Purely Functional Data Structures" book that
it is always possible to transform such non-uniform types into uniform ones by
introducing new type definitions. If that's true, shouldn't a sufficiently
smart whole program optimizing compiler be able to perform this source to
source transformation and then monomorphize the result?
I realize that the Mercury developers are probably not working on a whole
program compiler (yet! :) but given that one of the goals of Mercury is
fast executables and the language does support non-uniform datatypes, I
figured this is as good a place as any to ask. Since I haven't seen any
papers on this, it might be an interesting research topic. I got the idea
from MLton developer Stephen Weeks, who suggested it during an email
discsussion.
-- Brian
--------------------------------------------------------------------------
mercury-users mailing list
post: mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the users
mailing list