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

[Tillmann Rendel]

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