I had another thought on this which would work just as well and be much simpler: one could ignore types which are ground? since they are not allowed why give an error about them; simply share all other ones.

Of course, my preferred solution would be to simply check that they ground types are the same.


Lucas Dixon wrote:
Hash: SHA1

Thanks for the explanation; sounds like there are some rough edges there
that could be improved, but I get the gist of the point.

I'm pretty sure that type checking would not become undecidable or even
much more difficult if you allow sharing between unconstrained types. I
guess I should hash out, more formally, a theory for this. Do you know
what the plans are for another/next version of ML? Have other people
already proposed a `better' theory for ML modules?


David Matthews wrote:
Dave Berry wrote:
The reason your example fails is that sharing is only allowed between
non-ground types.
Yes, I was wondering about this restriction - is there some reason for
I think it's more general than just not allowing sharing between
non-ground types.  Sharing is not allowed between types other than
unconstrained type identifiers.  So the following is illegal:
signature S =
   type s
   type t = s*s
   type u
   sharing type t = u

I think the reason is that allowing it could result in undecidable type
schemes or at least something that would be very difficult to check.

More generally, I'm slightly confused about the distinction between
"where" and "sharing"; it seems that sharing is a restricted form of the
signature constraint that can be imposed by using "where".  Is this the
case, or is there a deeper difference? (as you pointed out, the
structure sharing is just an abbreviation for individual type sharing...
would be nice to have something similar for "where" - where signature A
= B... )
I seem to recall that ML90 did not have "where type" but did allow some
sharing between ground types and types in signatures.  In the ML97
semantics "sharing" and "where type" are treated differently.  The
semantics has a notion of a "type name" which is a sort of unique
identifier.  The sharing constraint says that two types share the same
type name so when the signature is matched to a structure the same
ground type must be used for both.  A "where type t = ty" declaration
introduces a "type function" into the name space in which a type
identifier (t) maps to a type function (ty).  Type functions don't have
"type names" so can't be the subject of sharing constraints.

If that isn't clear that's probably because I find it all rather
confusing myself and it's a long time since I looked at this.


Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

polyml mailing list

polyml mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to