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 2E4D381792 for ; Tue, 2 Jul 2013 01:20:56 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Au8AAP8M0lGFBoIFnGdsb2JhbABaw0yBEw4BAQEBAQgUCTyCIwEBBAEnHAE1AgMLCzQSVwYTiAkFqUmERwKFP4gAB48rMweDBGOJJI4nlGU X-IPAS-Result: Au8AAP8M0lGFBoIFnGdsb2JhbABaw0yBEw4BAQEBAQgUCTyCIwEBBAEnHAE1AgMLCzQSVwYTiAkFqUmERwKFP4gAB48rMweDBGOJJI4nlGU X-IronPort-AV: E=Sophos;i="4.87,976,1363129200"; d="scan'208";a="24159923" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 02 Jul 2013 01:20:53 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id C89136380; Tue, 2 Jul 2013 08:20:50 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 50C922517; Tue, 2 Jul 2013 08:20:50 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id BDC8524FD; Tue, 2 Jul 2013 08:20:49 +0900 (JST) Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 (Mac OS X Mail 6.5 \(1508\)) From: Jacques Garrigue In-Reply-To: <51D19680.4060609@frisch.fr> Date: Tue, 2 Jul 2013 08:20:50 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <3BB0E3A0-455F-40D0-AA97-621AB7D24E4B@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <51D19680.4060609@frisch.fr> To: Alain Frisch X-Mailer: Apple Mail (2.1508) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 2013/07/01, at 23:47, Alain Frisch wrote: > A GADT was recently introduced to replace this with a more direct represe= ntation: >=20 > module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) : > sig > type _ is_t =3D Is: 'a ttype -> 'a T.t is_t > val check: 'a ttype -> 'a is_t option > end >=20 > The problem is that this doesn't work any more (because T.t is not inject= ive). >=20 > For now, I think I'll use: >=20 > module ABSTRACT_1_MATCHER (T : sig type 'a t val t: unit t ttype end) : > sig > type _ is_t =3D Is: 'b ttype * ('a, 'b T.t) TypEq.t -> 'a is_t > val check : 'a ttype -> 'a is_t option > end >=20 > which is accepted and roughly equivalent (by opening the equality witness= , one can retrieve the static equality 'a =3D=3D 'b T.t). Nice natural example, and nice workaround. Of course, this is not strictly equivalent. For instance suppose the following function: let f (type a) (tt : a T.t ttype) =3D 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. Jacques=