From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id B185A7EE25 for ; Fri, 25 Oct 2013 13:10:27 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=74.125.83.41; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 74.125.83.41 as permitted sender) identity=mailfrom; client-ip=74.125.83.41; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ee0-f41.google.com) identity=helo; client-ip=74.125.83.41; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ee0-f41.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjIDAG1QalJKfVMplWdsb2JhbABZgz9Uq2iKGIhKgRkIFg4BAQEBBw0JCRIqgiUBAQQBJxkBGxILAQMBCwYFCwMXISIBEQEFAQoSBhMICodiAQMJBg2afoxWgwqEKwoZJwMKZIkBAQUMjz0EB4QsA5gKgS+ObBgphFE6 X-IPAS-Result: AjIDAG1QalJKfVMplWdsb2JhbABZgz9Uq2iKGIhKgRkIFg4BAQEBBw0JCRIqgiUBAQQBJxkBGxILAQMBCwYFCwMXISIBEQEFAQoSBhMICodiAQMJBg2afoxWgwqEKwoZJwMKZIkBAQUMjz0EB4QsA5gKgS+ObBgphFE6 X-IronPort-AV: E=Sophos;i="4.93,569,1378850400"; d="scan'208";a="31857662" Received: from mail-ee0-f41.google.com ([74.125.83.41]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Oct 2013 13:10:26 +0200 Received: by mail-ee0-f41.google.com with SMTP id d49so1878750eek.14 for ; Fri, 25 Oct 2013 04:10:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=wEm0QAOVRPCbuIXKws/4rDjRa4K4qxvyKCQlfsCfYtg=; b=ay82BHmGac+3hvtHaIzE86v6b1EcWITsi+/xumYokNS15ak5qMOYajKsLeWxt3qgLE upIraEewIAcFEQay+3wiR+p1cRt4OYNRlFu8XPN6akmjmn+M44sN68I/v8mT4dUrD49g oa8s8SPRtlpImsCVG8ZZk8WKydaIm8udEocT0CLsPnkWhhU4Lr91UaBWrlMHuFm12nv0 MioOFOsP1faqXB7sm13ryJM71qyj3QezmrYd5jOw9rbB+htQE8D8bW/cwzniT8J9eUNg E/7sLCouHH4BhzS8c1B1kvkB335upe3THQqEVdEH0VUdrEVqpfR8OhYH3MsFFYs/i3l0 wwbA== X-Received: by 10.204.63.7 with SMTP id z7mr6929bkh.23.1382699426135; Fri, 25 Oct 2013 04:10:26 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.122.72 with HTTP; Fri, 25 Oct 2013 04:09:46 -0700 (PDT) In-Reply-To: <878uxhd62p.fsf@golf.niidar.ru> References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> <878uxhd62p.fsf@golf.niidar.ru> From: Gabriel Scherer Date: Fri, 25 Oct 2013 13:09:46 +0200 Message-ID: To: Ivan Gotovchits Cc: Roberto Di Cosmo , Andreas Rossberg , Jacques Garrigue , OCaML List Mailing Content-Type: multipart/alternative; boundary=001a11c378282071ca04e98ecc4c Subject: Re: [Caml-list] Equality between abstract type definitions --001a11c378282071ca04e98ecc4c Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable > 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 =3D 12" to fail did n= ot (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 =3D fun x -> x let dup (x : 'a) ('a * 'a) =3D let result =3D (x, x) in (id : 'a -> 'a) result (* fails, while (id : 'b -> 'b) works *) On Fri, Oct 25, 2013 at 11:59 AM, Ivan Gotovchits wrote: > Roberto Di Cosmo 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 =3D b > ``` > > is a declaration that value `a` has type int (Just like C'ish > `int a =3D b;`). But, indeed, it should be understood as a type > constraint. Thus the following, will be readily accepted by the > type checker (because we =ABconstrain=BB a to be anything): > > ``` > let a : 'a =3D 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 =3D struct > let sum: 'a -> 'a -> 'a =3D > 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 > --001a11c378282071ca04e98ecc4c Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

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:=
=A0 http://caml.inria.fr/pub/docs/manual-ocaml-4.01/types.html#type= xpr
=A0
=A0 In type constraints, [type variables] represent unspecified types
=A0 that can be instantiated by any type to satisfy the type constraint.

The problem is that most people expecting &qu= ot;let x : 'a =3D 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 w= hen people guess what something is (so they don't feel a need to look i= t up), but consistently guess wrong.

I agree with Andreas that the current situation is unsatisfy= ing, and that his proposed change would be a net improvement. Roberto says = that we should teach the stuff better, but our constantly-repeated experien= ce is that people consistently *guess* that type annotations enforce polymo= rphism -- before seeking for help from teachers on that point. As to why th= is happen, I'm not sure (but I don't think we need to have the caus= e 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 ty= pe signatures, either inferred in the toplevel or explicitly written in .ml= i. After all, most OCaml programs have so few type annotations that people = only encounter type variables in those type signatures. The suggestion to u= se '_a for flexible variables seems reasonable.

However, I think that the current syntax of implicitly-intro= duced variables with heuristically-defined scoping rules is bad in any case= . My own toy experiment with explicit syntaxes always use an explicit bindi= ng syntax for both rigid and flexible variables (eg. "forall a b c in = ..." and "some a b c in ..."). In this regard, the ('a &= #39;b . ty) or (type a) syntaxes are definite improvements -- if only we ha= d 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:

=A0 let id : 'a -> 'a =3D fun x -> x
=

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


On Fri,= Oct 25, 2013 at 11:59 AM, Ivan Gotovchits <ivg@ieee.org> wrote:<= br>
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:

```
=A0 let a : int =3D b
```

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

```
=A0 let a : 'a =3D 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:

```
=A0 =A0module T : sig
=A0 =A0 val sum: 'a -> 'a -> 'a
=A0 =A0end =3D struct
=A0 =A0 let sum: 'a -> 'a -> 'a =3D
=A0 =A0 =A0 =A0 fun x y -> x + y
=A0 =A0end
```

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.




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

--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://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
--001a11c378282071ca04e98ecc4c--