Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
I suppose that I'm free to ignore D) and use the more IMHO intuitive C) declaration. I thought that I'd ask to make sure that I wasn't missing something in the D) one. TIA ....
On 1/29/2026 6:18 PM, Duke Normandin wrote:
Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
The type of the result is a real by implication of what * does on reals, i.e., it produces a real.
Eliot Moss
On Thu, 29 Jan 2026 21:38:48 -0500 Eliot Moss moss@cs.umass.edu wrote:
On 1/29/2026 6:18 PM, Duke Normandin wrote:
Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
The type of the result is a real by implication of what * does on reals, i.e., it produces a real.
An "implied" result type! Now why didn't I think of that?
Personally, I prefer:
fun square (x:real) = x * x : real;
because it's self-documenting to the max, IMO.
Thx for your reply ...
On 1/30/2026 12:16 AM, Duke Normandin wrote:
On Thu, 29 Jan 2026 21:38:48 -0500 Eliot Moss moss@cs.umass.edu wrote:
On 1/29/2026 6:18 PM, Duke Normandin wrote:
Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
The type of the result is a real by implication of what * does on reals, i.e., it produces a real.
An "implied" result type! Now why didn't I think of that?
Personally, I prefer:
fun square (x:real) = x * x : real;
because it's self-documenting to the max, IMO.
Functional languages are big on type inference. It can be a culture shock coming from languages that require many more type annotations.
EM
On Fri, 30 Jan 2026 06:45:43 -0500 Eliot Moss moss@cs.umass.edu wrote:
On 1/30/2026 12:16 AM, Duke Normandin wrote:
On Thu, 29 Jan 2026 21:38:48 -0500 Eliot Moss moss@cs.umass.edu wrote:
On 1/29/2026 6:18 PM, Duke Normandin wrote:
Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
The type of the result is a real by implication of what * does on reals, i.e., it produces a real.
An "implied" result type! Now why didn't I think of that?
Personally, I prefer:
fun square (x:real) = x * x : real;
because it's self-documenting to the max, IMO.
Functional languages are big on type inference.
I'm gathering as much ...
It can be a culture shock coming from languages that require many more type annotations.
Thankfully, it seems to me that using type inference can be by-passed most of the time. I'd hate to have to come back to my code 6 mos down the round and wonder what was *inferred* in the code. Commenting the code and/or using more type annotation - finding a suitable balance!
On 30/01/2026 20:18, Duke Normandin wrote:
It can be a culture shock coming from languages that require many more type annotations.
Thankfully, it seems to me that using type inference can be by-passed most of the time. I'd hate to have to come back to my code 6 mos down the round and wonder what was *inferred* in the code. Commenting the code and/or using more type annotation - finding a suitable balance!
No, you can't bypass the best of the culture.
It is a fine art to write just the right type constraints in the source text --- not to much, not too little --- both for readability, maintainability, robustness of compilation.
This is another opportunity to try our fine IDE for Poly/ML and Isabelle/ML https://isabelle.in.tum.de --- it provides control-hover-mouse tooltips for types inferred by the ML compiler, and many more things.
It also highlights scopes of defined entities, as you have been asking before on this list.
Makarius
On 1/30/2026 2:18 PM, Duke Normandin wrote:
On Fri, 30 Jan 2026 06:45:43 -0500 Eliot Moss moss@cs.umass.edu wrote:
On 1/30/2026 12:16 AM, Duke Normandin wrote:
On Thu, 29 Jan 2026 21:38:48 -0500 Eliot Moss moss@cs.umass.edu wrote:
On 1/29/2026 6:18 PM, Duke Normandin wrote:
Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
The type of the result is a real by implication of what * does on reals, i.e., it produces a real.
An "implied" result type! Now why didn't I think of that?
Personally, I prefer:
fun square (x:real) = x * x : real;
because it's self-documenting to the max, IMO.
Functional languages are big on type inference.
I'm gathering as much ...
It can be a culture shock coming from languages that require many more type annotations.
Thankfully, it seems to me that using type inference can be by-passed most of the time. I'd hate to have to come back to my code 6 mos down the round and wonder what was *inferred* in the code. Commenting the code and/or using more type annotation - finding a suitable balance!
Well, I've been coding in various languages since 1966 (8th grade), and I think that it's more helpful to try to meet each language on its own terms. I can take a while to get the hang of a particular language's "flow", but once you have it, going with the flow can be great. W.r.t type inference, I'll also mention that the trend for Java over time has been to introduce more type inference. This is different from *dynamic* typing, such as seen in Python and Javascript. I think you can make stronger arguments that that kind of dynamicity tend to undermine software reliability.
Cheers - EM
btw - another inconsistency between compilers
- fun square x = x * x;
val square = fn : int -> int
ie Moscow ML assumes int as a sort of default
Jeremy
On 30/1/26 16:16, Duke Normandin wrote:
On Thu, 29 Jan 2026 21:38:48 -0500 Eliot Moss moss@cs.umass.edu wrote:
On 1/29/2026 6:18 PM, Duke Normandin wrote:
Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
The type of the result is a real by implication of what * does on reals, i.e., it produces a real.
An "implied" result type! Now why didn't I think of that?
Personally, I prefer:
fun square (x:real) = x * x : real;
because it's self-documenting to the max, IMO.
Thx for your reply ...
On Tue, 3 Feb 2026 11:07:38 +1100 Jeremy Dawson jeredaw@gmx.com wrote:
btw - another inconsistency between compilers
- fun square x = x * x;
val square = fn : int -> int
ie Moscow ML assumes int as a sort of default
Thx for both your replies! Still waiting for Paulson's book to arrive, although I suspect that I might have been too impulsive in buying the book so soon.
On 03/02/2026 07:24, Duke Normandin wrote:
Still waiting for Paulson's book to arrive, although I suspect that I might have been too impulsive in buying the book so soon.
You can download the book here: https://www.cl.cam.ac.uk/~lp15/MLbook
It was once very influential to the Interactive Theorem Prover community many decades ago, as far as Standard ML is concerned. Now it is rather dated, not to say archaic.
When I browse today, I learn many things about approaches from distant past. Now, I would do it quite differently, e.g. see the vast Isabelle/ML codebase, with its main library in Isabelle/Pure.
Makarius
On 03/02/2026 00:07, Jeremy Dawson wrote:
btw - another inconsistency between compilers
- fun square x = x * x;
val square = fn : int -> int
ie Moscow ML assumes int as a sort of default
The default type for an overloaded operator, other than /, is defined to be int, so every compiler ought to treat it that way. The definition is vague on how much context to use in determining overloading. Poly/ML uses the whole "topdec"; other compilers require the overloading to be resolved within the function definition.
David
David,
Just to clarify the below, / in SML97 was defined to have type Real * Real -. Real where Real stands for some type in a set of types that contain the type real but may contain other types that extend or restrict the type real (such as reals with a higher or lower precision than the required type real or maybe complex numbers). Hence SML97 defines that / defaults to type real * real -> real, if there is no information for the type inferrer to determine otherwise.
Have I got that right? As far as I know, none of the extant SML compilers include any sucn extensions or restrictions of the type real.
Regards,
Rob.
On 3 Feb 2026, at 12:38, David Matthews David.Matthews@prolingua.co.uk wrote:
On 03/02/2026 00:07, Jeremy Dawson wrote:
btw - another inconsistency between compilers
- fun square x = x * x;
val square = fn : int -> int
ie Moscow ML assumes int as a sort of default
The default type for an overloaded operator, other than /, is defined to be int, so every compiler ought to treat it that way. The definition is vague on how much context to use in determining overloading. Poly/ML uses the whole "topdec"; other compilers require the overloading to be resolved within the function definition.
David
Poly/ML mailing list -- polyml@lists.polyml.org To unsubscribe send an email to polyml-leave@lists.polyml.org
no you're wrong about (D), it means square x is real
try the following to see
(1) fun f 2.0 : int = 2 ; (2) fun f 2.0 : real = 2 ;
incidentally, try fun (f : real -> real) x = x ;
from memory (going back over 20 years) it works in some compilers not in others
Cheers,
Jeremy
On 30/1/26 10:18, Duke Normandin wrote:
Taken from Paulson's book: Chap2.4
A) fun square x = x * x;
Error- Unable to resolve overloading for *
I understand the above!
B) fun square(x : real) = x * x; I understand: x is declared as a real
C) fun square x = x * x : real; I see this as declaring a function w/o parentheses AND that the r_result_ is a 'real'
I have a problem with this declaration:
D) fun square x : real = x * x; I see this as declaring a function w/o parentheses, AND declaring x to be a 'real' I do NOT see/understand that this syntax indicates that the type of the _result_ is a 'real'
I suppose that I'm free to ignore D) and use the more IMHO intuitive C) declaration. I thought that I'd ask to make sure that I wasn't missing something in the D) one. TIA ....
-
David Matthews -
Duke Normandin -
Eliot Moss -
Jeremy Dawson -
Makarius -
Rob Arthan