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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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