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
Lucas Dixon wrote:
-----BEGIN PGP SIGNED MESSAGE----- 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?
cheers, lucas
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 it?
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 = sig type s type t = s*s type u sharing type t = u end;
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.
David
-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFIQY3MogMqU4edHsMRAt5HAKCJUuHrg+1PqVQG+xjGl1rgoNJIXgCcDggH piGt+sB859FsTPwBbMIQq7w= =ivMA -----END PGP SIGNATURE----- _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml