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 7626F81792 for ; Wed, 3 Jul 2013 18:08:38 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=pra; client-ip=193.252.23.212; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.212; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@msa.smtpout.orange.fr) identity=helo; client-ip=193.252.23.212; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="postmaster@msa.smtpout.orange.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmkBADJM1FHB/BfUcmdsb2JhbABAGg6DLQHAeoEZDgEKCgwJFAMlgiMBAQQBJxFAAQULCxgJFg8JAwIBAgFFBg0BBQIBAYgFCggzul2PODMHg20Dl0mBKYR4jXdA X-IPAS-Result: AmkBADJM1FHB/BfUcmdsb2JhbABAGg6DLQHAeoEZDgEKCgwJFAMlgiMBAQQBJxFAAQULCxgJFg8JAwIBAgFFBg0BBQIBAYgFCggzul2PODMHg20Dl0mBKYR4jXdA X-IronPort-AV: E=Sophos;i="4.87,988,1363129200"; d="scan'208";a="19897419" Received: from msa03.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.212]) by mail3-smtp-sop.national.inria.fr with ESMTP; 03 Jul 2013 18:08:37 +0200 Received: from [192.168.1.111] ([92.151.124.168]) by mwinf5d29 with ME id vs8b1l0093e6krg03s8b03; Wed, 03 Jul 2013 18:08:37 +0200 Message-ID: <51D44C85.3040308@frisch.fr> Date: Wed, 03 Jul 2013 18:08:37 +0200 From: Alain Frisch User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:22.0) Gecko/20100101 Thunderbird/22.0 MIME-Version: 1.0 To: Jacques Garrigue CC: OCaML List Mailing 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> In-Reply-To: <3BB0E3A0-455F-40D0-AA97-621AB7D24E4B@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs 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