RE: [Sml-implementers] Free type variables on toplevel

[Robert H. <Rob...@cs...>]

This sounds like a nice solution.  I'm glad that my speculations on why it
might be hard were wrong.  Do other compilers do "top down" signature
ascription in this manner?

Bob

-----Original Message-----
From: David Matthews [mailto:Dav...@pr...]
Sent: Thursday, September 27, 2001 9:21 AM
To: 'Matthias Blume'
Cc: sml...@li...
Subject: RE: [Sml-implementers] Free type variables on toplevel


On Wednesday, September 26, 2001 7:41 PM, Matthias Blume
[SMTP:bl...@re...] wrote:
> As for the simultaneous type-checking-and-constraint-applying
approach:  Why
> can
> one not work with unbound type variables (just like when type-checking
a
> "let")?
> As I understand, that's what OCaml does.  Of course, I do not agree
with
> OCaml's
> solution of simply leaving unbound type variables in the final type; I
have
> explained
> why.  (It would not be a good idea in the context of separate
compilation.)
> What I am suggesting here is to leave the variable _tentatively_
unbound.
> At the end of the day, when the whole topdec including all its
signature
> constraints
> etc. has been considered and there are _still_ free type variables in
the
> result,
> then we reject the program.  But not before that.
> 
> Matthias

When I implemented this in Poly/ML I thought along similar lines and
this is a fairly accurate description of the current implementation.
The note to rules 87-89 says that no free type variables enter the basis
and this is enforced in the compiler by a final walk over all the
structures, functors and values.  Until then the variables are unbound.
Variables that don't appear in the result signature, such as those that
have been shadowed, are simply ignored.

> structure S:
sig
	val x: int list
end
=
struct
	val x = ref nil
	val x = nil @ nil
end;
# # # # # # # # structure S : sig val x : int list end

The original implementation in Poly/ML produced an error message and
failed if a free type-variable was found.  I changed that in a later
release to a warning and the type variables are unified with new unique
types.  The reason was much as Bob described.  To avoid confusion with
existing types or with type variables the types print with the (illegal)
identifiers _a, _b etc.

Without the signature:

structure S =
struct
	val x = ref nil
	val x = nil @ nil
end;
# # # # Warning:
The type of (S.x) contains a free type variable.
Setting it to a unique monotype.

structure S : sig val x : _a list end

David.


_______________________________________________
Sml-implementers mailing list
Sml...@li...
https://lists.sourceforge.net/lists/listinfo/sml-implementers