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 314407EE34 for ; Mon, 28 Mar 2016 10:08:36 +0200 (CEST) IronPort-PHdr: 9a23:SbS1rx87Qi6fL/9uRHKM819IXTAuvvDOBiVQ1KB92+0cTK2v8tzYMVDF4r011RmSDdWdsakP0buM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt6U1Z/8jbHos7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+mgPOQgyV9zM5W2EbmRpBS1zK6Rj+U5zxuwP1s+N83G+ROsigHp4uXjH3wK5hUh7ljG88PD406mzNwph/hahBoR+l4Qd0w4PObZu9O/93f6ebdtQfEzkSFv1NXjBMV9vvJ7AECPAMaKMB99Hw Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-ig0-f174.google.com 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=209.85.213.174; 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 209.85.213.174 as permitted sender) identity=mailfrom; client-ip=209.85.213.174; 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-ig0-f174.google.com) identity=helo; client-ip=209.85.213.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ig0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BVAACo5fhWkq7VVdFbhH4GumYBDYFwhg0CgRcHOBQBAQEBAQEBARABAQEBBwsLCSEvgi2CFAEBAQMBEhEEGQEbHQEDAQsGAwILAwoqAgIhAQERAQUBHAYTIodvAQMKCJJbj0GBMT4xizaBaoJXhg8KGScNUYQdAQEBAQEBBAEBAQEBFQEFCgWGD4REgj6EfoJWBZcwMYFSij+BdY8LhzaGFxEegQ8eAQGCOB6BUzowiFYBAQE X-IPAS-Result: A0BVAACo5fhWkq7VVdFbhH4GumYBDYFwhg0CgRcHOBQBAQEBAQEBARABAQEBBwsLCSEvgi2CFAEBAQMBEhEEGQEbHQEDAQsGAwILAwoqAgIhAQERAQUBHAYTIodvAQMKCJJbj0GBMT4xizaBaoJXhg8KGScNUYQdAQEBAQEBBAEBAQEBFQEFCgWGD4REgj6EfoJWBZcwMYFSij+BdY8LhzaGFxEegQ8eAQGCOB6BUzowiFYBAQE X-IronPort-AV: E=Sophos;i="5.24,405,1454972400"; d="scan'208,217";a="171218691" Received: from mail-ig0-f174.google.com ([209.85.213.174]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 28 Mar 2016 10:08:35 +0200 Received: by mail-ig0-f174.google.com with SMTP id nk17so47539612igb.1 for ; Mon, 28 Mar 2016 01:08:35 -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; bh=okZDtDgAZDAQHX7+rzsBFTdrUFf5kPgGHeIc8vYdKjI=; b=Z1J0qDiqSQ9v3lkJnrD01MEO0JyPNygqpdsx3yqasGkdxD+MYiew/OaETd4UtfJHpj 1EBBfsfjVg8Hd1tN5LR4xkL6n60h80iE30Ia4EJkw9nFm3MDlyvER9CFWqVzKHEDTBSn m6jwhjJkwsFHhJPyZRyAy2+liBsRvkP912kW0p8BU+QWJrc6pTwB+Lw1f21q/Ob8SY07 PDrloCD3i0zzZKM8HCOGULAoqkrn38nHpvYDwEtH53JAyBUecO+BCRYbSOe2SYKtfl9k XonPlz9P/M2AOIn/CKLkKLjcLzRtkSQ6Owd9FXIWzXa3VHuFu0yQBEY7dTA0D+pr46gu WfyA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=okZDtDgAZDAQHX7+rzsBFTdrUFf5kPgGHeIc8vYdKjI=; b=Ixl8u5jd/gBkTargwwtDxtoym2DbepMBVtdGEzTG6fM1ayW/ypQUDRSUocOMhRLm+h 45+x22cmBo2HzpTXvqy5iKkzuT2/z4oGdJXoAqxCFPj7HpMOY9Vbvqt/d9mutJqL7I0d 5TDv3rK+SC/zU7S7915HjhIxcFdCAZUBA5w2Fu9gTv+Iv/P9BT6tfgzpCGbP5FzLvJEE KXwzfYw9qzSvt9TDDmxJWP2ona89Lmu8Qxr9i19jqvmd7R+7DmNmaIJILXeruImA7blN NMlHlXado1i4hGv7NNubB93sc7ZXMe9rdozp2RrcaceduWvJFvSKQfPrrIMaXVzCPn2M 99YA== X-Gm-Message-State: AD7BkJIbU4OAEAkbGL08E3iJudAdjnvIk4UuKDXbThoMetNK0P9DcKpPfwWaujWFjzrmoEQayput612ZAuZ8Mg== X-Received: by 10.50.43.226 with SMTP id z2mr8465996igl.94.1459152514078; Mon, 28 Mar 2016 01:08:34 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.17.4 with HTTP; Mon, 28 Mar 2016 01:07:54 -0700 (PDT) In-Reply-To: References: <86d1qgqu45.fsf@lpw25.net> <2D2C7D68-D59A-407B-B83A-65622DF9CC25@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Mon, 28 Mar 2016 10:07:54 +0200 Message-ID: To: Gregory Malecha Cc: Jacques Garrigue , Mailing List OCaml Content-Type: multipart/alternative; boundary=047d7bfea0f446963a052f176bbf Subject: Re: [Caml-list] "Type constructor b would escape its scope" --047d7bfea0f446963a052f176bbf Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Locally abstract types scope over the definition body where they can be used as type names or to refine GADTs by pattern-matching. module type Ty =3D sig type t end (* we need the scoping of the locally abstract type in this example; note that (type a) would work as well *) let mkTy : type a . unit -> (module Ty with type t =3D a) =3D fun () -> let module T =3D struct type t =3D a end in (module T) > val mkTy : unit -> (module Ty with type t =3D 'a) =3D (* a type variable 'a only scopes over the type annotation *) let mkTy : 'a . unit -> (module Ty with type t =3D 'a) =3D fun () -> let module T =3D struct type t =3D 'a end in (module T) > let module T =3D struct type t =3D 'a end in > ^^ > Error: Unbound type parameter 'a type _ tag =3D Int : int tag | Prod : 'a tag * 'b tag -> ('a * 'b) tag (* we need the ability to be refined by GADT matching here *) let rec default : type a . a tag -> a =3D function | Int -> 0 | Prod (ta, tb) -> (default ta, default tb) > val default : 'a tag -> 'a =3D (* a type variable just unifies with the first case and fails on the second *) let rec default : 'a . 'a tag -> 'a =3D function | Int -> 0 | Prod (ta, tb) -> (default ta, default tb) > ^^^^^^^^^^^^^ > Error: This pattern matches values of type ($0 * $1) tag > but a pattern was expected which matches values of type int tag > Type $0 * $1 is not compatible with type int (* the difference by "(type a) ..." and "type a . ..." is that the latter allows polymorphic recursion (just as "'a . ..."), so this example fails with just (type a) *) let rec default (type a) : a tag -> a =3D function | Int -> 0 | Prod (ta, tb) -> (default ta, default tb) > ^^ > Error: This expression has type $0 tag but an expression > was expected of type 'a > The type constructor $0 would escape its scope On Mon, Mar 28, 2016 at 6:20 AM, Gregory Malecha wrote: > Thanks. I'm not sure I understand the difference between the two though. Is > there an example showing when they produce different results? > > On Sun, Mar 27, 2016 at 6:12 PM, Jacques Garrigue > wrote: >> >> On 2016/03/28 03:52, Gregory Malecha wrote: >> > >> > Thanks, Leo -- >> > >> > This is exactly what I needed to know. I thought that the (type a) >> > annotation was forcing the function to be polymorphic. For future reference, >> > is there any way to write the annotation (that forces the function to be >> > polymorphic) without having to write explicit =E2=80=98fun's? >> >> You should either write >> >> let generic_search_stream : =E2=80=98b. int option -> (internal_result= , =E2=80=98b) >> result_stream =3D =E2=80=A6 >> >> or >> >> let generic_search_stream : type b. int option -> (internal_result, b) >> result_stream =3D =E2=80=A6 >> >> where the latter one both requires polymorphism and defines a locally >> abstract type, >> i.e. probably the behavior you expect with (type b). >> >> Jacques >> > > > > -- > gregory malecha --047d7bfea0f446963a052f176bbf Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Locally abstract types scope over the definition body wher= e they can
be used as type names or to refine GADTs by pattern-matching.=

mo= dule type Ty =3D sig type t end

(* we need the scoping of the locall= y abstract type in this example;
=C2=A0 =C2=A0note that (type a) would w= ork as well *)
let mkTy : type a . unit -> (module Ty with type t =3D= a) =3D
=C2=A0 fun () ->
=C2=A0 =C2=A0 let module T =3D struct typ= e t =3D a end in
=C2=A0 =C2=A0 (module T)

> val mkTy : unit -&= gt; (module Ty with type t =3D 'a) =3D <fun>

(* a type var= iable 'a only scopes over the type annotation *)
let mkTy : 'a .= unit -> (module Ty with type t =3D 'a) =3D
=C2=A0 fun () ->=C2=A0 =C2=A0 let module T =3D struct type t =3D 'a end in
=C2=A0 = =C2=A0 (module T)

> =C2=A0let module T =3D struct type t =3D '= ;a end in
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 ^^
> Error: U= nbound type parameter 'a


type _ tag =3D Int : int tag | Prod= : 'a tag * 'b tag -> ('a * 'b) tag

(* we need th= e ability to be refined by GADT matching here *)
let rec default : type = a . a tag -> a =3D
=C2=A0 function
=C2=A0 | Int -> 0
=C2=A0 = | Prod (ta, tb) -> (default ta, default tb)

> val default : &#= 39;a tag -> 'a =3D <fun>

(* a type variable just unifie= s with the first case and fails on the second *)
let rec default : '= a . 'a tag -> 'a =3D
=C2=A0 function
=C2=A0 | Int -> 0<= br>=C2=A0 | Prod (ta, tb) -> (default ta, default tb)
> =C2=A0 ^^^= ^^^^^^^^^^
> Error: This pattern matches values of type ($0 * $1) tag=
> =C2=A0 =C2=A0 =C2=A0 =C2=A0but a pattern was expected which matche= s values of type int tag
> =C2=A0 =C2=A0 =C2=A0 =C2=A0Type $0 * $1 is= not compatible with type int

(* the difference by "(type a) ..= ." and "type a . ..." is that the latter
=C2=A0 =C2=A0all= ows polymorphic recursion (just as "'a . ..."), so this examp= le fails
=C2=A0 =C2=A0with just (type a) *)
let rec default (type a) = : a tag -> a =3D
=C2=A0 function
=C2=A0 | Int -> 0
=C2=A0 | = Prod (ta, tb) -> (default ta, default tb)
> =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 ^^
> Error: This expression has type $0 tag but an expression
= > was expected of type 'a
> The type constructor $0 would esca= pe its scope

On Mon, Mar 28, 2016 at 6:20 AM, Gregory = Malecha <gmalecha@gmail.com>= ; wrote:
> Thanks. I'm not sure I understand the difference betwe= en the two though. Is
> there an example showing when they produce di= fferent results?
>
> On Sun, Mar 27, 2016 at 6:12 PM, Jacques G= arrigue
> <garrigu= e@math.nagoya-u.ac.jp> wrote:
>>
>> On 2016/03/28 = 03:52, Gregory Malecha wrote:
>> >
>> > Thanks, Leo= --
>> >
>> > This is exactly what I needed to know= . I thought that the (type a)
>> > annotation was forcing the f= unction to be polymorphic. For future reference,
>> > is there = any way to write the annotation (that forces the function to be
>>= > polymorphic) without having to write explicit =E2=80=98fun's?
= >>
>> You should either write
>>
>> =C2=A0= let generic_search_stream : =E2=80=98b. int option -> (internal_result,= =E2=80=98b)
>> result_stream =3D =E2=80=A6
>>
>>= ; or
>>
>> =C2=A0 let generic_search_stream : type b. int= option -> (internal_result, b)
>> result_stream =3D =E2=80=A6<= br>>>
>> where the latter one both requires polymorphism and= defines a locally
>> abstract type,
>> i.e. probably the= behavior you expect with (type b).
>>
>> Jacques
>= >
>
>
>
> --
> gregory malecha
--047d7bfea0f446963a052f176bbf--