On 5/04/2013, at 1:22 AM, Tillmann Rendel wrote:
Hi,
Richard A. O'Keefe wrote:
As I understand it, in ML, it seemed to be a clever idea to not have type signatures at all.
Wrong. In ML, it seemed to be a clever idea not to *NEED* type signatures, and for local definitions they are very commonly omitted.
In the ML I used, I remember that it was syntactically impossible to use type signatures directly adjacent to a local definition.
Notice that the goal-posts just got moved far far away. The original complaint was that ML did not allow type signatures. Now the complaint is that it does not allow them to be "directly adjacent".
Instead, I was thaught to put something like a type signature in a comment, approximately like this:
(* getOpt : 'a option * 'a -> 'a *) fun getOpt (SOME x, y) = x | getOpt (NONE, y) = y
Well, that's a bit silly, isn't it? Put getOpt in a structure where it belongs, and the type in the signature, where the compiler can enforce it. A type signature that is not enforced is a type signature you cannot trust.
But you can certainly HAVE type signatures, and for modules ('structures') it is normal to have them in the interfaces ('signatures').
In my opinion, a signature for a structure would not count as "directly adjacent". Also, while I don't know much about the history of ML, I suspect that structures and signatures were a later addition to the core language.
The history of ML is not so hard to find out. Structures and signatures have been part of "Standard" ML since the 1980s. The ML in Edinburgh LCF and Luca Cardelli's VAX ML were significantly different languages from SML, but VAX ML at least did have modules. The distinction between "Core" and "Modules" in old SML documentation has to do with convenience of specification more than anything else.
I just checked Milner, Tofte and Harper, The Definition of Standard ML, MIT Press 1990 (available at http://www.itu.dk/people/tofte/publ/1990sml/1990sml.html),
That's the old out-of-date edition. The current version of the language is SML'97. However, this much is the same: - there are declarations that provide *interfaces* (grammatical category "spec" -- see page 13), which may occur in signatures - and declarations that provide *values* (grammatical category "dec" -- see page 8), which may occur in structures, at top level, and elsewhere So it is definitely true that, by design, SML "type signatures" (strictly speaking, "valdescs") are segregated from SML function definitions ("valbinds" or "fvalbinds"). This is pretty much a consequence of SML having a very expressive module system in which modules _have_ signatures.
and learned that we can have explicit type annotations for both patterns and expressions, so the following variants of the above are possible in Standard ML:
1. We can embed parts of the signature into the definition:
fun getOpt (SOME (x : 'a), y : 'a) : 'a = x | getOpt (NONE, y : 'a) : 'a = y
Perhaps better: fun get_opt (SOME x, _) = x | get_opt (NONE, y) = y val getOpt : 'a option * 'a -> 'a = get_opt which can be written local fun getOpt(SOME x, _) = x | getOpt(NONE, y) = y in val getOpt: 'a option * 'a -> 'a = getOpt end
With decomposing the type signature into its parts, and then duplicating these parts, this is not very attractive.
This is a sure sign that you are NOT using the language the way it was intended to be used, and maybe it isn't the language that's wrong.
2. We can do better by avoiding the derived form for function bindings:
val getOpt : 'a option * 'a -> 'a = fn (SOME x, y) => x | (NONE, y) => y
This looks ok to me, and I wonder why I was not thaught this style,
Because it is atrociously ugly. (Aside.) "val" here should be "val rec" in general. (End Aside). ML is designed to have type specifications for functions *inside signatures*. Since functions are supposed to be declared inside structures, and structures are supposed to *have* signatures, it would be rather silly to write function type specifications twice. So ML is *not* designed to encourage you to do that.