From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 13C9F7FB54 for ; Sun, 4 Jan 2015 15:13:31 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of kaspar.rohrer@gmail.com) identity=pra; client-ip=74.125.82.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kaspar.rohrer@gmail.com"; x-sender="kaspar.rohrer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of kaspar.rohrer@gmail.com designates 74.125.82.177 as permitted sender) identity=mailfrom; client-ip=74.125.82.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kaspar.rohrer@gmail.com"; x-sender="kaspar.rohrer@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-we0-f177.google.com) identity=helo; client-ip=74.125.82.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kaspar.rohrer@gmail.com"; x-sender="postmaster@mail-we0-f177.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: An0AAMRJqVRKfVKxlGdsb2JhbABTCYQwzREWAQEBAQERAQEBAQcLCwkSMIQOBBMVGQEbHgMBERBeEQEFAVeHdQEDCQgEAZhrgyc+MY0ZgneKAgoZJw1Ug0IBAQEYAQUOjw6DeIETBZcIhgSKAjWBFYQRboJDAQEB X-IPAS-Result: An0AAMRJqVRKfVKxlGdsb2JhbABTCYQwzREWAQEBAQERAQEBAQcLCwkSMIQOBBMVGQEbHgMBERBeEQEFAVeHdQEDCQgEAZhrgyc+MY0ZgneKAgoZJw1Ug0IBAQEYAQUOjw6DeIETBZcIhgSKAjWBFYQRboJDAQEB X-IronPort-AV: E=Sophos;i="5.07,695,1413237600"; d="scan'208,217";a="95260336" Received: from mail-we0-f177.google.com ([74.125.82.177]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jan 2015 15:13:30 +0100 Received: by mail-we0-f177.google.com with SMTP id q59so6490964wes.22 for ; Sun, 04 Jan 2015 06:13:30 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=from:content-type:subject:message-id:date:to:mime-version; bh=dn3KZEu+E/VYqUN56EYr6MIyHPMwenhfc7WccL6BprM=; b=PCozenPiG4SHg8L5pd+D+6AKpMjSh3izTZ/lwQ+JdBOzoLr5BsbNd0Ff/aNur/P2Hd igLo46KB4DIQl2CWcd+kjo5tx+BrQ1V191q8fXnSVJAiOXKDq5zFggcOkTi2yfgloAT3 68me8YQ/uQfUv1DJsDafLFFBrgbvW6ncn4HsServ1dYzA0Yx7U7c21YkWh4Zu0k5gQpy EysEtQMT/iBNQvokJnf/BcDYqteYVVUb/QhsPyNmnLxcp8Kv1u7yUEH7hQ0VY/5mH8C9 pRXCyWDBm/2M6KCDZJb6I1lZgiTdexVRA2IrCxk+JAiGLiOcckp6GPPidZWl2kSwsw+2 k+ng== X-Received: by 10.194.6.70 with SMTP id y6mr152393284wjy.97.1420380810077; Sun, 04 Jan 2015 06:13:30 -0800 (PST) Received: from [192.168.1.4] (dynamic-207-067.catv.glattnet.ch. [80.242.207.67]) by mx.google.com with ESMTPSA id b10sm25199892wjr.32.2015.01.04.06.13.28 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Sun, 04 Jan 2015 06:13:29 -0800 (PST) From: Kaspar Rohrer Content-Type: multipart/alternative; boundary="Apple-Mail=_A7F258AC-2D68-4FE4-929E-6292A38AE476" Message-Id: Date: Sun, 4 Jan 2015 15:13:26 +0100 To: caml-list@inria.fr Mime-Version: 1.0 (Mac OS X Mail 7.3 \(1878.6\)) X-Mailer: Apple Mail (2.1878.6) Subject: [Caml-list] Problem with GADTs and escaping types --Apple-Mail=_A7F258AC-2D68-4FE4-929E-6292A38AE476 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii Hi all I was playing around with GADTs over the last few days and encountered the = following problem (reduced to a minimal case here):=20 > type t =3D > | App : {k:'t . 'a->'t->'t; s:'a} -> t >=20 > let munge : ('a->'t->'t as 'k) -> 'k =3D fun k -> fun s r -> k s r >=20 > let transform =3D function > | App {k;s} -> App {k=3Dmunge k;s} Note that I am using inlined records, which are only available in the unrel= eased 4.03 version. But I get the same error when using a separate record i= n OCaml 4.01, i.e.: > type t =3D App : 'a app_t -> t > and 'a app_t =3D { k : 't. 'a->'t->'t; s:'a } OCaml will choke on the transform function with the following error: > Error: This field value has type a#17 -> 'b -> 'b which is less general t= han > 't. 'a -> 't -> 't If I add type annotations like so: > let transform_annotated =3D function > | App {k;s} -> App {k=3D(munge k : 'a->'t->'t);s=3D(s:'a)} OCaml will instead give me an error about escaping types: > Error: This expression has type a#19 -> 'a -> 'a > but an expression was expected of type a#19 -> 't -> 't > The type constructor a#19 would escape its scope I can work around this whole problem by inlining the munge function: > let transform_inline =3D function > | App {k;s} -> let k' s r =3D k s r in App {k=3Dk';s} This works but it is not ideal for my case, as it leads to somewhat unwield= y match expressions. Can somebody explain to me why the first case does not work? Especially whe= n considering that the types should be equal (substituting the identity fun= ction for munge produces the the same error). Thank you in advance Kaspar M. Rohrer --Apple-Mail=_A7F258AC-2D68-4FE4-929E-6292A38AE476 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii
Hi all

=
I was playing around with GADTs over the last few days and encou= ntered the following problem (reduced to a minimal case here): 
<= div>
type t =3D
  | = App : {k:'t . 'a->'t->'t; s:'a} -> t

let = munge : ('a->'t->'t as 'k) -> 'k =3D fun k -> fun s r -> k s= r

=
let transform = =3D function
  | App {k;s} ->= App {k=3Dmunge k;s}

Note that I am u= sing inlined records, which are only available in the unreleased 4.03 versi= on. But I get the same error when using a separate record in OCaml 4.01, i.= e.:

type t = =3D App : 'a app_t -> t
and 'a app_t =3D { k : 't. 'a->'t-&= gt;'t; s:'a }

OCaml will choke on the= transform function with the following error:

Error: This field value ha= s type a#17 -> 'b -> 'b which is less general than
  &= nbsp;      't. 'a -> 't -> 't
=

If I add type annotations like so:

=
let transform_annotated =3D = function
  | App {k;s} -> App {k=3D(munge k : 'a->'t-&= gt;'t);s=3D(s:'a)}

OCaml will instead give= me an error about escaping types:

=
Error: This expression has type a= #19 -> 'a -> 'a
       but an expressio= n was expected of type a#19 -> 't -> 't
     = ;  The type constructor a#19 would escape its scope

I can work around this whole problem by inlining = the munge function:

let transform_inline =3D function
  | App {k;s} = -> let k' s r =3D k s r in App {k=3Dk';s}

This works but it is not ideal for my case, as it leads to so= mewhat unwieldy match expressions.

Can somebody ex= plain to me why the first case does not work? Especially when considering t= hat the types should be equal (substituting the identity function for munge= produces the the same error).

Thank you in advanc= e
Kaspar M. Rohrer

= = --Apple-Mail=_A7F258AC-2D68-4FE4-929E-6292A38AE476--