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 47413817AA for ; Thu, 4 Jul 2013 03:00:18 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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: AnABAOTI1FGFBoIFnGdsb2JhbABAGoM7wQWBIQ4BAQEBAQgUCTyCIwEBBAEnHAE1AgMLC0ZXBhOICQUNM6drhEcChT2HfwePODMHgwRpiSSOKIEpkzwt X-IPAS-Result: AnABAOTI1FGFBoIFnGdsb2JhbABAGoM7wQWBIQ4BAQEBAQgUCTyCIwEBBAEnHAE1AgMLC0ZXBhOICQUNM6drhEcChT2HfwePODMHgwRpiSSOKIEpkzwt X-IronPort-AV: E=Sophos;i="4.87,992,1363129200"; d="scan'208";a="19930827" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Jul 2013 03:00:15 +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 35C5E639A; Thu, 4 Jul 2013 10:00:13 +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 BDA5A395D; Thu, 4 Jul 2013 10:00:12 +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 garrigue-mini.math.nagoya-u.ac.jp (garrigue-mini.math.nagoya-u.ac.jp [172.16.30.37]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id B54BF251A; Thu, 4 Jul 2013 10:00:12 +0900 (JST) Content-Type: text/plain; charset=windows-1252 Mime-Version: 1.0 (Mac OS X Mail 6.5 \(1508\)) From: Jacques Garrigue In-Reply-To: <51D44C85.3040308@frisch.fr> Date: Thu, 4 Jul 2013 10:00:12 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <4AA00D93-1FD9-4E5B-9960-959BA835E8E5@math.nagoya-u.ac.jp> 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> 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/04, at 1:08, Alain Frisch wrote: > 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: >=20 > match StringMap_matcher.check t with > | Some (StringMap_matcher.Is (s, TypEq.Eq)) -> vmap (StringMap.map (of= _value ~t:s env) x) > | None -> ... >=20 > while one could write: >=20 > match StringMap_matcher.check t with > | Some (Is (s, Eq)) -> vmap (StringMap.map (of_value ~t:s env) x) > | None -> ... >=20 > (see http://caml.inria.fr/mantis/view.php?id=3D6023 ) In theory, it would be OK to assume that all pattern-matchings may contain = GADT type constructors. The only real problem is with let's: if they contain GADTs, we must use the= code for pattern-matching, which doesn't handle unused definition warnings= in the same way=85 Having all non recursive let's go through this code wou= ld have a high impact on warnings. If unused definition warnings could be separated from type checking this wo= uld be much easier. > In some cases (in particular to add annotations to make sense of error me= ssages), it would be useful to be able to name the type constructor introdu= ced by opening the GADT to match the existential type. (I'd put this rathe= r high on my wish list around GADTs!) I did to. As Gabriel mentioned, there was a discussion about syntax on Mantis. http://caml.inria.fr/mantis/view.php?id=3D5780 As is often the case with syntax, this ended with no agreement, so there is= no such feature=85 Actually, the problem with syntax is a bit deeper than that. Namely, my real concern is that currently locally abstract types cannot han= dle abstract row types. I think this is a severe limitation, at least for some applications. Maybe this problem should be solved first, as adding new syntax for existen= tial types without solving this will only make it deeper. Jacques=