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 7C25C81792 for ; Fri, 5 Jul 2013 14:02:34 +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.210; 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.210; 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.210; 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: ApsAAG601lHB/BfSlGdsb2JhbABagzzAeIEVDgEBAQEHDQkJFAMlgiMBAQU4QAEQCxgJFg8JAwIBAgFFEwEFAgEBiA+4do9rBxaDVwOXSYYhjjc X-IPAS-Result: ApsAAG601lHB/BfSlGdsb2JhbABagzzAeIEVDgEBAQEHDQkJFAMlgiMBAQU4QAEQCxgJFg8JAwIBAgFFEwEFAgEBiA+4do9rBxaDVwOXSYYhjjc X-IronPort-AV: E=Sophos;i="4.87,1001,1363129200"; d="scan'208";a="20125763" Received: from msa01.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.210]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Jul 2013 14:02:33 +0200 Received: from [192.168.1.111] ([92.151.124.168]) by mwinf5d02 with ME id wc2U1l00K3e6krg03c2Uj4; Fri, 05 Jul 2013 14:02:33 +0200 Message-ID: <51D6B5D4.6040601@frisch.fr> Date: Fri, 05 Jul 2013 14:02:28 +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: oleg@okmij.org CC: garrigue@math.nagoya-u.ac.jp, caml-list@inria.fr References: <20130705103000.2248.qmail@www1.g3.pair.com> In-Reply-To: <20130705103000.2248.qmail@www1.g3.pair.com> 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 On 07/05/2013 12:30 PM, oleg@okmij.org wrote: >> Naming types created by opening GADT existentials is useful not only for >> error messages, but also to have a way to refer to that type in the >> branch (for instance to instantiate locally a functor whose argument >> refers to that type). > > That is true, but isn't this a separate problem? Do you often need to > refer to the type in a branch? On the other hand, good error messages > are needed often, or all the time. To be clear: the GHC way to report errors seems good to me. But even if the default error message is improved, it is still helpful to be able to name the existential type simply to be able to write a type annotation mentioning that type somewhere deep in the branch (as a way to track down the actual error). Typically, only a very small number of #exN types exist in a given scope, so the fact that the error message does not tell where they come from is not a blocking point in making sense of the error, and not being able to name the type is more problematic. And of course, there are many other cases where it is useful to name the type, not only to track errors, but as ways to document the code or simply to be able to write it at all (especially when using local modules). And to answer your question: yes, I've had to introduce a local polymorphic function (with a locally abstract type) quite often to work-around the lack of naming facility. -- Alain