[Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.

[Richard A. O'Keefe]

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.