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 E448F81792 for ; Wed, 3 Jul 2013 18:14:25 +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=209.85.214.42; 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.214.42 as permitted sender) identity=mailfrom; client-ip=209.85.214.42; 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-bk0-f42.google.com) identity=helo; client-ip=209.85.214.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f42.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiQBADFN1FHRVdYqjmdsb2JhbABAGoM7Sa4Xkht7CBYOAQEBAQcNCQkSBiSCIwEBBAEnGQEbEgsBAwELBgULDQ0hIgERAQUBChIGExKHagEDCQYMM51FjE2Cf4QhChknAwpYh3QBBQyPXweDbQOXSYEpjjcWKYQ5Og X-IPAS-Result: AiQBADFN1FHRVdYqjmdsb2JhbABAGoM7Sa4Xkht7CBYOAQEBAQcNCQkSBiSCIwEBBAEnGQEbEgsBAwELBgULDQ0hIgERAQUBChIGExKHagEDCQYMM51FjE2Cf4QhChknAwpYh3QBBQyPXweDbQOXSYEpjjcWKYQ5Og X-IronPort-AV: E=Sophos;i="4.87,989,1363129200"; d="scan'208";a="19898011" Received: from mail-bk0-f42.google.com ([209.85.214.42]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 03 Jul 2013 18:14:25 +0200 Received: by mail-bk0-f42.google.com with SMTP id jk13so182341bkc.15 for ; Wed, 03 Jul 2013 09:14:24 -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=cEYnC0A4VhPQ6dvFUMqhr6SmF3CLxaviiGZB0JqTwuY=; b=wsNIqeB31dUiPsjTSppO3R3Ou2jqxGCetWAN0mjVKaJvITSOit8YKiuEA1pNtekVuZ Kt1ePa2nSUo66ObbtlqKz/cBpRl8QZQuTQL++BHdwmeqZcaSVb2c1+eVt2+rasakOmMu qEXiJ841zbMmzZw34EOcbTlSubPIlfCtHPnZ9y7WajiUOFOjILWZuJfGWvESi4ulk67p 2MC+4J2VQAk5PO8rjKmnVBmuO10taXHoZA5RcjK71QWxVRuxYS6vmvKSo55W2J9qV2Kc WGe6hk6ZbzWx97HSg51F5+KonsVvzxJvi6d1W39jiocm+NVveY9WQvXq91Tw2+wGm4DC TF0A== X-Received: by 10.204.191.10 with SMTP id dk10mr302224bkb.35.1372868064612; Wed, 03 Jul 2013 09:14:24 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.20.131 with HTTP; Wed, 3 Jul 2013 09:13:44 -0700 (PDT) In-Reply-To: <51D44C85.3040308@frisch.fr> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <51D19680.4060609@frisch.fr> <3BB0E3A0-455F-40D0-AA97-621AB7D24E4B@math.nagoya-u.ac.jp> <51D44C85.3040308@frisch.fr> From: Gabriel Scherer Date: Wed, 3 Jul 2013 18:13:44 +0200 Message-ID: To: Alain Frisch Cc: Jacques Garrigue , OCaML List Mailing Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs > In some cases (in particular to add annotations to make sense of error > messages), it would be useful to be able to name the type constructor > introduced by opening the GADT to match the existential type. (I'd put this > rather high on my wish list around GADTs!) Indeed, virtually anyone that used GADTs in OCaml encountered that problem and has a way to name existential type high on his/her wishlist. We discussed a few ideas in the following bugtracking dicussion: http://caml.inria.fr/mantis/view.php?id=5780 On Wed, Jul 3, 2013 at 6:08 PM, Alain Frisch wrote: > On 07/02/2013 01:20 AM, Jacques Garrigue wrote: >> >> On 2013/07/01, at 23:47, Alain Frisch wrote: >> >>> A GADT was recently introduced to replace this with a more direct >>> representation: >>> >>> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) : >>> sig >>> type _ is_t = Is: 'a ttype -> 'a T.t is_t >>> val check: 'a ttype -> 'a is_t option >>> end >>> >>> The problem is that this doesn't work any more (because T.t is not >>> injective). >>> >>> For now, I think I'll use: >>> >>> module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) : >>> sig >>> type _ is_t = Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t >>> val check : 'a ttype -> 'a is_t option >>> end >>> >>> which is accepted and roughly equivalent (by opening the equality >>> witness, one can retrieve the static equality 'a == 'b T.t). >> >> >> Nice natural example, and nice workaround. > > > Btw, this is also an example where type-based disambiguation in presence of > a GADT would be useful. For instance, we currently need to write: > > match StringMap_matcher.check t with > | Some (StringMap_matcher.Is (s, TypEq.Eq)) -> vmap (StringMap.map > (of_value ~t:s env) x) > | None -> ... > > while one could write: > > match StringMap_matcher.check t with > | Some (Is (s, Eq)) -> vmap (StringMap.map (of_value ~t:s env) x) > | None -> ... > > (see http://caml.inria.fr/mantis/view.php?id=6023 ) > > >> Of course, this is not strictly equivalent. >> For instance suppose the following function: >> let f (type a) (tt : a T.t ttype) = >> match check tt with None -> assert false >> | Some (Is (tta, Eq)) -> (tta : a ttype) >> The pattern matching will succeed, but tta will only have type "a ttype" >> if T.t is injective. The nice part is that this is delayed to the use >> site, >> where we may have more information about T.t, so this trick may still >> be useful after introducing injectivity annotations. >> >> Anyway, I suppose that this will work fine for you: check is intended >> to be called on unknown types, so the missing equality should not >> be a problem. > > > Indeed! > > In some cases (in particular to add annotations to make sense of error > messages), it would be useful to be able to name the type constructor > introduced by opening the GADT to match the existential type. (I'd put this > rather high on my wish list around GADTs!) > > > Alain > > > -- > 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