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 D497E7F9A7 for ; Mon, 30 Jun 2014 13:07:42 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of bmillwood@janestreet.com) identity=pra; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of bmillwood@janestreet.com designates 38.105.200.112 as permitted sender) identity=mailfrom; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.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@mxout1.mail.janestreet.com) identity=helo; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AloBAJBDsVMmachwnGdsb2JhbABahDmCbqguBpo1AX8IFg8BAQEBAQgUCTyEAwEBAQMBEhEdAQE3AQQLCwQBBjAHAgIiEgEFARwGEyKIGAgDAp5aaoowd4UCAQWXGhEGCoVaiSMHgneBTJpjkgwYKYMwgUM X-IPAS-Result: AloBAJBDsVMmachwnGdsb2JhbABahDmCbqguBpo1AX8IFg8BAQEBAQgUCTyEAwEBAQMBEhEdAQE3AQQLCwQBBjAHAgIiEgEFARwGEyKIGAgDAp5aaoowd4UCAQWXGhEGCoVaiSMHgneBTJpjkgwYKYMwgUM X-IronPort-AV: E=Sophos;i="5.01,574,1400018400"; d="scan'208";a="82911654" Received: from mxout1.mail.janestreet.com ([38.105.200.112]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 30 Jun 2014 13:07:41 +0200 Received: from tot-smtp.delacy.com ([172.27.22.15] helo=tot-smtp) by mxout1.mail.janestreet.com with esmtps (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.82) (envelope-from ) id 1X1ZQw-0000rX-Td for caml-list@inria.fr; Mon, 30 Jun 2014 07:07:38 -0400 Received: from tot-dmz-mxgoog1.delacy.com ([172.27.224.14] helo=mxgoog2.janestreet.com) by tot-smtp with esmtps (TLSv1:AES256-SHA:256) (Exim 4.72) (envelope-from ) id 1X1ZQw-0006ZX-Pp for caml-list@inria.fr; Mon, 30 Jun 2014 07:07:38 -0400 Received: from mail-qc0-f179.google.com ([209.85.216.179]) by mxgoog2.janestreet.com with esmtp (Exim 4.76) (envelope-from ) id 1X1ZQw-00035k-OG for caml-list@inria.fr; Mon, 30 Jun 2014 07:07:38 -0400 Received: by mail-qc0-f179.google.com with SMTP id x3so6872627qcv.38 for ; Mon, 30 Jun 2014 04:07:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=/XL4C0lc1LJor1Vxj5DDEntm+lJd17H2Qu6lmWjXrPo=; b=a8C6gWwisQ9OdygUb6XsjpVzt5BlDeHhr9fJVgxlBbX1NG79QUU4zkMxYXt+v7BR4/ pSGLIMXG+Oml6meI8omsy/q18WvRVNdP6xl9Toer/8vHYBt0JUBl4ghAyCrvJberZEzd NXVmtxjAfIJzyD8S18AH317UX07QN17Kuh+R4= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type; bh=/XL4C0lc1LJor1Vxj5DDEntm+lJd17H2Qu6lmWjXrPo=; b=XBSAcef2R78FjGbNUI+0+ZAi/dUMe3AJcvyM0AEAAx9OSrCqZFx/FPJ0suaEJmJe5Z LTCveT3y2TdJ/OEmJ0dKQXofvREBdpI7AlxIFuhwnsOV3iOl6Ni6QPeO2NpRxXfxpyVD JOzbkEy7NuLakbXz0bHJm+1Qn1/3W9yE2WzEGb7cOUaZhxuWleQb/efodMKi3gwA88wK XZlPwJ39beYI69dm4Zpd3MhhcGC9avPNKB3ukB+qww8ehE8/M1gSvR2YF98BszN9FqeQ p6SzeJHLbBEXqj69H/O1ALRYna7OWT/wgpjrXkfaCBZRBYI5g/KecnfhQt4cKxwD4FCq Fr0A== X-Gm-Message-State: ALoCoQlyHGWQL/eWC18r84+YRTV9Pr1R/vIHDL4jRx+NGsdFPlSwnnZC+2ao9lD5e+zKf9YiVaG6OUg0RhCHjdiErXrXV5J3hR/eqrGhbPafTpQRNxzFftYPiTPp+8y1bH1hgtBXlpeA X-Received: by 10.140.32.166 with SMTP id h35mr11236888qgh.114.1404126458582; Mon, 30 Jun 2014 04:07:38 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.140.32.166 with SMTP id h35mr11236872qgh.114.1404126458497; Mon, 30 Jun 2014 04:07:38 -0700 (PDT) Received: by 10.140.103.67 with HTTP; Mon, 30 Jun 2014 04:07:38 -0700 (PDT) In-Reply-To: <20140629144929.GB32483@mlqds.hnr.gr> References: <1403996132.26873.18.camel@chi.nicolast.be> <20140629144929.GB32483@mlqds.hnr.gr> Date: Mon, 30 Jun 2014 12:07:38 +0100 Message-ID: From: Ben Millwood To: =?UTF-8?Q?Gr=C3=A9goire_Henry?= Cc: Nicolas Trangez , Caml-list Content-Type: multipart/alternative; boundary=001a11397ec0c765b704fd0baaaf Subject: Re: [Caml-list] Strange interaction between recursive modules, GADT exhaustiveness checking and type-checking? --001a11397ec0c765b704fd0baaaf Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On 29 June 2014 15:49, Gr=C3=A9goire Henry wr= ote: > Your first example is a particular case where we could assume that > 'W.a' and 'W.b' are distinct. They are 'fully abstract types', they > have no inhabitants. They were introduced in current typing context > (and not imported from the signature of another module) and we known > they are distinct. > This has bitten me before as well. It seems to me that whether or not a type is abstract and whether or not it has any values should be essentially independent characteristics, but it seems impossible to state in a signature that a type has no constructors. So there's this property of types that you can't preserve across module boundaries. --001a11397ec0c765b704fd0baaaf Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On 2= 9 June 2014 15:49, Gr=C3=A9goire Henry <gregoire.henry@ocamlpro.= com> wrote:
Your first example is a particular case where we could assume that
'W.a' and 'W.b' are distinct. They are 'fully abstract = types', they
have no inhabitants. They were introduced in current typing context
(and not imported from the signature of another module) and we known
they are distinct.

This has bitten me b= efore as well. It seems to me that whether or not a type is abstract and wh= ether or not it has any values should be essentially independent characteri= stics, but it seems impossible to state in a signature that a type has no c= onstructors. So there's this property of types that you can't prese= rve across module boundaries.
--001a11397ec0c765b704fd0baaaf--