
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. 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 An example of this style can be found in Danvy and Nielsen, Defunctionalization at Work, Proc. of PPDP 2001 (extended version available at ftp://ftp.daimi.au.dk/pub/BRICS/Reports/RS/01/23/BRICS-RS-01-23.pdf).
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. 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), 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 With decomposing the type signature into its parts, and then duplicating these parts, this is not very attractive. 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, at least as an alternative. The benefit over type signatures in comments is clear: The type checker will check that the signatures are accurate, and there is a chance that error messages contain type variables chosen by the programmer instead of automatically generated names. Tillmann