From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 BA2287FB54 for ; Sun, 4 Jan 2015 18:12:38 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-50.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.150; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-50.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnUAAFh0qVSDbwiWnGdsb2JhbABcuAwGmCsCgQQWAQEBAQERAQEBAQEGDQkJFC6EDQEEASdSBQsLISUPAQRJLogJCAS4PINGAQEIAQEBAR4YhWuJdAeEKQWYFY0KgzmEEIMyAQEB X-IPAS-Result: AnUAAFh0qVSDbwiWnGdsb2JhbABcuAwGmCsCgQQWAQEBAQERAQEBAQEGDQkJFC6EDQEEASdSBQsLISUPAQRJLogJCAS4PINGAQEIAQEBAR4YhWuJdAeEKQWYFY0KgzmEEIMyAQEB X-IronPort-AV: E=Sophos;i="5.07,695,1413237600"; d="scan'208";a="115577305" Received: from ppsw-50.csi.cam.ac.uk ([131.111.8.150]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 04 Jan 2015 18:12:38 +0100 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from host86-182-254-133.range86-182.btcentralplus.com ([86.182.254.133]:37896 helo=netbook) by ppsw-50.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:AES128-GCM-SHA256:128) id 1Y7ojF-0002Oy-rP (Exim 4.82_3-c0e5623) (return-path ); Sun, 04 Jan 2015 17:12:37 +0000 From: Leo White To: Kaspar Rohrer Cc: caml-list@inria.fr References: X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Sun, 04 Jan 2015 17:12:36 +0000 In-Reply-To: (Kaspar Rohrer's message of "Sun, 4 Jan 2015 15:13:26 +0100") Message-ID: <86ppaucvwb.fsf@cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain Subject: Re: [Caml-list] Problem with GADTs and escaping types > type t = > | App : {k:'t . 'a->'t->'t; s:'a} -> t > > let munge : ('a->'t->'t as 'k) -> 'k = fun k -> fun s r -> k s r > > let transform = function > | App {k;s} -> App {k=munge k;s} > > 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 than > 't. 'a -> 't -> 't This is an example of the value restriction. A function application (like `munge k`) is not a syntactic value so it cannot be considered polymorphic. Since `App` requires `k` to be polymorphic, you get an error. The simplest solution in your case is probably to make `munge` work directly on the record type: let munge {k; s} = {k = (fun s r -> k s r); s} You could also create another record type containing only `k`, and have `munge` operate on that. > > If I add type annotations like so: > > let transform_annotated = function > | App {k;s} -> App {k=(munge k : 'a->'t->'t);s=(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 This is an example of the slightly surprising scoping of type variables. It sometimes surprises people, but any type variable (e.g. 'a in your above code), is given the same scope as the enclosing top-level definition (e.g. `transform_annotated`). Since it would not be safe for the existential type `'a` in the definition of `App` to escape outside of its match case this results in a slightly surprising error. Note that the annotation you have added does not actually do what you want anyway. You are trying to enforce the result of `munge k` to have the *polymorphic* type `'t. 'a -> 't -> 't`, but `'a -> 't -> 't` just ensures that both 't types are equal, it does not ensure that they are polymorphic. In fact, thanks to the top-level scope of type variables, your annotation is having the opposite effect, forcing `'t` to be considered monomorphic within the scope of the top-level definition. Hope that clears things up for you. You've managed to hit two slightly complicated parts of the type system in a single example. Regards, Leo