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

[Roberto Di Cosmo <roberto@dicosmo.org>]

Dear Andreas,
     let me offer a comment on terminology here: 'a, 'b and the
like have always been used to denote polymorphism in a type, and
hence used as unification variables since the beginning of the ML
language history, to infer the type of a program.

When you annotate a program with types, you are just adding more
type equations to the unification problem, and you may of
course get at the end a type that is less generic than the one
you gave in the annotation (that's the key rule of the game
in unification).

I am curious to know why you consider this a pitfall: if it is
not what people expect, it is probably because nobody explained
their meaning to them properly, and I am quite interested in
understanding how to explain this better.

On the other side, the '_a, '_b variables are just a convenient device that
allows to give a type to programs with side effect when OCaml does not know if
it's safe to apply the generalization rule: a function f of type '_a -> '_a can
be instantiated only once, and after that its type will no longer change
(sometimes these are called "logical" variables, but this terminology is kind of
misleading).  You cannot use '_a variables yourself:

# let f (x: '_a) = x;;
Error: The type variable name '_a is not allowed in programs

--
Roberto

On Fri, Oct 25, 2013 at 08:44:50AM +0200, Andreas Rossberg wrote:
> 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
> 
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

-- 
Roberto Di Cosmo
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 3020 (3rd floor)
Batiment Sophie Germain
Avenue de France
Metro Bibliotheque Francois Mitterrand, ligne 14/RER C
-----------------------------------------------------------------
GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3