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 6CC3E7EE51 for ; Mon, 29 Apr 2013 18:37:12 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nathan.mishralinger@gmail.com) identity=pra; client-ip=74.125.82.179; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nathan.mishralinger@gmail.com"; x-sender="nathan.mishralinger@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of nathan.mishralinger@gmail.com designates 74.125.82.179 as permitted sender) identity=mailfrom; client-ip=74.125.82.179; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nathan.mishralinger@gmail.com"; x-sender="nathan.mishralinger@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f179.google.com) identity=helo; client-ip=74.125.82.179; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nathan.mishralinger@gmail.com"; x-sender="postmaster@mail-we0-f179.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AosCAL+gflFKfVKzk2dsb2JhbABTgz2sL5ITfggWDgEBAQEHCwsJFAQkgh8BAQVAARsSCwEDDAYFCw0NISIBEQEFAQoSBhMICodxAQMPDKAzjDGCfYQMChknAwpZhxsBBQyPDgeDTwOXHoEmjh8WKYRTIA X-IPAS-Result: AosCAL+gflFKfVKzk2dsb2JhbABTgz2sL5ITfggWDgEBAQEHCwsJFAQkgh8BAQVAARsSCwEDDAYFCw0NISIBEQEFAQoSBhMICodxAQMPDKAzjDGCfYQMChknAwpZhxsBBQyPDgeDTwOXHoEmjh8WKYRTIA X-IronPort-AV: E=Sophos;i="4.87,574,1363129200"; d="scan'208";a="15352694" Received: from mail-we0-f179.google.com ([74.125.82.179]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 29 Apr 2013 18:37:12 +0200 Received: by mail-we0-f179.google.com with SMTP id u7so1817579wey.38 for ; Mon, 29 Apr 2013 09:37:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:x-received:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=LEINuqmgz4EpX1zl/Izm11CEFxCOKFA0xUR3HCW3l1M=; b=gomNRJU3WeYsWIu/R/yQSO9xL77IKAY1dc9cpfvBcnXHqf4jYwsuGtX5IT0mfIJBKG QB0MhjaLk72PPBU0ofWdNc79sUR4AOOaUcrxE+aGa20tD9Pb3BZ54rIE0ZZhRCRRK9v8 wK7AqVuy3Do6bxAxZ0GSZWhDleADYLteqxCqiCrb4FavPL1jnsdkh5tvMn6vpPHW/O1X 4ESy+hrnjVOCOrp37oNQgwo1Z17efEapDlwa2HeB8SzqUIgS1UmqrzUgJcqRiIqpxOI9 wPDl2LZIUHH0PATdH1QodSIW6nDdxaGml5zTf1KpeOyOlzcN+Ohg+VxbPw5q5dkpiwHA N1XQ== MIME-Version: 1.0 X-Received: by 10.194.133.130 with SMTP id pc2mr16239307wjb.35.1367253431692; Mon, 29 Apr 2013 09:37:11 -0700 (PDT) Received: by 10.194.35.70 with HTTP; Mon, 29 Apr 2013 09:37:11 -0700 (PDT) In-Reply-To: <517E581A.20506@frisch.fr> 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> <517E581A.20506@frisch.fr> Date: Mon, 29 Apr 2013 12:37:11 -0400 Message-ID: From: Nathan Mishra Linger To: Alain Frisch Cc: Jacques Garrigue , OCaML List Mailing Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs Our codebase at Jane Street would not suffer from the proposed fix. In fact, we have previously wished the type system tracked injectivity of type constructors. Because it didn't, we wrote Type_equal.Injective [^1] for cases when we need to track injectivity ourselves. [^1] https://ocaml.janestreet.com/ocaml-core/latest/doc/core/Type_equal.Injective.html On Mon, Apr 29, 2013 at 7:23 AM, Alain Frisch wrote: > On 04/29/2013 12:52 PM, Jacques Garrigue wrote: >> >> What I want to know is whether anybody is using GADTs in a way that >> would be broken if we disallow type variables under abstract types >> (other than the predefined ones) in the return type of GADTs. >> I.e., for instance defining a type witness type involving such abstract >> types. > > > The only abstract types in the return type of GADTs in LexiFi's code base > code are currently either non-parametrized ones or built-in types (array, > lazy). So we'd be fine with the proposed fix (assuming that abstract types > are not injective). > > -- Alain > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs