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 9C9167EC6E for ; Fri, 20 Dec 2013 00:47:31 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rathereasy@gmail.com) identity=pra; client-ip=209.85.160.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="rathereasy@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rathereasy@gmail.com designates 209.85.160.50 as permitted sender) identity=mailfrom; client-ip=209.85.160.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="rathereasy@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-pb0-f50.google.com) identity=helo; client-ip=209.85.160.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rathereasy@gmail.com"; x-sender="postmaster@mail-pb0-f50.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao0BACqFs1LRVaAym2dsb2JhbABZhAwMgwO2LYEOCBYOAQEBAQEGCwsJFCiCJQEBAQMBIx0BGxILAQMBCwYFBAcNKgICIQEBEQEFARwGE4dvAQMJCKVKjAdTgwmOBAoZJw1khhgRAQUMjHOBMREBUAeCboFIBIlDjGiBa4xag00YKYR1HoE1 X-IPAS-Result: Ao0BACqFs1LRVaAym2dsb2JhbABZhAwMgwO2LYEOCBYOAQEBAQEGCwsJFCiCJQEBAQMBIx0BGxILAQMBCwYFBAcNKgICIQEBEQEFARwGE4dvAQMJCKVKjAdTgwmOBAoZJw1khhgRAQUMjHOBMREBUAeCboFIBIlDjGiBa4xag00YKYR1HoE1 X-IronPort-AV: E=Sophos;i="4.95,516,1384297200"; d="scan'208";a="49787742" Received: from mail-pb0-f50.google.com ([209.85.160.50]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 20 Dec 2013 00:47:30 +0100 Received: by mail-pb0-f50.google.com with SMTP id rr13so1825387pbb.37 for ; Thu, 19 Dec 2013 15:47:29 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=sW/2APaXwj2/UQDbKuHlFceR5PsJEWf85y8H+CCc/LY=; b=nVY1Axs8Futq8+xERK+GI8jWUcd/RCJJ1c7yVPIBLDuTLTyrHsclbRICwDz/nQt1GY bW+e4rg8+OZl4ajaJpdRrwibAWUpsj/LnPSdEAz6rXrKZ1cGjfpH+emZAS49/0rWhK8c 5rAT3Cd+Hsxb26gHYQAj88ZTPhiZWcqTkJKax6dTQwg5gy6difHlZp0L+QdFYFdZ3+Dl 4RV9Qn8ListDy2Wtwv54LVJt5eKO5cQPc7Ebi0kvKfiShv5Rl1AI1RxqD2hSkTXjQHt0 TaADeLQZl04xZGbBzQSRqMwnttcrTcZwnCQOKr2qbU/VDHByZBviFsLhJhOoplKWELgV Elnw== MIME-Version: 1.0 X-Received: by 10.67.3.3 with SMTP id bs3mr4975114pad.46.1387496849254; Thu, 19 Dec 2013 15:47:29 -0800 (PST) Received: by 10.70.128.195 with HTTP; Thu, 19 Dec 2013 15:47:29 -0800 (PST) In-Reply-To: References: Date: Thu, 19 Dec 2013 18:47:29 -0500 Message-ID: From: Jacques Le Normand To: Gabriel Scherer Cc: Lukasz Stafiniak , =?ISO-8859-2?Q?Milan_Stanojevi=E6?= , Caml Content-Type: multipart/alternative; boundary=047d7b15afd3d3aea204edebc806 Subject: Re: [Caml-list] GADT definition --047d7b15afd3d3aea204edebc806 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable or type _ s =3D S On Thu, Dec 19, 2013 at 6:10 PM, Gabriel Scherer wrote: > type z > type _ s > > Don't use this kind of abstract type definition. Use instead (and export) > concrete definitions (even if you don't use their constructors for anythi= ng) > > type 'a s =3D S of 'a > (or just type 'a s =3D S) > > They have "better" injectivity properties. We've mentioned in on the > mailing-list a couple of time, and it's also the "easy take-away lesson" > from Jacques Garrigue talk at the OCaml workshop in September. > > > On Thu, Dec 19, 2013 at 11:35 PM, Lukasz Stafiniak wr= ote: > >> On Thu, Dec 19, 2013 at 11:27 PM, Milan Stanojevi=C4=87 wrote: >> >>> What version of ocaml are you using? It works for me on 4.00.1 >>> >>> OCaml 4.01.0 from OPAM. >> >> On Thu, Dec 19, 2013 at 5:21 PM, Lukasz Stafiniak >>> wrote: >>> > On Thu, Dec 19, 2013 at 11:20 PM, Lukasz Stafiniak >> > >>> > wrote: >>> >> >>> >> Sorry! I've spotted it reading the email. (I should read before >>> sending.) >>> >> >>> > No, that's not it. My question is still open. >>> >> >> > --047d7b15afd3d3aea204edebc806 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
or type _ s =3D S


=
On Thu, Dec 19, 2013 at 6:10 PM, Gabriel Scherer= <gabriel.scherer@gmail.com> wrote:
type= z
type _ s

Don't use this kin= d of abstract type definition. Use instead (and export) concrete definition= s (even if you don't use their constructors for anything)

type 'a s =3D S of 'a
(or just ty= pe 'a s =3D S)

They have "better" in= jectivity properties. We've mentioned in on the mailing-list a couple o= f time, and it's also the "easy take-away lesson" from Jacque= s Garrigue talk at the OCaml workshop in September.

On Thu, Dec 19, 2013 at 11:35 PM, Lukasz S= tafiniak <lukstafi@gmail.com> wrote:
=
On Thu, Dec 19, 2013 at 11:27 PM, Milan Sta= nojevi=C4=87 <milanst@gmail.com> wrote:
What version of ocaml are you using? It work= s for me on 4.00.1

=C2=A0OCaml 4.01.0 from O= PAM.

On Thu, Dec 19, 2013 at 5:21 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
> On Thu, Dec 19, 2013 at 11:20 PM, Lukasz Stafiniak <lukstafi@gmail.com>
> wrote:
>>
>> Sorry! I've spotted it reading the email. (I should read befor= e sending.)
>>
> No, that's not it. My question is still open.



--047d7b15afd3d3aea204edebc806--