There are various ideas about how to take SML forward on the successor ML site: http://successor-ml.org/ This includes items relating to modules. Some of these items could be implemented in an experimental version of HaMLet: http://www.ps.uni-sb.de/hamlet/ I haven't looked myself though.
Hope that's a useful start, Phil
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
The information contained in this E-Mail and any subsequent correspondence is private and is intended solely for the intended recipient(s). The information in this communication may be confidential and/or legally privileged. Nothing in this e-mail is intended to conclude a contract on behalf of QinetiQ or make QinetiQ subject to any other legally binding commitments, unless the e-mail contains an express statement to the contrary or incorporates a formal Purchase Order.
For those other than the recipient any disclosure, copying, distribution, or any action taken or omitted to be taken in reliance on such information is prohibited and may be unlawful.
Emails and other electronic communication with QinetiQ may be monitored and recorded for business purposes including security, audit and archival purposes. Any response to this email indicates consent to this.
Telephone calls to QinetiQ may be monitored or recorded for quality control, security and other business purposes.
QinetiQ Limited Registered in England & Wales: Company Number:3796233 Registered office: 85 Buckingham Gate, London SW1E 6PD, United Kingdom Trading address: Cody Technology Park, Cody Building, Ively Road, Farnborough, Hampshire, GU14 0LX, United Kingdom http://www.QinetiQ.com/home/legal.html