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 14D3881792 for ; Thu, 4 Jul 2013 10:50:46 +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: AnMBAFM21VGFBoIFnGdsb2JhbABagzzBBoEaDgEBAQEBCBQJPIIjAQEEAUMBNQIDCwsYLlcGE4gJBadshEcChTaHfwePODMHgwRpiSSOKIYhjkQt X-IPAS-Result: AnMBAFM21VGFBoIFnGdsb2JhbABagzzBBoEaDgEBAQEBCBQJPIIjAQEEAUMBNQIDCwsYLlcGE4gJBadshEcChTaHfwePODMHgwRpiSSOKIYhjkQt X-IronPort-AV: E=Sophos;i="4.87,993,1363129200"; d="scan'208";a="19973506" 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 10:50:43 +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 093B0639F; Thu, 4 Jul 2013 17:50:39 +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 F1C40396A; Thu, 4 Jul 2013 17:50:38 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type: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 [192.168.1.23] (bsdserver10-alias1.math.nagoya-u.ac.jp [172.16.62.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 22556251A; Thu, 4 Jul 2013 17:50:38 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 6.5 \(1508\)) Content-Type: text/plain; charset=windows-1252 From: Jacques Garrigue In-Reply-To: <51D52ED1.30808@frisch.fr> Date: Thu, 4 Jul 2013 17:52:37 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <02A805B7-5114-43F6-8A27-6EF0818AE973@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> <4AA00D93-1FD9-4E5B-9960-959BA835E8E5@math.nagoya-u.ac.jp> <51D52ED1.30808@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 17:14, Alain Frisch wrote: > On 07/04/2013 03:00 AM, Jacques Garrigue wrote: >> In theory, it would be OK to assume that all pattern-matchings may conta= in 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 warni= ngs in the same way=85 Having all non recursive let's go through this code = would have a high impact on warnings. >=20 > If this is the only problem with the direct approach (not depending on ba= cktracking), maybe the treatment of warnings can be parametrized to behave = as expected? This does not remove the need for backtracking, as the backtracking occurs = in the code for typing pattern-matching. It is needed to detect where GADTs are actually used. (By the way this backtracking concerns only the typing of pattern-matching,= and it is not costly, so there is no real need to avoid it). The goal is to allow to switch between the code for let-in and the code for= match freely. >> If unused definition warnings could be separated from type checking this= would be much easier. >=20 > Maybe I'm wrong, but it seems to me that achieving the same behavior woul= d require to duplicate of lot of the "data-flow" logic in the type-checker,= thus increasing the global complexity (and the risk to have diverging beha= viors). I just mean that if it could abstracted so that one could call the same use= -tracking function for type_cases and type_let, things would be simpler. Th= e goal here is factoring, not duplicating. Jacques Garrigue=