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 2E0487FC18 for ; Sun, 15 Feb 2015 21:17:51 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of nicolas.boulay@gmail.com) identity=pra; client-ip=209.85.213.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="nicolas.boulay@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of nicolas.boulay@gmail.com designates 209.85.213.174 as permitted sender) identity=mailfrom; client-ip=209.85.213.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="nicolas.boulay@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ig0-f174.google.com) identity=helo; client-ip=209.85.213.174; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="postmaster@mail-ig0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DoAgAf/uBUm67VVdFcg1haBIJ/vUuBcIZ6B0MBAQEBAQEQAQEBAQEGCwsJFC6EDAEBAQMBEhEEGQE4AQMBCwEFBQQHDSoCAiEBEgEFARwGEyKHdwMJCA2pMz4xiy6EYotZJw2FRgELARkBBQ6KfoJDhRmBQgWTD4QagUaBUIs5hDoSI4EVW4FJHIFRPTEBAYJBAQEB X-IPAS-Result: A0DoAgAf/uBUm67VVdFcg1haBIJ/vUuBcIZ6B0MBAQEBAQEQAQEBAQEGCwsJFC6EDAEBAQMBEhEEGQE4AQMBCwEFBQQHDSoCAiEBEgEFARwGEyKHdwMJCA2pMz4xiy6EYotZJw2FRgELARkBBQ6KfoJDhRmBQgWTD4QagUaBUIs5hDoSI4EVW4FJHIFRPTEBAYJBAQEB X-IronPort-AV: E=Sophos;i="5.09,582,1418079600"; d="scan'208";a="100142028" Received: from mail-ig0-f174.google.com ([209.85.213.174]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 15 Feb 2015 21:17:50 +0100 Received: by mail-ig0-f174.google.com with SMTP id b16so20147010igk.1 for ; Sun, 15 Feb 2015 12:17:48 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:date:message-id:subject :from:to:cc:content-type; bh=lvf1/l3geGJYoYdY1qKcKpwxXMovSo6UXNzz+B7INQ8=; b=r7xNzxc2SZUv3hOGiuLLheSX6r+8edwKZj1xEJSPC0rVcQdPmMg39Hs6LoybMNrtx7 1EjgVwTn8Gje4hfTu9NBXxO5mcvb9y8IncsoS6B6ULQ0Cs4Y3FTO0sM1OIDBWapW1Mqs k8xHM6/x+R97tlvrxi+TfSmyU8HsSrl4PS3l4b/vTmu8HA6TkmqofhWDp8AZhg8Itrl9 Ubg07c14Rcf0lB+SFIjywdQdb4q3Hd1yBgW2WugZ4dDVIhpSjRK71qxYk0l17OmojdsQ W5J5VfvLW5BO2bCBIDyuUnAYLDEUyhwdVRn1cuzac71MfOnBH0avHdYojTbbtSjoDZzk jZRQ== MIME-Version: 1.0 X-Received: by 10.50.43.198 with SMTP id y6mr17751623igl.16.1424031468799; Sun, 15 Feb 2015 12:17:48 -0800 (PST) Sender: nicolas.boulay@gmail.com Received: by 10.50.132.194 with HTTP; Sun, 15 Feb 2015 12:17:48 -0800 (PST) In-Reply-To: References: Date: Sun, 15 Feb 2015 21:17:48 +0100 X-Google-Sender-Auth: Cqqgr8I0KEZhNeMdOb2VDLyQE8k Message-ID: From: Nicolas Boulay To: Gabriel Scherer Cc: OCaml Mailing List Content-Type: multipart/alternative; boundary=089e01537a96d8ce4d050f262928 X-Validation-by: nicolas@boulay.name Subject: Re: [Caml-list] problem to use gadt --089e01537a96d8ce4d050f262928 Content-Type: text/plain; charset=UTF-8 It will not work with a "And". | And : 'a t * 'a t -> 'a t let aa = And ((Int || Float), Int) (*won't compile, int t != any t*) 2015-02-15 15:47 GMT+01:00 Gabriel Scherer : > The typing rule for Or is rather weird: any type can be used as the > result type, which is non-standard. You could define a dummy type > "any" > > type any = Any > > [...] > > | Or : _ t * _ t -> any t > > and the output type of Or wouldn't be polymorphic anymore, so the > value restriction ( > http://caml.inria.fr/resources/doc/faq/core.en.html#weak-type-variables > ) wouldn't be a problem anymore. > > On Sun, Feb 15, 2015 at 2:35 PM, Nicolas Boulay > wrote: > > I try to define my own type system using gadt. But it seems that is > complex > > to mix both type system : mine and the ocaml one. > > > > This tiny example did not compile: > > > > type _ t = > > | Or: _ t * _ t -> _ t > > | Int : int t > > | Float : float t > > > > let a = Or (Int, Float) (*is ok*) > > > > let (||) a b = Or (a, b) > > > > let aa = Int || Float (*Error: '_a t, contains type variable that cannot > be > > generalized*) > > > > Using an operator make a difference. But how to exprime "don't care" if a > > choice between 2 types is not possible to be define. It could be nice if > > "('a | 'b) t" worked :) Should i use normal sum type, and make all type > > check by a function ? > > > > Nicolas Boulay > --089e01537a96d8ce4d050f262928 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
It will not work with a "And".

| And= : 'a t * 'a t -> 'a t
let aa =3D And ((Int || Floa= t), Int) (*won't compile, int t !=3D any t*)

2015-02-15 15:47 GMT+01:00 Gabriel Scherer = <gabriel.scherer@gmail.com>:
The typing rule for Or is rather weird: any type can be used = as the
result type, which is non-standard. You could define a dummy type
"any"

=C2=A0 type any =3D Any

=C2=A0 [...]

=C2=A0 | Or : _ t * _ t -> any t

and the output type of Or wouldn't be polymorphic anymore, so the
value restriction (
http://caml.inria.fr/resources/doc/faq/core.en.h= tml#weak-type-variables
) wouldn't be a problem anymore.

On Sun, Feb 15, 2015 at 2:35 PM, Nicolas Boulay <nicolas@boulay.name> wrote:
> I try to define my own type system using gadt. But it seems that is co= mplex
> to mix both type system : mine and the ocaml one.
>
> This tiny example did not compile:
>
> type _ t =3D
>=C2=A0 | Or: _ t * _ t -> _ t
>=C2=A0 | Int : int t
>=C2=A0 | Float : float t
>
> let a =3D Or (Int, Float)=C2=A0 (*is ok*)
>
> let (||)=C2=A0 a b =3D Or (a, b)
>
> let aa =3D Int || Float (*Error: '_a t, contains type variable tha= t cannot be
> generalized*)
>
> Using an operator make a difference. But how to exprime "don'= t care" if a
> choice between 2 types is not possible to be define.=C2=A0 It could be= nice if
> "('a | 'b) t" worked :) Should i use normal sum type= , and make all type
> check by a function ?
>
> Nicolas Boulay

--089e01537a96d8ce4d050f262928--