For example, given
infix & datatype t = &
Poly/ML (5.4) reports:
Warning-(&) has infix status but was not preceded by op.
So Poly/ML seems to prefer the use of 'op' in a datatype declaration. However, if 'op' is present, i.e.
datatype t = op &
SML/NJ (110.73) reports:
stdIn:2.14-2.16 Warning: unnecessary `op'
Generally, it is a good principle to avoid warnings but, in this particular respect, that isn't possible for code that is shared between Poly/ML and SML/NJ. Note that MLton (20100608) doesn't warn either way.
Does the Standard provide any guidance about the use of op here? Can anything be done to align the warnings from Poly/ML and SML/NJ in this respect?
Thanks, Phil
On 27 Mar 2012, at 22:41, Phil Clayton wrote:
For example, given
infix & datatype t = &
Poly/ML (5.4) reports:
Warning-(&) has infix status but was not preceded by op.
So Poly/ML seems to prefer the use of 'op' in a datatype declaration. However, if 'op' is present, i.e.
datatype t = op &
SML/NJ (110.73) reports:
stdIn:2.14-2.16 Warning: unnecessary `op'
Generally, it is a good principle to avoid warnings but, in this particular respect, that isn't possible for code that is shared between Poly/ML and SML/NJ. Note that MLton (20100608) doesn't warn either way.
Does the Standard provide any guidance about the use of op here?
All it says is "The only required use of op is in prefixing a non-infixed occurrence of an identifier vid which has infix status; elsewhere op, where permitted, has no effect". vid here is the syntactic category of value identifiers. Then at various points in the syntax an optional op appears (written <op>). The relevant point in the syntax here is in the production for conbind, the thing to the right of the equals signs in a data type declaration. It looks like this:
conbind = <op> vid < of ty> < | conbind>
It is a bit odd to allow op here if it is never necessary, so I can see the Poly/ML point of view, suggesting that it is good style to put it in. On the other hand, there is nothing else other than a vid that can appear immediately after the equauls signs in datatype declaration, so I can see the SML/NJ point of view too. However, SML/NJ isn't consistent. What I have just said about the equals sign in a data type declaration is equally try of a value declaration. If you try:
val x = &;
or (after starting again and reentering the infix declaration)
val & = 99;
Poly/ML will give you a warning, while SML/NJ will reject these both as errors, which I think is wrong.
Can anything be done to align the warnings from Poly/ML and SML/NJ in this respect?
The standard is unclear, since it fails to define what "non-infixed occurrence" means. It looks like SML/NJ is taking it to mean an occurrence where a pattern or an expression is expected, while Poly/ML is taking it to mean an occurrence where it would be possible to parse the vid as infix, but the non-infix construal is wanted. However Poly/ML is not completely consistent about this as shown in the following transcript.
infix &;
fun &(x,y) = x + y + 1;
Warning-(&) has infix status but was not preceded by op. val & = fn: int * int -> int
&(1,2);
Warning-(&) has infix status but was not preceded by op. val it = 4: int
exception &;
exception &;
fun f _ = ();
val f = fn: 'a -> unit
f(&);
Warning-(&) has infix status but was not preceded by op. val it = (): unit
(f &);
Error-<identifier> expected but ) was found
I would have expected Poly/ML to give a warning on the exception binding. I also can't explain why it doesn't allow (f &). Maybe David can give a more accurate explanation of when Poly/ML requires op.
Regards,
Rob.
On 29/03/2012 16:00, Rob Arthan wrote:
On 27 Mar 2012, at 22:41, Phil Clayton wrote:
For example, given
infix& datatype t =&
Poly/ML (5.4) reports:
Warning-(&) has infix status but was not preceded by op.
So Poly/ML seems to prefer the use of 'op' in a datatype declaration. However, if 'op' is present, i.e.
I've had another look at this and committed a change to the parser. I can't see any reason for producing the warning in this case so I've removed it. I have a vague feeling that in an early draft of Standard ML the syntax of datatype bindings more closely resembled pattern matching so there was a real reason for using "op". Something like datatype 'a list = nil | 'a :: 'a list compared with datatype 'a list = nil | op :: 'a * 'a list
Looking carefully at the syntax, though, "op" is not allowed in a datatype specification although in all other respects the syntax of a binding and a specification are the same. I've added an error message if "op" is used in a specification.
Can anything be done to align the warnings from Poly/ML and SML/NJ in this respect?
It is, of course, possible to write local nonfix & in datatype t = & end This should work in both Poly/ML and SML/NJ although I haven't tested SML/NJ here.
(f&);
Error-<identifier> expected but ) was found
I would have expected Poly/ML to give a warning on the exception binding. I also can't explain why it doesn't allow (f&). Maybe David can give a more accurate explanation of when Poly/ML requires op.
I hadn't actually realised that "op" was allowed on exception bindings and I've now fixed that. I think a sensible approach is to produce a warning in the cases where a symbol could be used as an infix; in an expression, a fun binding or in a pattern (val binding) and to ignore it in other cases.
The reason that "f &" gives an error is that here we have something that could actually be an infixed use of "&" but isn't because the right-hand side is missing. I think it's actually more helpful than producing a warning. For example, val a = 1; val b = a + ; is probably a missing expression. Producing a warning about a missing "op" and then an error saying "a" is not a function could well be more confusing than helpful.
David
On 30/03/12 12:52, David Matthews wrote:
It is, of course, possible to write local nonfix & in datatype t = & end This should work in both Poly/ML and SML/NJ although I haven't tested SML/NJ here.
Good point - I'd forgotten about nonfix.
Thanks for the updates. That is much more preferable to a workaround!
Phil
On 30 Mar 2012, at 12:52, David Matthews wrote:
On 29/03/2012 16:00, Rob Arthan wrote:
On 27 Mar 2012, at 22:41, Phil Clayton wrote:
For example, given
infix& datatype t =&
Poly/ML (5.4) reports:
Warning-(&) has infix status but was not preceded by op.
So Poly/ML seems to prefer the use of 'op' in a datatype declaration. However, if 'op' is present, i.e.
I've had another look at this and committed a change to the parser. I can't see any reason for producing the warning in this case so I've removed it. I have a vague feeling that in an early draft of Standard ML the syntax of datatype bindings more closely resembled pattern matching so there was a real reason for using "op". Something like datatype 'a list = nil | 'a :: 'a list compared with datatype 'a list = nil | op :: 'a * 'a list
Looking carefully at the syntax, though, "op" is not allowed in a datatype specification although in all other respects the syntax of a binding and a specification are the same. I've added an error message if "op" is used in a specification.
I didn't look at the syntax of modules. You are quite right. In fact, as far as I can see, op is not allowed anywhere in a signature.
Can anything be done to align the warnings from Poly/ML and SML/NJ in this respect?
It is, of course, possible to write local nonfix & in datatype t = & end This should work in both Poly/ML and SML/NJ although I haven't tested SML/NJ here.
(f&);
Error-<identifier> expected but ) was found
I would have expected Poly/ML to give a warning on the exception binding. I also can't explain why it doesn't allow (f&). Maybe David can give a more accurate explanation of when Poly/ML requires op.
I hadn't actually realised that "op" was allowed on exception bindings and I've now fixed that. I think a sensible approach is to produce a warning in the cases where a symbol could be used as an infix; in an expression, a fun binding or in a pattern (val binding) and to ignore it in other cases.
I think it is wise to give the warning in those cases, because other compilers are not as liberal as Poly/ML, so I read the warning as a warning about a potential portability problem (and always act on it).
The reason that "f &" gives an error is that here we have something that could actually be an infixed use of "&" but isn't because the right-hand side is missing. I think it's actually more helpful than producing a warning. For example, val a = 1; val b = a + ; is probably a missing expression. Producing a warning about a missing "op" and then an error saying "a" is not a function could well be more confusing than helpful.
Out of interest, are you still planning to allow things like "(+)"?
Regards,
Rob.
On 03/04/2012 16:20, Rob Arthan wrote:
On 30 Mar 2012, at 12:52, David Matthews wrote:
Looking carefully at the syntax, though, "op" is not allowed in a datatype specification although in all other respects the syntax of a binding and a specification are the same. I've added an error message if "op" is used in a specification.
I didn't look at the syntax of modules. You are quite right. In fact, as far as I can see, op is not allowed anywhere in a signature.
I've now reduced the error message to a warning since it seems Isabelle has "op" in signatures.
I hadn't actually realised that "op" was allowed on exception bindings and I've now fixed that. I think a sensible approach is to produce a warning in the cases where a symbol could be used as an infix; in an expression, a fun binding or in a pattern (val binding) and to ignore it in other cases.
I think it is wise to give the warning in those cases, because other compilers are not as liberal as Poly/ML, so I read the warning as a warning about a potential portability problem (and always act on it).
Do any other compilers complain about missing "op" in those cases? Phil's point was that SML/NJ was complaining about the presence of "op" rather than its absence. I tried an "op" in a datatype in a signature in MLton and it didn't say anything although it's not correct.
Out of interest, are you still planning to allow things like "(+)"?
Do you mean something like val p = map (+) rather than val p = map (op +) ? I wasn't planning to since I don't think it's legal ML. Did you mean somewhere else?
Regards, David
On 4 Apr 2012, at 11:48, David Matthews wrote:
On 03/04/2012 16:20, Rob Arthan wrote:
On 30 Mar 2012, at 12:52, David Matthews wrote:
Looking carefully at the syntax, though, "op" is not allowed in a datatype specification although in all other respects the syntax of a binding and a specification are the same. I've added an error message if "op" is used in a specification.
I didn't look at the syntax of modules. You are quite right. In fact, as far as I can see, op is not allowed anywhere in a signature.
I've now reduced the error message to a warning since it seems Isabelle has "op" in signatures.
Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply with the standard syntax, even though I was completely unaware that "op" wasn't allowed in signatures.
I hadn't actually realised that "op" was allowed on exception bindings and I've now fixed that. I think a sensible approach is to produce a warning in the cases where a symbol could be used as an infix; in an expression, a fun binding or in a pattern (val binding) and to ignore it in other cases.
I think it is wise to give the warning in those cases, because other compilers are not as liberal as Poly/ML, so I read the warning as a warning about a potential portability problem (and always act on it).
Do any other compilers complain about missing "op" in those cases?
Yes, SML/NJ and MLton don't allow an infix vid without an "op" as an expression or a pattern.
Phil's point was that SML/NJ was complaining about the presence of "op" rather than its absence.
It is only a warning. I think Phil's point was that, as things stood, you couldn't write a datatype declaration with an infix constructor that would not give a warning on one of the two compilers: as was, Poly/ML warned when you didn't use "op" before an infix constructor in a datatype, while SML/NJ warned when you did.
I tried an "op" in a datatype in a signature in MLton and it didn't say anything although it's not correct.
Likewise SML/NJ appears to extend the standard syntax by allowing "op" in datatypes in signature (but giving a warning saying that they are unnecessary).
Out of interest, are you still planning to allow things like "(+)"?
Do you mean something like val p = map (+) rather than val p = map (op +) ? I wasn't planning to since I don't think it's legal ML. Did you mean somewhere else?
No, that is what I meant: Poly/ML 5.4.1 doesn't share your view that it is illegal:
Poly/ML 5.4.1 Release
(+);
Warning-(+) has infix status but was not preceded by op. val it = fn: int * int -> int
map (+);
Warning-(+) has infix status but was not preceded by op. val it = fn: (int * int) list -> int list
This is why I said the warning is useful as it flags a potential portability problem: other compilers won't compile the above.
Regards,
Rob.
On Wed, 4 Apr 2012, Rob Arthan wrote:
On 4 Apr 2012, at 11:48, David Matthews wrote:
On 03/04/2012 16:20, Rob Arthan wrote:
On 30 Mar 2012, at 12:52, David Matthews wrote:
Looking carefully at the syntax, though, "op" is not allowed in a datatype specification although in all other respects the syntax of a binding and a specification are the same. I've added an error message if "op" is used in a specification.
I didn't look at the syntax of modules. You are quite right. In fact, as far as I can see, op is not allowed anywhere in a signature.
I've now reduced the error message to a warning since it seems Isabelle has "op" in signatures.
Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply with the standard syntax, even though I was completely unaware that "op" wasn't allowed in signatures.
Historically, we've always tried to minimize the problems in the grey areas of the SML standard, with its occasional changes that were not immediately clear from outside.
I have no problems to remove inappropriate "op" occurrences from the Isabelle sources, if it does not break SML/NJ or old versions of Poly/ML (5.2.1, 5.3.0, 5.4.x). On the other hand it will make testing of old Isabelle versions with brand new Poly/ML versions more difficult.
Makarius
On 4 Apr 2012, at 14:33, Makarius wrote:
On Wed, 4 Apr 2012, Rob Arthan wrote:
On 4 Apr 2012, at 11:48, David Matthews wrote:
On 03/04/2012 16:20, Rob Arthan wrote:
On 30 Mar 2012, at 12:52, David Matthews wrote:
Looking carefully at the syntax, though, "op" is not allowed in a datatype specification although in all other respects the syntax of a binding and a specification are the same. I've added an error message if "op" is used in a specification.
I didn't look at the syntax of modules. You are quite right. In fact, as far as I can see, op is not allowed anywhere in a signature.
I've now reduced the error message to a warning since it seems Isabelle has "op" in signatures.
Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply with the standard syntax, even though I was completely unaware that "op" wasn't allowed in signatures.
Historically, we've always tried to minimize the problems in the grey areas of the SML standard, with its occasional changes that were not immediately clear from outside.
I have no problems to remove inappropriate "op" occurrences from the Isabelle sources, if it does not break SML/NJ or old versions of Poly/ML (5.2.1, 5.3.0, 5.4.x). On the other hand it will make testing of old Isabelle versions with brand new Poly/ML versions more difficult.
I should explain that "Tut, tut" was just intended to be a light-hearted jibe at the Isabelle code. I didn't intend to suggest that Poly/ML should stop supporting the extended syntax that allows your old code to compile.
Regards,
Rob.
On 04/04/2012 14:33, Makarius wrote:
On Wed, 4 Apr 2012, Rob Arthan wrote:
I've now reduced the error message to a warning since it seems Isabelle has "op" in signatures.
Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply with the standard syntax, even though I was completely unaware that "op" wasn't allowed in signatures.
Historically, we've always tried to minimize the problems in the grey areas of the SML standard, with its occasional changes that were not immediately clear from outside.
I have no problems to remove inappropriate "op" occurrences from the Isabelle sources, if it does not break SML/NJ or old versions of Poly/ML (5.2.1, 5.3.0, 5.4.x). On the other hand it will make testing of old Isabelle versions with brand new Poly/ML versions more difficult.
It's probably worth summarising the current and previous situation.
There's no change to the handling of patterns or expressions. Poly/ML produces warnings if it is able to parse an infix operator without "op". So "(+)" and "map (+)" will continue to be accepted but produce a warning.
"op" is now allowed in exception declarations but not in signatures. So exception op y exception op x = op y are accepted. The "op" is simply ignored; there's no warning if it is missing for infix operators.
In a datatype constructor previously a warning was produced if a value constructor was declared which had infix status but "op" was not used. That warning has been removed so "op" is simply ignored.
In a datatype specification (i.e. in a signature) "op" used to be allowed but ignored. No warning was produced for constructors with infix status. This has changed. Now a warning is produced if "op" is used at all. This is the only place where a warning is produced when it wasn't previously. Since I've now realised that the ML syntax does not allow an "op" here it seems sensible to produce some sort of message. It could cause compatibility problems if other compilers stick to the letter of the ML standard, although it doesn't look like they do. It should be possible get rid of this warning by removing the "op" and still retain compatibility with older versions of Poly/ML since they never complained about a missing "op".
In any case this is just the current SVN and I'm open to suggestions for changes.
Regards, David
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
phil.clayton＠lineone.net -
rda＠lemma-one.com