[MLton] Re: [MLton-devel] MLton HOL

[Joe Hurd]

On Sun, 19 Oct 2003, Stephen Weeks wrote:

> Yes, this is a bug.  We changed how equality is handled, and only
> propagated the change to the 2002 basis.  I've checked in a fix to our
> CVS.  If you want to get it, you can use the 20031018 binary package
> to process the latest CVS basis library sources and rebuild
> world.mlton by using the following command
>
> /usr/lib/mlton/mlton-compile <path>/<to>/basis-library/ /usr/lib/mlton/world

I've done this, and have (almost) managed to compile the metis prover.
There were several changes to do with LargeWords going from 32 to 64
bits. Also, the following example now fails:

longbottom:~$ mlton
MLton 20031018 (built Sun Oct 19 21:07:11 2003 on longbottom.lotr)
longbottom:~$ cat t.sml
signature Foo = sig val f : ('a -> 'a) -> 'a -> 'a end
structure Foo :> Foo = struct fun f g x = g x end
fun g x = []
val z = Foo.f g ([] : int list)
longbottom:~$ mlton t.sml
Error: t.sml 4.1: unable to infer type for z
   type: ??? list
   in: val z = Foo.f g ([]: int list)
compilation aborted: elaborate reported errors

It used to work:

longbottom:~$ /usr/bin/mlton
MLton 20030716 (built Wed Jul 16 10:23:10 2003 on redhat71)
longbottom:~$ /usr/bin/mlton t.sml
longbottom:~$

The example is a very cut-down version of a real program implementing
parser combinators. Here mlton should be able to deduce the type of
the final result z, but seems to be ignoring the signature of Foo.

Joe



_______________________________________________
MLton mailing list
MLton@mlton.org
http://www.mlton.org/mailman/listinfo/mlton