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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

Dear Andreas,

It is a bit late to enter this discussion, but I just have two comments

1) All the bug reports (and messages on this list, but for this one) I have seen were
  about the non-generalization of type variables, not their interpretation. Namely,
  people have a hard time understanding why the following is not accepted:

    let f () =
      let id : 'a -> 'a = fun x -> x in
      (id 1, id true)

  I agree that in this respect SML’s choice of inferring a minimal scope (and allowing
  local generalization of named type variables) is more helpful.
  This part could be implemented without breaking existing programs.
  Note however that we already have other ways of introducing local type variables.
  (For instance, writing " id : ‘a. ‘a -> ‘a " in the above.)

2) In ocaml, type variables are also used for describing sharing in recursive types:
     (<m : int; self : 'a> as ‘a)
    and also for talking about types that have a row variable
     (< m : int; .. > as ‘a) -> ‘a
    These two cases use an existential view of type variables.

Jacques

> On Oct 25, 2013, at 01:23 , Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
>> In OCaml, type variables used in type annotations are just unification variables:
>> the type checker is allowed to merge them or instantiate them.
>> This is useful when you want to indicate that two things have the same type,
>> without writing the type by hand.
> 
> Jacques, do you think there is any chance that this will ever be changed? I think this keeps being one of the most annoying pitfalls in the OCaml type system, not what most people expect, and in 98% of the cases, not what they want either -- especially since there often is no convenient way to actually express what they want.
> 
> A simple proposal, which I'm sure has been made many times before, would be to interpret type variables of the form 'a, 'b as proper universal variables, and only ones of the form '_a, '_b as unification variables. That matches the notation that OCaml has always been using in its output. More expressive and clearer signalling of intent.
> 
> Obviously, such a change would break some code, code that actually relies on 'a being just a unification variable. But my optimistic guess is that such code is rather rare. And it would be trivial to adapt.
> 
> It would also break code that assumed the wrong behaviour and only compiled by accident (such as the Peter's example). But arguably, that's a good thing, because it uncovers actual bugs.
> 
> Anyway, just dreaming aloud… :)
> 
> /Andreas
>