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 0662A7EE51 for ; Tue, 30 Apr 2013 01:53:30 +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: AtcGACcHf1GFBoIFdGdsb2JhbABSgz2+SAQEAYEcDgEMFQg8gh8BAQQBJxwBNQIDCws0EiE2BhOIBAMJBQ2tGYMygRIChQsNTIc1AwSMRIEkfzMHgm5hiROMKoFkjAuIP4Fk X-IPAS-Result: AtcGACcHf1GFBoIFdGdsb2JhbABSgz2+SAQEAYEcDgEMFQg8gh8BAQQBJxwBNQIDCws0EiE2BhOIBAMJBQ2tGYMygRIChQsNTIc1AwSMRIEkfzMHgm5hiROMKoFkjAuIP4Fk X-IronPort-AV: E=Sophos;i="4.87,576,1363129200"; d="scan'208";a="15400689" 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; 30 Apr 2013 01:53:27 +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 599A0636B; Tue, 30 Apr 2013 08:53:24 +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 2924F2564; Tue, 30 Apr 2013 08:53:24 +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 DCC9F2504; Tue, 30 Apr 2013 08:53:23 +0900 (JST) Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) From: Jacques Garrigue In-Reply-To: Date: Tue, 30 Apr 2013 08:53:23 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <4282AC1F-F399-4492-980D-8A52C4215E92@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> <517E2818.5040506@frisch.fr> <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp> <517E581A.20506@frisch.fr> To: Nathan Mishra Linger X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 2013/04/30, at 1:37, Nathan Mishra Linger wrote: > Our codebase at Jane Street would not suffer from the proposed fix. >=20 > In fact, we have previously wished the type system tracked injectivity of= type > constructors. Because it didn't, we wrote Type_equal.Injective [^1] for = cases > when we need to track injectivity ourselves. >=20 > [^1] https://ocaml.janestreet.com/ocaml-core/latest/doc/core/Type_equal.I= njective.html Thank you for the pointer. One could say this actually shows the need for injectivity annotations (eventhough Core currently works around them). To be more precise, injectivity has several uses: 1) To allow you to infer equations between types. For instance, assuming the standard equality witness type: type (_,_) equal =3D Eq : ('a,'a) equal the following function typeckecks let conv1 : type a b. (a array, b array) equal -> a -> b =3D fun Eq= x -> x because array is known to be injective, but this one doesn't let conv2 : type a b. (a Queue.t, b Queue.t) equal -> a -> b =3D fun Eq x = -> x because Queue.t is an abstract type whose injectivity is unknown. This part was correctly handled since 4.00.0. 2) To allow you to prove exhaustiveness of pattern matching, by ensuring that other cases cannot happen. For instance, type (_,_) comp =3D | Ceq : ('a,'a) comp | Cany : ('a,'b) comp let f (x : (int array,bool array) comp) =3D match x with Cany -> () =20=20=20=20=20=20=20 causes no warning, because the type system can prove that Ceq since int array and bool array cannot be equal in any scope. However let f (x : (int Queue.t, bool Queue.t) comp) =3D match x with Cany -> 0 should emit a warning, because we cannot prove that int Queue.t and bool Queue.t are distinct in the absence of injectivity information. Note that this is not correctly handled in 4.00, and you will get no war= ning in this situation. Worse, since the code is optimized accordingly (i.e. = no runtime check is introduced), if the type is really not injective, and y= ou pass Eq, you can use this as a hole in the type system. This now works correctly in trunk (PR#5981). 3) The problem I describe in my first mail. I.e. when defining a type, if you use type variables appearing in constrained type parameters, you need the type constructors leading to the type variables to be injective. This is PR#5985, and it is only fixed in branches/non-vanishi= ng. The goal of the Type_equal.Injective interface in Core is to work around t= he limitation on abstract types in (1), by letting you prove injectivity by ha= nd. But if we had injectivity annotations, this would solve simultaneously all 3 problems: no need to build proofs by hand anymore. So I understand you answer as: Jane Street is not directly concerned by (3) at this point, and has already developed a workaround for (1). I suppose you could profit from injectivity annotations, since you had to develop a workaround, but this may not be that urgent. (2) is not so much a problem, since it only means that you may have to add extra cases to pattern-matching. Jacques Garrigue=