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 D484F7EE63 for ; Mon, 29 Apr 2013 09:58:21 +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.212; 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.212; 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.212; 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: Ao4CAJknflHB/BfUcmdsb2JhbABSDoMwu2KCZYEUDgEKCgwJFAMlgh8BAQU4QAEQCxgJFg8JAwIBAgFFBgEMAQcBAYgWvE2PGgeDTwOXHoYTjWlB X-IPAS-Result: Ao4CAJknflHB/BfUcmdsb2JhbABSDoMwu2KCZYEUDgEKCgwJFAMlgh8BAQU4QAEQCxgJFg8JAwIBAgFFBgEMAQcBAYgWvE2PGgeDTwOXHoYTjWlB X-IronPort-AV: E=Sophos;i="4.87,572,1363129200"; d="scan'208";a="12550933" Received: from msa03.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.212]) by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Apr 2013 09:58:18 +0200 Received: from [192.168.1.106] ([86.195.153.11]) by mwinf5d61 with ME id VjyF1l0110F12tA03jyG7Y; Mon, 29 Apr 2013 09:58:17 +0200 Message-ID: <517E2818.5040506@frisch.fr> Date: Mon, 29 Apr 2013 09:58:16 +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 Le Normand , Jacques Garrigue CC: OCaML List Mailing References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> In-Reply-To: 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 and GADTs On 04/29/2013 07:17 AM, Jacques Le Normand wrote: > Fully injective types are the norm. It would have been nice to have a > "non injectivity" or "phantom type" annotation. Since phantom types are > seldom used, beginners won't get confused. It might even help beginners > understand the concept of a phantom type. I'd also prefer an annotation on "non injective" type parameters, rather than on "injective" one. The problem with this approach is that it requires existing well-typed code to be rewritten, to add these annotations (while annotating injectivity will only impact code using GADTs). I still believe this is less intrusive than requiring most parametrized abstract type to be annotated, or else making GADTs less useful. For the transition, we could have two compilation modes (decided on the command-line) for this feature. In "non-injective" (legacy) mode, every parametrized abstract type would be assumed to be non-injective. This would allow to compile existing code bases (at least those not relying on GADTs). In "injective-by-default" mode, non-injective parameters would need to be marked as such. Enabling this mode will require a few annotations to be added to existing code, but this will be very easy, so I guess we don't need to support "injectivity" annotations the "non-injective" mode. Alain