Re: [Caml-list] Equality between abstract type definitions

[oleg@okmij.org]

Perhaps a bit of history may help. In the Haskell compiler GHC, until
version 6 as I recall, type variables in annotations have the same
semantics as presently in OCaml. That is, type variables in Haskell
were all `flexible', with OCaml's scoping rules. When GHC started to
play with GADTs (ca 2006), the semantics of type variables has changed
-- to what Andreas is proposing. That is, type variables became rigid,
like they are in SML. The scoping rules are cleaned up (although
whether the rules became simpler is the subject of a debate -- there are
lots of corner cases to trip the unwary). The changeover from flexible
to rigid did break all code that used type variables in annotations --
including mine. Well, one learns to live with it. It wasn't the first
or the last time when a new version of GHC breaks code. Almost always the
change is for the better. It seems the community prefers acute but
short pain to the dull and prolonged.

> succ :: a -> a
> succ n = n+1
>
> here is the system's answer
>
>     No instance for (Num a)
>       arising from a use of `+'
>     In the expression: n + 1
>     In an equation for `succ': succ n = n + 1
>
> Is this really more new-user friendly?

Perhaps this is a too advanced example for new users. Polymorphic
numerals of Haskell per se are not new-user friendly. One is welcome
to try to explain to new users the following error message:

> *Prelude> 1 + "a"
>
> <interactive>:1163:3:
>     No instance for (Num [Char])
>       arising from a use of `+'
>     Possible fix: add an instance declaration for (Num [Char])
>     In the expression: 1 + "a"
>     In an equation for `it': it = 1 + "a"

And there are people who may be tempted to follow the proposed fix.

In all fairness, although the error message is greatly off-putting to
the new users, the surprise does not last long and people quickly get
past it. It means the education does work. The same education quickly
tells the users the problem with the original succ example: the
type inferred typed turns out not as general as the type specified
in the annotation. The type variable cannot be quantified without
constraints: the Num a constraint should be added. A better example

    foo :: a -> a
    foo = not

        Couldn't match type `a' with `Bool'
          `a' is a rigid type variable bound by
              the type signature for foo :: a -> a at <interactive>:1165:20
        Expected type: a -> a
          Actual type: Bool -> Bool
        In the expression: not
        In an equation for `foo': foo = not

gives a much more understandable error message, even to new users. GHC
error messages are generally very good: note how the error message
tells where the type variable is bound.

Since all type variables in Haskell are rigid, there is no longer any
convenient way to tell GHC that I think two sub-expression in a large
definition should have the same type. That's a pity. OCaml's type
variables are great for that. OCaml type variables can be understood
purely declaratively, as an assertion from the programmer that all
sub-expressions marked by the same type variables must have the same
type, whatever it turns out to be. I often feel the need for such
annotations in Haskell. There are workarounds, but they are ugly.

My own suggestion is to make clear that type variables in the 'val'
declarations are universally quantified. That is, the inferred type
of 
        let foo = fun x -> x
should be printed as
        val foo : 'a. 'a -> 'a
Likewise, such syntax should be encouraged for val declarations in
modules (omitting the quantifier "'a ." should also be acceptable for
val declarations, perhaps prompting a warning).