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 5609E7EE51 for ; Tue, 30 Apr 2013 08:59:07 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=pra; client-ip=193.252.23.211; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.211; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@msa.smtpout.orange.fr) identity=helo; client-ip=193.252.23.211; receiver=mail2-smtp-roc.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: AswBAL1of1HB/BfTlGdsb2JhbABSDoMwu3KCZIEfDgEBAQEJCwkJFAMlgh8BAQQBMgEFQAYLCxgJFg8JAwIBAgFFBgEMCAEBF4d1CrA1jliNaIE5g08Dlx6GE41pQYFx X-IPAS-Result: AswBAL1of1HB/BfTlGdsb2JhbABSDoMwu3KCZIEfDgEBAQEJCwkJFAMlgh8BAQQBMgEFQAYLCxgJFg8JAwIBAgFFBgEMCAEBF4d1CrA1jliNaIE5g08Dlx6GE41pQYFx X-IronPort-AV: E=Sophos;i="4.87,579,1363129200"; d="scan'208";a="15436851" Received: from msa02.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.211]) by mail2-smtp-roc.national.inria.fr with ESMTP; 30 Apr 2013 08:59:07 +0200 Received: from [192.168.1.106] ([86.195.153.11]) by mwinf5d57 with ME id W6z51l0010F12tA036z5FB; Tue, 30 Apr 2013 08:59:06 +0200 Message-ID: <517F6BB9.4070703@frisch.fr> Date: Tue, 30 Apr 2013 08:59:05 +0200 From: Alain Frisch User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:21.0) Gecko/20100101 Thunderbird/21.0 MIME-Version: 1.0 To: Jacques Garrigue , OCaML List Mailing 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> In-Reply-To: <1EA5B7CE-C0C3-4113-9F8F-C4C3BC888D49@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On 04/29/2013 12:52 PM, Jacques Garrigue wrote: > Again, the defect of such a mode is that it is going to apply to everything, including functors. > A functor compiled in this mode might be not be applicable to some modules, whereas there was > no reason from the beginning to require injectivity there. > > And just using variance to change the behavior is not going to work well: > a standard practice is to explicitly define module types for the input and output of > the functor. We want the output types to be injective, but we don't really need such > requirement for the input types. But they are just module type definitions… > (See hashtbl.mli for instance for this pattern.) These are interesting arguments against the "injective by default" mode (explicit non-injectivity annotations). I did not think about the consequences on functors indeed. In practice, though, it might be ok to annotate, if needed, some module types used as functor arguments with non-injectivity annotations (or more precisely "not-necessarily injective" annotations). But this certainly deserves some careful thinking. It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying. I'm only concerned with: > 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-vanishing. Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs? -- Alain