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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 2635D7EE34 for ; Mon, 28 Mar 2016 17:35:43 +0200 (CEST) IronPort-PHdr: 9a23:td+hlRTvfC7ngbR8jkf9H3V3R9psv+yvbD5Q0YIujvd0So/mwa64bBGN2/xhgRfzUJnB7Loc0qyN4/CmAzBLsMrJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uJP04Z2HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1QVWH8Xnx4AOAPF4Qv3RN+lvSLwrOtw3G+BNs37V70ucTun5qZvDhTvjXFUGSQ+9TT4kMF/i7hK6DeooxF0w4ecNI6QPf5zdaPUVdwfTGtFGM1WUnoSUcuHc4ITAr9Zbq5jpI7nqg5L9EPmCA== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha@gmail.com; spf=Pass smtp.mailfrom=gmalecha@gmail.com; spf=None smtp.helo=postmaster@mail-oi0-f52.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gmalecha@gmail.com) identity=pra; client-ip=209.85.218.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gmalecha@gmail.com"; x-sender="gmalecha@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gmalecha@gmail.com designates 209.85.218.52 as permitted sender) identity=mailfrom; client-ip=209.85.218.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gmalecha@gmail.com"; x-sender="gmalecha@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-oi0-f52.google.com) identity=helo; client-ip=209.85.218.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gmalecha@gmail.com"; x-sender="postmaster@mail-oi0-f52.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BTAABJTvlWizTaVdFchH62BIRuAQ2BcIYNAoEgOBQBAQEBAQEBARABAQEICwsJHzGCLYIUAQEBAwESEQQZARsdAQMBCwYDAgsNKgICIQEBEQEFARwGEyKHbwEDCgiSR49BgTE+MYs2gWqCV4YXChknDVGEBwEBAQEBAQEDAQEBAQEBAQESAQUKBYUXeIREgj6EfoJWBZMGhCoxjBGBdY8LhzaGFy+BDx4BAYI4HoFRPDCIegEBAQ X-IPAS-Result: A0BTAABJTvlWizTaVdFchH62BIRuAQ2BcIYNAoEgOBQBAQEBAQEBARABAQEICwsJHzGCLYIUAQEBAwESEQQZARsdAQMBCwYDAgsNKgICIQEBEQEFARwGEyKHbwEDCgiSR49BgTE+MYs2gWqCV4YXChknDVGEBwEBAQEBAQEDAQEBAQEBAQESAQUKBYUXeIREgj6EfoJWBZMGhCoxjBGBdY8LhzaGFy+BDx4BAYI4HoFRPDCIegEBAQ X-IronPort-AV: E=Sophos;i="5.24,407,1454972400"; d="scan'208,217";a="210684372" Received: from mail-oi0-f52.google.com ([209.85.218.52]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 28 Mar 2016 17:35:41 +0200 Received: by mail-oi0-f52.google.com with SMTP id o62so61678268oig.1 for ; Mon, 28 Mar 2016 08:35:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=+EmmLUu0xYNk3Rfy0DHLflpc+sO3wQGMa675B7bJ/Lo=; b=dsK/HSFif/PpXmZpqGf05AYK98+UlDVmL89rZB3wjmHadyfsE5ecb1D1G7LBpcNWuI EjSVPz8l4mAWj+695WtIDCBUdrFP98JvIny/HicUlI0OOgwR/rHG53x0S1TBByJMHrA6 ab3+nc/5oWT38ks3TFp+djsMKUJGphiiBZSB0QE7cYehbTb/fprYUjdU1V9YYbYce0An O1FnIwczHe70wezkOoYXSZDRI7i+ZlApA97u5vFDmAR0tgPUwZZDWeuoMrkO3yw6vJCR XHudy6uhBZvXiC1pvf83KjS4T/KdccW/rtCiqMX5CLSAZczRQOnGlA/3jahVE1/mMxlk TV/Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=+EmmLUu0xYNk3Rfy0DHLflpc+sO3wQGMa675B7bJ/Lo=; b=iiBYZfOK/rMpKx4cPvhiJzEbmnR+GJ2fPghCoyVoRBdCRWcuXaZxjC2KR5R/0tMJql h/twfyXDqINIDR/eZG4AzZvWeLTRnvJMUDCXCK9Fu2WsHyTBo0K983cB+RXD5BRwFBKW IdO8DUZeTEdi0IUiGoImZkQ2QO4X8EIRfMguMXEOTtPaNgYcxjDmldBHPUe/3L7nz66R AV2+nYl/khtwyMxt1GcJAAAFv/PsvXr8FQqPbqHjQaTM+y4ke1nzExK5agwMVh6SW4RU crSbT2is5QsLUsk8EYKexCGKJI0fiXaNjCwt635v8s3jqXefCfOxOcXK4m2YU/qf9d7w RPFg== X-Gm-Message-State: AD7BkJLKw6c+Obf/YZOP1SNDSQc7SVGe8wDbtWiuxm6hg1KDyY7jaAtimCYHLE5XhMcN4KmJ2Z4cGgARZCaoqg== X-Received: by 10.202.195.69 with SMTP id t66mr1465058oif.26.1459179340320; Mon, 28 Mar 2016 08:35:40 -0700 (PDT) MIME-Version: 1.0 References: <86d1qgqu45.fsf@lpw25.net> <2D2C7D68-D59A-407B-B83A-65622DF9CC25@math.nagoya-u.ac.jp> In-Reply-To: From: Gregory Malecha Date: Mon, 28 Mar 2016 15:35:30 +0000 Message-ID: To: Gabriel Scherer Cc: Jacques Garrigue , Mailing List OCaml Content-Type: multipart/alternative; boundary=001a113e235a3e55ac052f1daaaa Subject: Re: [Caml-list] "Type constructor b would escape its scope" --001a113e235a3e55ac052f1daaaa Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thanks so much. On Mon, Mar 28, 2016, 1:08 AM Gabriel Scherer wrote: > 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 fai= ls > 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_resu= lt, =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 > --001a113e235a3e55ac052f1daaaa Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

Thanks so much.


On Mon, Mar 28, 2016, 1:08 = AM Gabriel Scherer <gabriel= .scherer@gmail.com> wrote:
<= div dir=3D"ltr">Locally abstract types scope over the definition body where= they can
be used as type names or to refine GADTs by pattern-matching.<= br>
mod= ule type Ty =3D sig type t end

(* we need the scoping of the locally= abstract type in this example;
=C2=A0 =C2=A0note that (type a) would wo= rk 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 type= t =3D a end in
=C2=A0 =C2=A0 (module T)

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

(* a type vari= able '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, 20= 16 at 6:20 AM, Gregory Malecha <gmalecha@gmail.com> wrote:
> Thanks. I'm n= ot sure I understand the difference between the two though. Is
> ther= e an example showing when they produce different results?
>
> O= n Sun, Mar 27, 2016 at 6:12 PM, Jacques Garrigue
> <garrigue@math.nagoya-u.= ac.jp> wrote:
>>
>> On 2016/03/28 03:52, Gregory M= alecha wrote:
>> >
>> > Thanks, Leo --
>> = >
>> > This is exactly what I needed to know. I thought that= the (type a)
>> > annotation was forcing the function to be po= lymorphic. For future reference,
>> > is there any way to write= the annotation (that forces the function to be
>> > polymorphi= c) without having to write explicit =E2=80=98fun's?
>>
>= > You should either write
>>
>> =C2=A0 let generic_sea= rch_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 -> (i= nternal_result, b)
>> result_stream =3D =E2=80=A6
>>
&= gt;> where the latter one both requires polymorphism and defines a local= ly
>> abstract type,
>> i.e. probably the behavior you ex= pect with (type b).
>>
>> Jacques
>>
>
= >
>
> --
> gregory malecha
--001a113e235a3e55ac052f1daaaa--