-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
I've been trying to use the module system and come across a few issues, some of which I cannot easily pin down, and one which I can.
The issue I can clearly identify concerns what seems to be failure of associativity in structure sharing, and is demonstrated in the following:
signature ORD_DATA = sig type data end; signature VERTEX = sig type name type data end;
signature BVERTEX = sig structure Boundary : ORD_DATA include VERTEX end;
signature GRAPH = sig structure Vertex : VERTEX type T; end;
signature BGRAPH = sig include GRAPH; structure BVertex : BVERTEX sharing Vertex = BVertex end;
signature RG_VERTEX = sig include BVERTEX where type Boundary.data = unit end;
signature RG_GRAPH = sig include BGRAPH structure RGVertex : RG_VERTEX sharing BVertex = RGVertex (* why is it OK if I change BVertex to Vertex? *) end
Running this gives the error: Error: in '/tmp/sml25644bEn', line 26. Cannot share: (unit) is a type function Found near sig include BGRAPH structure RGVertex : RG_VERTEX sharing BVertex = RGVertex end
Exception- Fail Static errors (pass2) raised
Apart from just being confused by what the error means, I am confused that given, in BGraph, "sharing Vertex = BVertex", later I get an error if "BVertex = RGVertex" but not if "Vertex = RGVertex".
Is there some subtle (or obvious?) thing I'm missing?
Another thing I don't quite understand, but which I suspect is just part of the definition of ML, is that you cannot write "sharing type localtype = globaltype", is there some clever reason why this isn't allowed? Or even "sharing local_structure = global_structure", would sometimes be nice. :)
The other issue I have is with the names given to types being printed in error messages; is there any way to control this? I sometimes seem to get mis-typed types; which makes errors hard to spot. A common thing I find is that a parameterised type loses it's parameter. I have example of this I can repeat, but they require a large amount of code... I'll try to find a smaller example.
any suggestions/corrections/infomration, and possibly bug fixes, very welcome! :)
cheers, lucas
Hi Lucas,
The reason your example fails is that sharing is only allowed between non-ground types. You are attempting to share a non-ground type (BVertex.Boundary.data) with a ground type (RGVertex.Boundary.data = unit). In this instance you would need a "where" clause instead. I agree that the PolyML error message isn't clear.
If you replace BVertex with Vertex, there is no constraint on RGVertex.Boundary.data because Vertex doesn't include a Boundary substructure. In SML 97, structure sharing is just an abbreviation for sharing the types that are present in both structures.
Dave.
At 16:35 23/05/2008, Lucas Dixon wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
I've been trying to use the module system and come across a few issues, some of which I cannot easily pin down, and one which I can.
The issue I can clearly identify concerns what seems to be failure of associativity in structure sharing, and is demonstrated in the following:
signature ORD_DATA = sig type data end; signature VERTEX = sig type name type data end;
signature BVERTEX = sig structure Boundary : ORD_DATA include VERTEX end;
signature GRAPH = sig structure Vertex : VERTEX type T; end;
signature BGRAPH = sig include GRAPH; structure BVertex : BVERTEX sharing Vertex = BVertex end;
signature RG_VERTEX = sig include BVERTEX where type Boundary.data = unit end;
signature RG_GRAPH = sig include BGRAPH structure RGVertex : RG_VERTEX sharing BVertex = RGVertex (* why is it OK if I change BVertex to Vertex? *) end
Running this gives the error: Error: in '/tmp/sml25644bEn', line 26. Cannot share: (unit) is a type function Found near sig include BGRAPH structure RGVertex : RG_VERTEX sharing BVertex = RGVertex end
Exception- Fail Static errors (pass2) raised
Apart from just being confused by what the error means, I am confused that given, in BGraph, "sharing Vertex = BVertex", later I get an error if "BVertex = RGVertex" but not if "Vertex = RGVertex".
Is there some subtle (or obvious?) thing I'm missing?
Another thing I don't quite understand, but which I suspect is just part of the definition of ML, is that you cannot write "sharing type localtype = globaltype", is there some clever reason why this isn't allowed? Or even "sharing local_structure = global_structure", would sometimes be nice. :)
The other issue I have is with the names given to types being printed in error messages; is there any way to control this? I sometimes seem to get mis-typed types; which makes errors hard to spot. A common thing I find is that a parameterised type loses it's parameter. I have example of this I can repeat, but they require a large amount of code... I'll try to find a smaller example.
any suggestions/corrections/infomration, and possibly bug fixes, very welcome! :)
cheers, lucas -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFINuQvogMqU4edHsMRAnq3AKDEOOZK6W4Yl9qLIybMvIYRmrGu8ACeKZIG 2RtB76HxIEiw+Kxd/xiYvGw= =mxpJ -----END PGP SIGNATURE----- _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
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?
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... )
You are attempting to share a non-ground type (BVertex.Boundary.data) with a ground type (RGVertex.Boundary.data = unit). In this instance you would need a "where" clause instead. I agree that the PolyML error message isn't clear.
If you replace BVertex with Vertex, there is no constraint on RGVertex.Boundary.data because Vertex doesn't include a Boundary substructure.
Oh yeah, for some reason I missed that! thanks - that certainly clears up my confusion.
thanks! lucas
At 16:35 23/05/2008, Lucas Dixon wrote: I've been trying to use the module system and come across a few issues, some of which I cannot easily pin down, and one which I can.
The issue I can clearly identify concerns what seems to be failure of associativity in structure sharing, and is demonstrated in the following:
signature ORD_DATA = sig type data end; signature VERTEX = sig type name type data end;
signature BVERTEX = sig structure Boundary : ORD_DATA include VERTEX end;
signature GRAPH = sig structure Vertex : VERTEX type T; end;
signature BGRAPH = sig include GRAPH; structure BVertex : BVERTEX sharing Vertex = BVertex end;
signature RG_VERTEX = sig include BVERTEX where type Boundary.data = unit end;
signature RG_GRAPH = sig include BGRAPH structure RGVertex : RG_VERTEX sharing BVertex = RGVertex (* why is it OK if I change BVertex to Vertex? *) end
Running this gives the error: Error: in '/tmp/sml25644bEn', line 26. Cannot share: (unit) is a type function Found near sig include BGRAPH structure RGVertex : RG_VERTEX sharing BVertex = RGVertex end
Exception- Fail Static errors (pass2) raised
Apart from just being confused by what the error means, I am confused that given, in BGraph, "sharing Vertex = BVertex", later I get an error if "BVertex = RGVertex" but not if "Vertex = RGVertex".
Is there some subtle (or obvious?) thing I'm missing?
Another thing I don't quite understand, but which I suspect is just part of the definition of ML, is that you cannot write "sharing type localtype = globaltype", is there some clever reason why this isn't allowed? Or even "sharing local_structure = global_structure", would sometimes be nice. :)
The other issue I have is with the names given to types being printed in error messages; is there any way to control this? I sometimes seem to get mis-typed types; which makes errors hard to spot. A common thing I find is that a parameterised type loses it's parameter. I have example of this I can repeat, but they require a large amount of code... I'll try to find a smaller example.
any suggestions/corrections/infomration, and possibly bug fixes, very welcome! :)
cheers, lucas
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 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
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
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
Hi Lucas,
It's more complicated than that. If you want to pursue this, you need to get hold of the formal semantics of Standard ML and construct proposals in terms of that semantics. There are people in Informatics who should have copies of the definition and the "commentary" that accompanies it.
Dave.
At 17:28 02/07/2008, Lucas Dixon wrote:
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
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
Dave Berry wrote:
Hi Lucas,
It's more complicated than that. If you want to pursue this, you need to get hold of the formal semantics of Standard ML and construct proposals in terms of that semantics. There are people in Informatics who should have copies of the definition and the "commentary" that accompanies it.
Hi Dave,
I am not sure it is more complicated than that: structure sharing, as of ML 97, is an abbreviation for sharing the types in the structure (sharing type ... = ...) and given David Matthews statement that this is only allowed for unconstrained type identifiers, I'm suggesting the abbreviation is only expanded for unconstrained type identifiers.
This doesn't affect the semantics as I'm just suggesting a different abbreviation that happens outside the semantics. Or is there something else I missed?
lucas
-
dave＠berrybental.me.uk -
David.Matthews＠prolingua.co.uk -
ldixon＠inf.ed.ac.uk -
pclayton＠taz.qinetiq.com