[Caml-list] Equality between abstract type definitions

[Caml-list] Equality between abstract type definitions

[Peter Frey]

Please consider the following two definitions of map which I would have
considered equal.  

  exception Empty

  type 'a t = Cons of 'a * (int -> 'a t) * int

  let null = Cons( Obj.magic None, (fun _ -> assert false), max_int ) 

  let map (f: 'a -> 'b) (t: 'a t) : 'b t =
      if t == null then null else match t with (Cons( h, fn, p )) ->
      let rec aux h1 p1 =
      try match fn p1 with (Cons (h2,_, p2)) -> 
         (Cons(f h1, aux h2, p2 ))
      with Empty                             -> (Cons(f h1, fn, p1)) in
      aux h p

  let map : 'a 'b. ( 'a -> 'b ) -> 'a t -> 'b t = fun f t -> 
    if t == null then null else match t with (Cons( h, fn, p )) ->
    let rec aux h1 p1 =
      try match fn p1 with (Cons (h2,_, p2)) -> (Cons(f h1, aux h2, 2 ))
    with Empty                               -> (Cons(f h1, fn, p1)) in
    aux h p

The second one gives the error below; no surprise.

Error: This definition has type 'b. ('b -> 'b) -> 'b t -> 'b t
       which is less general than 'a 'b. ('a -> 'b) -> 'a t -> 'b t

Why is the first definition accepted?  

Peter Frey

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

[Jacques Garrigue]

2013/10/25 7:57、Peter Frey <pjfrey@sympatico.ca> のメール：

> Please consider the following two definitions of map which I would have
> considered equal.  
> 
>  exception Empty
> 
>  type 'a t = Cons of 'a * (int -> 'a t) * int
> 
>  let null = Cons( Obj.magic None, (fun _ -> assert false), max_int ) 
> 
>  let map (f: 'a -> 'b) (t: 'a t) : 'b t =
>      if t == null then null else match t with (Cons( h, fn, p )) ->
>      let rec aux h1 p1 =
>      try match fn p1 with (Cons (h2,_, p2)) -> 
>         (Cons(f h1, aux h2, p2 ))
>      with Empty                             -> (Cons(f h1, fn, p1)) in
>      aux h p
> 
>  let map : 'a 'b. ( 'a -> 'b ) -> 'a t -> 'b t = fun f t -> 
>    if t == null then null else match t with (Cons( h, fn, p )) ->
>    let rec aux h1 p1 =
>      try match fn p1 with (Cons (h2,_, p2)) -> (Cons(f h1, aux h2, 2 ))
>    with Empty                               -> (Cons(f h1, fn, p1)) in
>    aux h p
> 
> The second one gives the error below; no surprise.
> 
> Error: This definition has type 'b. ('b -> 'b) -> 'b t -> 'b t
>       which is less general than 'a 'b. ('a -> 'b) -> 'a t -> 'b t
> 
> Why is the first definition accepted?  

Here is the type inferred for the first definition:
val map : ('b -> 'b) -> 'b t -> 'b t = <fun>

As you can see, types for ‘a and ‘b are merged.
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.
In the second example you use an explicit polymorphic type, which does not
allow instantiating ‘a and ‘b, so you get an error.

Jacques Garrigue

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

[Andreas Rossberg]

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

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

[Roberto Di Cosmo]

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                        

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

[Ivan Gotovchits]

Roberto Di Cosmo <roberto@dicosmo.org> writes:

>
> 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.
>

I think that people expect that an expression:

```
  let a : int = b 
```

is a declaration that value `a` has type int (Just like C'ish 
`int a = b;`). But, indeed, it should be understood as a type
constraint. Thus the following, will be readily accepted by the
type checker (because we «constrain» a to be anything):

```
  let a : 'a = 12
```

The root of misunderstanding, I think, lies in that the same syntax is
used for type annotations and value specifications. Consider the
following example:

```
   module T : sig
    val sum: 'a -> 'a -> 'a
   end = struct
    let sum: 'a -> 'a -> 'a = 
        fun x y -> x + y
   end
```

It looks like that the value sum has the same type in the module
specification and in the module implementation. So if compiler accepts
definition, it should accept that it conforms to the specification. 

Indeed, it's rather intuitional - this types do look the same!

So, I think, that it should be clarified by someone, who knows OCaml and
English much better than me, what is the difference between this two
cases. And it would be great if it will be described in the manual,
too. 




-- 
         (__) 
         (oo) 
   /------\/ 
  / |    ||   
 *  /\---/\ 
    ~~   ~~   
...."Have you mooed today?"...

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

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 4488 bytes --]

> So, I think, that it should be clarified by someone, who knows OCaml and
> English much better than me, what is the difference between this two
> cases. And it would be great if it will be described in the manual,
>
too.
>

Oh, it is described in the manual:
  http://caml.inria.fr/pub/docs/manual-ocaml-4.01/types.html#typexpr

  In type constraints, [type variables] represent unspecified types
  that can be instantiated by any type to satisfy the type constraint.

The problem is that most people expecting "let x : 'a = 12" to fail did not
(and often will never) read that manual section. Documenting is enough when
people notice they don't know something (and look for the answer). It
doesn't work very well when people guess what something is (so they don't
feel a need to look it up), but consistently guess wrong.

I agree with Andreas that the current situation is unsatisfying, and that
his proposed change would be a net improvement. Roberto says that we should
teach the stuff better, but our constantly-repeated experience is that
people consistently *guess* that type annotations enforce polymorphism --
before seeking for help from teachers on that point. As to why this happen,
I'm not sure (but I don't think we need to have the cause to agree that the
issue requires a change), but I would hazard Ivan's explanation that they
expect that from the meaning of type variables in type signatures, either
inferred in the toplevel or explicitly written in .mli. After all, most
OCaml programs have so few type annotations that people only encounter type
variables in those type signatures. The suggestion to use '_a for flexible
variables seems reasonable.

However, I think that the current syntax of implicitly-introduced variables
with heuristically-defined scoping rules is bad in any case. My own toy
experiment with explicit syntaxes always use an explicit binding syntax for
both rigid and flexible variables (eg. "forall a b c in ..." and "some a b
c in ..."). In this regard, the ('a 'b . ty) or (type a) syntaxes are
definite improvements -- if only we had applied those explicit binding
forms to GADT constructor types as well... So I think that even with
Andreas' proposed change, people would still be surprised by things like
the following:

  let id : 'a -> 'a = fun x -> x

  let dup (x : 'a) ('a * 'a) =
    let result = (x, x) in
    (id : 'a -> 'a) result  (* fails, while (id : 'b -> 'b) works *)


On Fri, Oct 25, 2013 at 11:59 AM, Ivan Gotovchits <ivg@ieee.org> wrote:

> Roberto Di Cosmo <roberto@dicosmo.org> writes:
>
> >
> > 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.
> >
>
> I think that people expect that an expression:
>
> ```
>   let a : int = b
> ```
>
> is a declaration that value `a` has type int (Just like C'ish
> `int a = b;`). But, indeed, it should be understood as a type
> constraint. Thus the following, will be readily accepted by the
> type checker (because we «constrain» a to be anything):
>
> ```
>   let a : 'a = 12
> ```
>
> The root of misunderstanding, I think, lies in that the same syntax is
> used for type annotations and value specifications. Consider the
> following example:
>
> ```
>    module T : sig
>     val sum: 'a -> 'a -> 'a
>    end = struct
>     let sum: 'a -> 'a -> 'a =
>         fun x y -> x + y
>    end
> ```
>
> It looks like that the value sum has the same type in the module
> specification and in the module implementation. So if compiler accepts
> definition, it should accept that it conforms to the specification.
>
> Indeed, it's rather intuitional - this types do look the same!
>
> So, I think, that it should be clarified by someone, who knows OCaml and
> English much better than me, what is the difference between this two
> cases. And it would be great if it will be described in the manual,
> too.
>
>
>
>
> --
>          (__)
>          (oo)
>    /------\/
>   / |    ||
>  *  /\---/\
>     ~~   ~~
> ...."Have you mooed today?"...
>
> --
> 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
>

[-- Attachment #2: Type: text/html, Size: 6019 bytes --]

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

[Andreas Rossberg]

On 10/25/2013 01:09 PM, Gabriel Scherer wrote:
> However, I think that the current syntax of implicitly-introduced
> variables with heuristically-defined scoping rules is bad in any case.
> My own toy experiment with explicit syntaxes always use an explicit
> binding syntax for both rigid and flexible variables (eg. "forall a b c
> in ..." and "some a b c in ..."). In this regard, the ('a 'b . ty) or
> (type a) syntaxes are definite improvements -- if only we had applied
> those explicit binding forms to GADT constructor types as well... So I
> think that even with Andreas' proposed change, people would still be
> surprised by things like the following:
>
>    let id : 'a -> 'a = fun x -> x
>
>    let dup (x : 'a) ('a * 'a) =
>      let result = (x, x) in
>      (id : 'a -> 'a) result  (* fails, while (id : 'b -> 'b) works *)

Yes, I agree that implicit scoping is a bit of an ugly hack. That said, 
I don't expect anybody to be truly surprised about the example above. At 
least I never heard this being an issue for SML programmers. People 
probably hardly ever write anything like the above, or avoid shadowing 
for clarity anyway.

/Andreas

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

[Yaron Minsky]

Changing the semantics of this will, I think, break a _lot_ of code.
I for one am not excited to do so.

For what it's worth, I suspect that most people who are surprised by
this are people who were trained on Standard ML.  At Jane Street we've
had a lot of people learn the language, and the complaints I've heard
about this feature are, I think, mostly from that group.

I also don't find Andreas suggestion particularly intuitive.  I would
have guessed that (x: '_a) would constrain x to be a weakly
polymorphic value, which is at odds with the proposal.

y

On Fri, Oct 25, 2013 at 10:24 AM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> On 10/25/2013 01:09 PM, Gabriel Scherer wrote:
>>
>> However, I think that the current syntax of implicitly-introduced
>> variables with heuristically-defined scoping rules is bad in any case.
>> My own toy experiment with explicit syntaxes always use an explicit
>> binding syntax for both rigid and flexible variables (eg. "forall a b c
>> in ..." and "some a b c in ..."). In this regard, the ('a 'b . ty) or
>> (type a) syntaxes are definite improvements -- if only we had applied
>> those explicit binding forms to GADT constructor types as well... So I
>> think that even with Andreas' proposed change, people would still be
>> surprised by things like the following:
>>
>>    let id : 'a -> 'a = fun x -> x
>>
>>    let dup (x : 'a) ('a * 'a) =
>>      let result = (x, x) in
>>      (id : 'a -> 'a) result  (* fails, while (id : 'b -> 'b) works *)
>
>
> Yes, I agree that implicit scoping is a bit of an ugly hack. That said, I
> don't expect anybody to be truly surprised about the example above. At least
> I never heard this being an issue for SML programmers. People probably
> hardly ever write anything like the above, or avoid shadowing for clarity
> anyway.
>
> /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

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

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 2586 bytes --]

I'm surprised noone has pointed out the new type annotation syntax:

let id : type s. s -> s = fun x -> x


On Fri, Oct 25, 2013 at 4:32 PM, Yaron Minsky <yminsky@janestreet.com>wrote:

> Changing the semantics of this will, I think, break a _lot_ of code.
> I for one am not excited to do so.
>
> For what it's worth, I suspect that most people who are surprised by
> this are people who were trained on Standard ML.  At Jane Street we've
> had a lot of people learn the language, and the complaints I've heard
> about this feature are, I think, mostly from that group.
>
> I also don't find Andreas suggestion particularly intuitive.  I would
> have guessed that (x: '_a) would constrain x to be a weakly
> polymorphic value, which is at odds with the proposal.
>
> y
>
> On Fri, Oct 25, 2013 at 10:24 AM, Andreas Rossberg <rossberg@mpi-sws.org>
> wrote:
> > On 10/25/2013 01:09 PM, Gabriel Scherer wrote:
> >>
> >> However, I think that the current syntax of implicitly-introduced
> >> variables with heuristically-defined scoping rules is bad in any case.
> >> My own toy experiment with explicit syntaxes always use an explicit
> >> binding syntax for both rigid and flexible variables (eg. "forall a b c
> >> in ..." and "some a b c in ..."). In this regard, the ('a 'b . ty) or
> >> (type a) syntaxes are definite improvements -- if only we had applied
> >> those explicit binding forms to GADT constructor types as well... So I
> >> think that even with Andreas' proposed change, people would still be
> >> surprised by things like the following:
> >>
> >>    let id : 'a -> 'a = fun x -> x
> >>
> >>    let dup (x : 'a) ('a * 'a) =
> >>      let result = (x, x) in
> >>      (id : 'a -> 'a) result  (* fails, while (id : 'b -> 'b) works *)
> >
> >
> > Yes, I agree that implicit scoping is a bit of an ugly hack. That said, I
> > don't expect anybody to be truly surprised about the example above. At
> least
> > I never heard this being an issue for SML programmers. People probably
> > hardly ever write anything like the above, or avoid shadowing for clarity
> > anyway.
> >
> > /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
>
> --
> 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
>

[-- Attachment #2: Type: text/html, Size: 3930 bytes --]

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

[Norman Hardy]

[-- Attachment #1: Type: text/plain, Size: 468 bytes --]


On 2013 Oct 25, at 13:44 , Jacques Le Normand <rathereasy@gmail.com> wrote:

> I'm surprised noone has pointed out the new type annotation syntax:
> 
> let id : type s. s -> s = fun x -> x
> 

I like that syntax, I think.
I suppose that "id : type s. s -> s = fun x -> x" is a let-binding
and that "id : type s. s -> s" is a pattern,
but I cannot get the syntax at http://caml.inria.fr/pub/docs/manual-ocaml/patterns.html
to produce "id : type s. s -> s”.

[-- Attachment #2: Type: text/html, Size: 1426 bytes --]

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

[Jacques Garrigue]

[-- Attachment #1: Type: text/plain, Size: 763 bytes --]

Both explicit polymorphic annotations and the polymorphic syntax of locally
abstract types are extensions.
http://caml.inria.fr/pub/docs/manual-ocaml/extn.html
See subsections 7.12 and 7.13.

Jacques Garrigue
2013/10/26 10:09 "Norman Hardy" <norm@cap-lore.com>:

>
> On 2013 Oct 25, at 13:44 , Jacques Le Normand <rathereasy@gmail.com>
> wrote:
>
> I'm surprised noone has pointed out the new type annotation syntax:
>
> let id : type s. s -> s = fun x -> x
>
>
> I like that syntax, I think.
> I suppose that "id : type s. s -> s = fun x -> x" is a let-binding
> and that "id : type s. s -> s" is a pattern,
> but I cannot get the syntax at
> http://caml.inria.fr/pub/docs/manual-ocaml/patterns.html
> to produce "id : type s. s -> s”.
>

[-- Attachment #2: Type: text/html, Size: 1672 bytes --]

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

[Andreas Rossberg]

On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com> wrote:
> Changing the semantics of this will, I think, break a _lot_ of code.

Interesting. Do you have specific examples in mind?

> For what it's worth, I suspect that most people who are surprised by
> this are people who were trained on Standard ML.  At Jane Street we've
> had a lot of people learn the language, and the complaints I've heard
> about this feature are, I think, mostly from that group.

Maybe, but it's not my impression that this is true for most people I see asking related questions here on the list or on SO.

> I also don't find Andreas suggestion particularly intuitive.  I would
> have guessed that (x: '_a) would constrain x to be a weakly
> polymorphic value, which is at odds with the proposal.

Now, _that_ is something I would only expect from programmers trained on SML -- ancient SML'90 to be precise. ;)

Note how OCaml already uses '_a for a sort of flexible variable in its output.

/Andreas

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

[Yaron Minsky]

On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com> wrote:
>> Changing the semantics of this will, I think, break a _lot_ of code.
>
> Interesting. Do you have specific examples in mind?

I know that I've seen many examples come up in my code.  One common
use is to partially specify a type.  For example, if I wanted to
ignore a return value that is a Tcp.Server.t from Async, I would
probably write it like this:

    (ignore server : ('a,'b) Tcp.Server.t)

without specifying the sometimes rather complicated details of those
types.  Similarly, if I were to ignore a Map, I might write

    (ignore map : (int,string,'a) Map.t

since it's not helpful here to specify the comparator type, which is
what goes into the third slot here.

Nowadays, I would probably use an underscore in these cases rather
than an explicit type variable, but our codebase has plenty of old
examples of this kind of thing.  If a change like the one you propose
is changed, I presume that _ would keep its current meeting, which
would address many use cases.

Given the existence of such use-cases, I would hope that we could
avoid making the change in a way that would non-optionally break lots
of code.  If people agree this change should be made, perhaps it
should be done in the mode of -strict-sequence.  That change was added
as a flag, so users could take it at their own pace.

>> For what it's worth, I suspect that most people who are surprised by
>> this are people who were trained on Standard ML.  At Jane Street we've
>> had a lot of people learn the language, and the complaints I've heard
>> about this feature are, I think, mostly from that group.
>
> Maybe, but it's not my impression that this is true for most people I see asking related questions here on the list or on SO.

To be clear, my guess above is less than scientific.

>> I also don't find Andreas suggestion particularly intuitive.  I would
>> have guessed that (x: '_a) would constrain x to be a weakly
>> polymorphic value, which is at odds with the proposal.
>
> Now, _that_ is something I would only expect from programmers trained on SML -- ancient SML'90 to be precise. ;)
>
> Note how OCaml already uses '_a for a sort of flexible variable in its output.

Where?

> /Andreas
>

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

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 3026 bytes --]

> > Note how OCaml already uses '_a for a sort of flexible variable in its
output.
> Where?

'_a is used for type variables that cannot be generalized.

# let x = ref None;;
val x : '_a option ref = {contents = None}
# let id x = x in id id;;
- : '_a -> '_a = <fun>



On Sun, Oct 27, 2013 at 1:56 PM, Yaron Minsky <yminsky@janestreet.com>wrote:

> On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg <rossberg@mpi-sws.org>
> wrote:
> > On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com> wrote:
> >> Changing the semantics of this will, I think, break a _lot_ of code.
> >
> > Interesting. Do you have specific examples in mind?
>
> I know that I've seen many examples come up in my code.  One common
> use is to partially specify a type.  For example, if I wanted to
> ignore a return value that is a Tcp.Server.t from Async, I would
> probably write it like this:
>
>     (ignore server : ('a,'b) Tcp.Server.t)
>
> without specifying the sometimes rather complicated details of those
> types.  Similarly, if I were to ignore a Map, I might write
>
>     (ignore map : (int,string,'a) Map.t
>
> since it's not helpful here to specify the comparator type, which is
> what goes into the third slot here.
>
> Nowadays, I would probably use an underscore in these cases rather
> than an explicit type variable, but our codebase has plenty of old
> examples of this kind of thing.  If a change like the one you propose
> is changed, I presume that _ would keep its current meeting, which
> would address many use cases.
>
> Given the existence of such use-cases, I would hope that we could
> avoid making the change in a way that would non-optionally break lots
> of code.  If people agree this change should be made, perhaps it
> should be done in the mode of -strict-sequence.  That change was added
> as a flag, so users could take it at their own pace.
>
> >> For what it's worth, I suspect that most people who are surprised by
> >> this are people who were trained on Standard ML.  At Jane Street we've
> >> had a lot of people learn the language, and the complaints I've heard
> >> about this feature are, I think, mostly from that group.
> >
> > Maybe, but it's not my impression that this is true for most people I
> see asking related questions here on the list or on SO.
>
> To be clear, my guess above is less than scientific.
>
> >> I also don't find Andreas suggestion particularly intuitive.  I would
> >> have guessed that (x: '_a) would constrain x to be a weakly
> >> polymorphic value, which is at odds with the proposal.
> >
> > Now, _that_ is something I would only expect from programmers trained on
> SML -- ancient SML'90 to be precise. ;)
> >
> > Note how OCaml already uses '_a for a sort of flexible variable in its
> output.
>
> Where?
>
> > /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
>

[-- Attachment #2: Type: text/html, Size: 4176 bytes --]

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

[Yaron Minsky]

But isn't this the exact opposite of Andreas' proposal?  He was
proposing using '_a as a unification variable, which may very well be
generalized.  It is exactly this use case for '_a that seems at odds
with Andreas' proposal.

y

On Sun, Oct 27, 2013 at 10:28 AM, Gabriel Scherer
<gabriel.scherer@gmail.com> wrote:
>> > Note how OCaml already uses '_a for a sort of flexible variable in its
>> > output.
>> Where?
>
> '_a is used for type variables that cannot be generalized.
>
> # let x = ref None;;
> val x : '_a option ref = {contents = None}
> # let id x = x in id id;;
> - : '_a -> '_a = <fun>
>
>
>
> On Sun, Oct 27, 2013 at 1:56 PM, Yaron Minsky <yminsky@janestreet.com>
> wrote:
>>
>> On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg <rossberg@mpi-sws.org>
>> wrote:
>> > On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com> wrote:
>> >> Changing the semantics of this will, I think, break a _lot_ of code.
>> >
>> > Interesting. Do you have specific examples in mind?
>>
>> I know that I've seen many examples come up in my code.  One common
>> use is to partially specify a type.  For example, if I wanted to
>> ignore a return value that is a Tcp.Server.t from Async, I would
>> probably write it like this:
>>
>>     (ignore server : ('a,'b) Tcp.Server.t)
>>
>> without specifying the sometimes rather complicated details of those
>> types.  Similarly, if I were to ignore a Map, I might write
>>
>>     (ignore map : (int,string,'a) Map.t
>>
>> since it's not helpful here to specify the comparator type, which is
>> what goes into the third slot here.
>>
>> Nowadays, I would probably use an underscore in these cases rather
>> than an explicit type variable, but our codebase has plenty of old
>> examples of this kind of thing.  If a change like the one you propose
>> is changed, I presume that _ would keep its current meeting, which
>> would address many use cases.
>>
>> Given the existence of such use-cases, I would hope that we could
>> avoid making the change in a way that would non-optionally break lots
>> of code.  If people agree this change should be made, perhaps it
>> should be done in the mode of -strict-sequence.  That change was added
>> as a flag, so users could take it at their own pace.
>>
>> >> For what it's worth, I suspect that most people who are surprised by
>> >> this are people who were trained on Standard ML.  At Jane Street we've
>> >> had a lot of people learn the language, and the complaints I've heard
>> >> about this feature are, I think, mostly from that group.
>> >
>> > Maybe, but it's not my impression that this is true for most people I
>> > see asking related questions here on the list or on SO.
>>
>> To be clear, my guess above is less than scientific.
>>
>> >> I also don't find Andreas suggestion particularly intuitive.  I would
>> >> have guessed that (x: '_a) would constrain x to be a weakly
>> >> polymorphic value, which is at odds with the proposal.
>> >
>> > Now, _that_ is something I would only expect from programmers trained on
>> > SML -- ancient SML'90 to be precise. ;)
>> >
>> > Note how OCaml already uses '_a for a sort of flexible variable in its
>> > output.
>>
>> Where?
>>
>> > /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
>
>

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

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 4762 bytes --]

Today the only time where you see '_a is for variable that did not get
generalized, and as a output of the type inference, never as input. But it
would be consistent to extend their meaning to flexible variables anywhere,
regardless of whether they'll get generalized later.

Andreas' idea is to have '_a meaning "instantiate me with any suitable type
that makes this expression type-check" (including a freshly generalized
variable), and have 'a meaning instead "this type must remain a polymorphic
variable". The interpretation for '_a corresponds to the meaning it has
when printed by the type-checker today -- and the interpretation of 'a
would behave as the (type a) construct does today, minus possibly the
specific GADT interaction.

(One minor difference being that, today, the type-checker is not too
careful about respecting weak variable identity when printing them. The
weak variables appearing in the two phrases I've shown have the same name
'_a, when they in fact denote distinct flexible variables which occur in
the same scope.)




On Sun, Oct 27, 2013 at 3:43 PM, Yaron Minsky <yminsky@janestreet.com>wrote:

> But isn't this the exact opposite of Andreas' proposal?  He was
> proposing using '_a as a unification variable, which may very well be
> generalized.  It is exactly this use case for '_a that seems at odds
> with Andreas' proposal.
>
> y
>
> On Sun, Oct 27, 2013 at 10:28 AM, Gabriel Scherer
> <gabriel.scherer@gmail.com> wrote:
> >> > Note how OCaml already uses '_a for a sort of flexible variable in its
> >> > output.
> >> Where?
> >
> > '_a is used for type variables that cannot be generalized.
> >
> > # let x = ref None;;
> > val x : '_a option ref = {contents = None}
> > # let id x = x in id id;;
> > - : '_a -> '_a = <fun>
> >
> >
> >
> > On Sun, Oct 27, 2013 at 1:56 PM, Yaron Minsky <yminsky@janestreet.com>
> > wrote:
> >>
> >> On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg <rossberg@mpi-sws.org
> >
> >> wrote:
> >> > On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com>
> wrote:
> >> >> Changing the semantics of this will, I think, break a _lot_ of code.
> >> >
> >> > Interesting. Do you have specific examples in mind?
> >>
> >> I know that I've seen many examples come up in my code.  One common
> >> use is to partially specify a type.  For example, if I wanted to
> >> ignore a return value that is a Tcp.Server.t from Async, I would
> >> probably write it like this:
> >>
> >>     (ignore server : ('a,'b) Tcp.Server.t)
> >>
> >> without specifying the sometimes rather complicated details of those
> >> types.  Similarly, if I were to ignore a Map, I might write
> >>
> >>     (ignore map : (int,string,'a) Map.t
> >>
> >> since it's not helpful here to specify the comparator type, which is
> >> what goes into the third slot here.
> >>
> >> Nowadays, I would probably use an underscore in these cases rather
> >> than an explicit type variable, but our codebase has plenty of old
> >> examples of this kind of thing.  If a change like the one you propose
> >> is changed, I presume that _ would keep its current meeting, which
> >> would address many use cases.
> >>
> >> Given the existence of such use-cases, I would hope that we could
> >> avoid making the change in a way that would non-optionally break lots
> >> of code.  If people agree this change should be made, perhaps it
> >> should be done in the mode of -strict-sequence.  That change was added
> >> as a flag, so users could take it at their own pace.
> >>
> >> >> For what it's worth, I suspect that most people who are surprised by
> >> >> this are people who were trained on Standard ML.  At Jane Street
> we've
> >> >> had a lot of people learn the language, and the complaints I've heard
> >> >> about this feature are, I think, mostly from that group.
> >> >
> >> > Maybe, but it's not my impression that this is true for most people I
> >> > see asking related questions here on the list or on SO.
> >>
> >> To be clear, my guess above is less than scientific.
> >>
> >> >> I also don't find Andreas suggestion particularly intuitive.  I would
> >> >> have guessed that (x: '_a) would constrain x to be a weakly
> >> >> polymorphic value, which is at odds with the proposal.
> >> >
> >> > Now, _that_ is something I would only expect from programmers trained
> on
> >> > SML -- ancient SML'90 to be precise. ;)
> >> >
> >> > Note how OCaml already uses '_a for a sort of flexible variable in its
> >> > output.
> >>
> >> Where?
> >>
> >> > /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
> >
> >
>

[-- Attachment #2: Type: text/html, Size: 6691 bytes --]

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

[Yaron Minsky]

I trust you that it's a consistent interpretation, but it still
strikes me as surprising, and I suspect it would be so for new users.
From a user's perspective, you only see '_a now when there a weakly
polymorphic type variable is inferred.  Andreas' proposal is that as
an annotation, this should imply a unification variable, i.e., a
constraint on what can be inferred for that type.  I don't know why
those both count as "flexible variables" (not surprising, since I had
not heard of them before this conversation), but I'm not sure it
matters much.

The new situation seems not a lot clearer than the old, merely moving
around the confusion from one syntax to another.  All told, following
Roberto's observation, I suspect there isn't enough of a win here to
justify changing the meaning of old syntax.

y

On Sun, Oct 27, 2013 at 11:25 AM, Gabriel Scherer
<gabriel.scherer@gmail.com> wrote:
> Today the only time where you see '_a is for variable that did not get
> generalized, and as a output of the type inference, never as input. But it
> would be consistent to extend their meaning to flexible variables anywhere,
> regardless of whether they'll get generalized later.
>
> Andreas' idea is to have '_a meaning "instantiate me with any suitable type
> that makes this expression type-check" (including a freshly generalized
> variable), and have 'a meaning instead "this type must remain a polymorphic
> variable". The interpretation for '_a corresponds to the meaning it has when
> printed by the type-checker today -- and the interpretation of 'a would
> behave as the (type a) construct does today, minus possibly the specific
> GADT interaction.
>
> (One minor difference being that, today, the type-checker is not too careful
> about respecting weak variable identity when printing them. The weak
> variables appearing in the two phrases I've shown have the same name '_a,
> when they in fact denote distinct flexible variables which occur in the same
> scope.)
>
>
>
>
> On Sun, Oct 27, 2013 at 3:43 PM, Yaron Minsky <yminsky@janestreet.com>
> wrote:
>>
>> But isn't this the exact opposite of Andreas' proposal?  He was
>> proposing using '_a as a unification variable, which may very well be
>> generalized.  It is exactly this use case for '_a that seems at odds
>> with Andreas' proposal.
>>
>> y
>>
>> On Sun, Oct 27, 2013 at 10:28 AM, Gabriel Scherer
>> <gabriel.scherer@gmail.com> wrote:
>> >> > Note how OCaml already uses '_a for a sort of flexible variable in
>> >> > its
>> >> > output.
>> >> Where?
>> >
>> > '_a is used for type variables that cannot be generalized.
>> >
>> > # let x = ref None;;
>> > val x : '_a option ref = {contents = None}
>> > # let id x = x in id id;;
>> > - : '_a -> '_a = <fun>
>> >
>> >
>> >
>> > On Sun, Oct 27, 2013 at 1:56 PM, Yaron Minsky <yminsky@janestreet.com>
>> > wrote:
>> >>
>> >> On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg
>> >> <rossberg@mpi-sws.org>
>> >> wrote:
>> >> > On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com>
>> >> > wrote:
>> >> >> Changing the semantics of this will, I think, break a _lot_ of code.
>> >> >
>> >> > Interesting. Do you have specific examples in mind?
>> >>
>> >> I know that I've seen many examples come up in my code.  One common
>> >> use is to partially specify a type.  For example, if I wanted to
>> >> ignore a return value that is a Tcp.Server.t from Async, I would
>> >> probably write it like this:
>> >>
>> >>     (ignore server : ('a,'b) Tcp.Server.t)
>> >>
>> >> without specifying the sometimes rather complicated details of those
>> >> types.  Similarly, if I were to ignore a Map, I might write
>> >>
>> >>     (ignore map : (int,string,'a) Map.t
>> >>
>> >> since it's not helpful here to specify the comparator type, which is
>> >> what goes into the third slot here.
>> >>
>> >> Nowadays, I would probably use an underscore in these cases rather
>> >> than an explicit type variable, but our codebase has plenty of old
>> >> examples of this kind of thing.  If a change like the one you propose
>> >> is changed, I presume that _ would keep its current meeting, which
>> >> would address many use cases.
>> >>
>> >> Given the existence of such use-cases, I would hope that we could
>> >> avoid making the change in a way that would non-optionally break lots
>> >> of code.  If people agree this change should be made, perhaps it
>> >> should be done in the mode of -strict-sequence.  That change was added
>> >> as a flag, so users could take it at their own pace.
>> >>
>> >> >> For what it's worth, I suspect that most people who are surprised by
>> >> >> this are people who were trained on Standard ML.  At Jane Street
>> >> >> we've
>> >> >> had a lot of people learn the language, and the complaints I've
>> >> >> heard
>> >> >> about this feature are, I think, mostly from that group.
>> >> >
>> >> > Maybe, but it's not my impression that this is true for most people I
>> >> > see asking related questions here on the list or on SO.
>> >>
>> >> To be clear, my guess above is less than scientific.
>> >>
>> >> >> I also don't find Andreas suggestion particularly intuitive.  I
>> >> >> would
>> >> >> have guessed that (x: '_a) would constrain x to be a weakly
>> >> >> polymorphic value, which is at odds with the proposal.
>> >> >
>> >> > Now, _that_ is something I would only expect from programmers trained
>> >> > on
>> >> > SML -- ancient SML'90 to be precise. ;)
>> >> >
>> >> > Note how OCaml already uses '_a for a sort of flexible variable in
>> >> > its
>> >> > output.
>> >>
>> >> Where?
>> >>
>> >> > /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
>> >
>> >
>
>

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

[Roberto Di Cosmo]

Thanks Ivan,
       the potential confusion between type annotations
in the code and type specifications in module interfaces
is a very good point.

Writing

 let f : 'a -> 'a = fun x -> x+1 

will just boil down to defining 

 val f : int -> int = <fun>

On the other side, declaring 

 val f : 'a -> 'a 

in a module signature actually *requires* the implementation
to be at least as generic as 'a -> 'a, so a definition
let f = fun x -> x+1 in the body will not work.

Nevertheless, I would say that the difference is pretty
easy to grasp, as soon as one explains that specifications
are only introduced in modules signatures, with the val
keyword.

One may want to introduce type specifications in the code
like in Haskell, but I am not sure that il will be much
better for newbies... : let's write some code similar
to the above one

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?

--
Roberto

 

On Fri, Oct 25, 2013 at 01:59:26PM +0400, Ivan Gotovchits wrote:
> Roberto Di Cosmo <roberto@dicosmo.org> writes:
> 
> >
> > 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.
> >
> 
> I think that people expect that an expression:
> 
> ```
>   let a : int = b 
> ```
> 
> is a declaration that value `a` has type int (Just like C'ish 
> `int a = b;`). But, indeed, it should be understood as a type
> constraint. Thus the following, will be readily accepted by the
> type checker (because we «constrain» a to be anything):
> 
> ```
>   let a : 'a = 12
> ```
> 
> The root of misunderstanding, I think, lies in that the same syntax is
> used for type annotations and value specifications. Consider the
> following example:
> 
> ```
>    module T : sig
>     val sum: 'a -> 'a -> 'a
>    end = struct
>     let sum: 'a -> 'a -> 'a = 
>         fun x y -> x + y
>    end
> ```
> 
> It looks like that the value sum has the same type in the module
> specification and in the module implementation. So if compiler accepts
> definition, it should accept that it conforms to the specification. 
> 
> Indeed, it's rather intuitional - this types do look the same!
> 
> So, I think, that it should be clarified by someone, who knows OCaml and
> English much better than me, what is the difference between this two
> cases. And it would be great if it will be described in the manual,
> too. 
> 
> 
> 
> 
> -- 
>          (__) 
>          (oo) 
>    /------\/ 
>   / |    ||   
>  *  /\---/\ 
>     ~~   ~~   
> ...."Have you mooed today?"...

-- 
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                        

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

[Jonathan Protzenko]

On 10/25/2013 02:35 PM, Roberto Di Cosmo wrote:
> Thanks Ivan,
>        the potential confusion between type annotations
> in the code and type specifications in module interfaces
> is a very good point.
>
> Writing
>
>  let f : 'a -> 'a = fun x -> x+1 
>
> will just boil down to defining 
>
>  val f : int -> int = <fun>
>
> On the other side, declaring 
>
>  val f : 'a -> 'a 
>
> in a module signature actually *requires* the implementation
> to be at least as generic as 'a -> 'a, so a definition
> let f = fun x -> x+1 in the body will not work.
You should also remember that the top-level, which is what most
beginners use, also favors the confusion.

# let f x = x;;
val f : 'a -> 'a = <fun>
# let f : 'a -> 'a = fun x -> x + 1;;
val f : int -> int = <fun>

What OCaml is actually telling you is: "this function has type 'a -> 'a,
but if you write 'a -> 'a yourself, I'm going to give it a totally
different meaning".

~ jonathan

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

[Roberto Di Cosmo]

Hi Jonathan,
   I beg to disagree

On Fri, Oct 25, 2013 at 02:45:52PM +0200, Jonathan Protzenko wrote:
> You should also remember that the top-level, which is what most
> beginners use, also favors the confusion.
> 
> # let f x = x;;
> val f : 'a -> 'a = <fun>

OCaml is telling you: hey, your code is so generic that I can give it
the type 'a -> 'a, you got a polymorphic function!

> # let f : 'a -> 'a = fun x -> x + 1;;
> val f : int -> int = <fun>
> 

Here you are telling OCaml: 
 look, I'd like to see f as having type 'a -> 'a, what do you think?

And OCaml tells you: sorry sir, the best I can give you is int -> int

> What OCaml is actually telling you is: "this function has type 'a -> 'a,
> but if you write 'a -> 'a yourself, I'm going to give it a totally
> different meaning".
> 
> ~ jonathan

The point on which I agree is that if we leave these annotations in
the code, they may end up being read as specifications by whomever
looks at the sources alone, and this may lead to confusion.

But to spot such issues we do not need to change the syntax and semantics of 
type annotations, it would be enough to have yet another warning
that informs us that the type annotations have been instanciated...
something like

# let f : 'a -> 'a = fun x -> x + 1;;
           _______
Warning 66: the user provided type constraint is too general:
variable 'a has been instanciated to type int
val f : int -> int = <fun>

--
Roberto

P.S.: I will not feed the troll any longer though, time to
get back to work :-)

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

[Andreas Rossberg]

On 10/25/2013 10:29 AM, Roberto Di Cosmo wrote:
>       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.

I believe you are mistaken. At least in Standard ML, explicit type 
variables have always been interpreted as quantified variables, not 
unification variables. If you try to write

   fun f(x : 'a) = x + 1

or

   fun g(x : 'a) = x : 'b

that's an error.


> 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).

Aren't you conflating two different universes here? Namely, the 
declarative type system and the type inference algorithm? The ML type 
system semantics as such, at least in most formalisations I can 
remember, knows nothing about unification variables -- that's an 
implementation detail of algorithm W. And the user interface of a 
language is the declarative system, not the underlying implementation. 
Making unification variables user-visible is an extension to the basic 
ML type system that I have rarely seen made precise (I seem to remember 
that the Didiers did that in the context of MLF).

/Andreas

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

[oleg]

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).

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

[Didier Remy]

> 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.

Indeed, both forms are useful, since in a system that does type inferenece I
may wish to specify part of the annotations but not all of it.  Rigid
variables will make the type checker complain if the inferred type is weaker
than what I expected and flexible variables allow me to omit parts of types
that I don't care about or just say that two parts of a type should be the
same without caring what these parts exactly are.

    For example, one should be able to express annotations of the form:

        for all 'a, 'b, for some 'u, ('a -> 'b) -> 'a * 'u -> 'b * 'u

    where 'u, 'v are flexible but 'a, 'b are rigid.

    Bindings should not just be in a single type annotations but in programs,
    so that two arguments can for instance be requested to have the same type.

        let g =
            let f (for some 'a) (x : 'a) (y : 'a) = ... in
        in ...

    Notice, that the inner binding has a limited scope,  which allows
    variables that will appear in the type inferred for 'a to be generalized
    in the type of f.

In fact, now that existential variables have been introduced in the
language, via local modules or gadts, there are three kinds of bindings:
rigid (universal or existential) and flexible variables. Even though
universal and existential are treated in the same way as rigid variables
which cannot be instantiated, their meaning is different and we should
probaly reflect this by a syntactic difference.

Hence, a good design (if we were to redo it from scratch) should require the
user to always explicitly bind type variables, forcing him to say how and
were there are bound.

     Didier

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

[Didier Remy]

>> 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).

> Aren't you conflating two different universes here? Namely, the
> declarative type system and the type inference algorithm? The ML type
> system semantics as such, at least in most formalisations I can remember,
> knows nothing about unification variables -- that's an implementation
> detail of algorithm W. And the user interface of a language is the
> declarative system, not the underlying implementation. Making unification
> variables user-visible is an extension to the basic ML type system that I
> have rarely seen made precise

Andreas, I am not sure what point you are trying to make.

Sure, the name "unification variable" is misleading and should not be used
here, as it refers to the algorithm. Instead, one should call them flexible
type variable or whatever that refers to the specification.

Still, flexible variables make a lot of sense in the specification (even
if not often done in formal presentations).

A language that does type inference should allow the user to say that two
arguments have the same type without telling what these types are, using a
flexible type variable.  (It should also allow the user to tell the type
checker that some expression whould have exactly this type scheme, using a
rigid type variable.

For this reason, the language should expose to the user the both notions of
rigid and flexible bindings.

One can easily specify the introduction of a flexible variable 'a in some
program M as the following typing rule and without reference to the
implementation:

                           G |- M ['a <- t] : s
                           -----------------------
                           G |- for some 'a. M : s

François and I discuss this and formalize it in our chapter "The Essence of
ML Type Inference" in "Advanced Topics in Types and Programming".

----------------

> (I seem to remember that the Didiers did that in the context of MLF).

Yes, since we needed more annotations in MLF because all function paramters
that are used polymorphically must be annotated, we wanted to be able to
only annoatte specify parts of the parameter that had to be used
polymorphically.  We could give type annotations of the form:

         for some 'u, for all 'a, 'b, ('a -> 'b) -> 'a * 'u -> 'b * 'v

When used as the annotation of a function parameter, 'u could be freely
instantiated, even to a polymorphic type, as long as this part of the
argument was not used polymorphically.

We found this necessary in MLF, but it would also be quite useful in OCaml.

         Didier

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

[Andreas Rossberg]

On Oct 26, 2013, at 19:32 , Didier Remy <Didier.Remy@inria.fr> wrote:
>>> 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).
> 
>> Aren't you conflating two different universes here? Namely, the
>> declarative type system and the type inference algorithm? The ML type
>> system semantics as such, at least in most formalisations I can remember,
>> knows nothing about unification variables -- that's an implementation
>> detail of algorithm W. And the user interface of a language is the
>> declarative system, not the underlying implementation. Making unification
>> variables user-visible is an extension to the basic ML type system that I
>> have rarely seen made precise
> 
> Andreas, I am not sure what point you are trying to make.
> 
> Sure, the name "unification variable" is misleading and should not be used
> here, as it refers to the algorithm. Instead, one should call them flexible
> type variable or whatever that refers to the specification.
> 
> Still, flexible variables make a lot of sense in the specification (even
> if not often done in formal presentations).

Oh, I agree. I was merely questioning that all explicit type variables in ML would naturally be flexible variables, which was what I was reading into Roberto's reply (if you take the preceding paragraph from his post as context). Sure, flexible variables are easy (and useful) to add, but technically speaking they are an extension, i.e., require extra rules. Or would you not say so?

And yes, I want to have both forms of variables/bindings, as I suggested in my original post. My main concern with the current state of affairs in OCaml is that implicitly interpreting 'a as the flexible kind obviously is surprising to many people, arguably because it is somewhat inconsistent. Especially when rigid probably is the more common use case.


> One can easily specify the introduction of a flexible variable 'a in some
> program M as the following typing rule and without reference to the
> implementation:
> 
>                          G |- M ['a <- t] : s
>                          -----------------------
>                          G |- for some 'a. M : s
> 
> François and I discuss this and formalize it in our chapter "The Essence of
> ML Type Inference" in "Advanced Topics in Types and Programming".

Ah, yes, thanks for the reminder.


>> (I seem to remember that the Didiers did that in the context of MLF).
> 
> Yes, since we needed more annotations in MLF because all function paramters
> that are used polymorphically must be annotated, we wanted to be able to
> only annoatte specify parts of the parameter that had to be used
> polymorphically.  We could give type annotations of the form:
> 
>        for some 'u, for all 'a, 'b, ('a -> 'b) -> 'a * 'u -> 'b * 'v
> 
> When used as the annotation of a function parameter, 'u could be freely
> instantiated, even to a polymorphic type, as long as this part of the
> argument was not used polymorphically.
> 
> We found this necessary in MLF, but it would also be quite useful in OCaml.


Yes, makes sense. I suppose the main obstacle is retrofitting a nice syntax into OCaml.

/Andreas

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

[Roberto Di Cosmo]

Wow, I did not expect to be spawning such a long exchange with my
request of information on what appears surprising in type annotations
as they are used today in OCaml, but all in all, I don't regret it,
as it brought up a lot of useful information, that I'll refrain from
summarising here: I just want to thank sincerely everybody for all the
comments, as I actually ended up learning a lot here, and I believe
I am not alone.

Let me offer, though, a general comment which goes beyond the specific scope of
this thread: of course incompatible changes to a language can be done, and
have been regularly done in the past of our preferred language, with the
wonderful CamlLight/CSL/OCaml team providing auto-magic converters that
reduced somehow the pain of the transition.

But I believe that such changes should only be made after a very careful
and thorough consideration of their advantages and impact: it cannot just
be motivated by the fact that a part of the user community finds a certain
notation more or less intuitive than another, as another part of the
community may feel exactly the opposite.

-- 
Roberto
 
------------------------------------------------------------------
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                        

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

[Jacques Garrigue]

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
>