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 E04B17FC18 for ; Sun, 15 Feb 2015 21:16:20 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nicolas.boulay@gmail.com) identity=pra; client-ip=209.85.213.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="nicolas.boulay@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of nicolas.boulay@gmail.com designates 209.85.213.169 as permitted sender) identity=mailfrom; client-ip=209.85.213.169; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ig0-f169.google.com) identity=helo; client-ip=209.85.213.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="postmaster@mail-ig0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AyAgAq/uBUlKnVVdFchDIEgn+8XYJSAYcFB0MBAQEBAQEQAQEBAQcLCwkSMIQMAQEBAwEBAg8RBBkBOAEDAQsBBQUEBwMKKgICIhIBBQEcBhMIEgiHdwMJCKlAPjGLLoRii1onDYVGAQEIAgEZAQUOin6HXIFCBY1MiyOBGI43gXQSI4EVW4FJHIFRPTGCQwEBAQ X-IPAS-Result: A0AyAgAq/uBUlKnVVdFchDIEgn+8XYJSAYcFB0MBAQEBAQEQAQEBAQcLCwkSMIQMAQEBAwEBAg8RBBkBOAEDAQsBBQUEBwMKKgICIhIBBQEcBhMIEgiHdwMJCKlAPjGLLoRii1onDYVGAQEIAgEZAQUOin6HXIFCBY1MiyOBGI43gXQSI4EVW4FJHIFRPTGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.09,582,1418079600"; d="scan'208";a="121853297" Received: from mail-ig0-f169.google.com ([209.85.213.169]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 15 Feb 2015 21:16:20 +0100 Received: by mail-ig0-f169.google.com with SMTP id hl2so28618869igb.0 for ; Sun, 15 Feb 2015 12:16:18 -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=glkrC3wjEm+GbcPL95Fpd2LtdjG8E9Dv55KBCpU6VXk=; b=LWFQNPQ8XIa4dnCiOE+7IIj6kmx3tkAa/x3szxaYvQYuOt3gp49/Sqpv+u5VM3w5JK fJv675wMqoALrsyO9BqXVw3wtHee0nt/fRbN8/9Nsw5CvoljaBfcu2zh7zCAfDzhdP4G mJaGUW32slWhSy/w/nlrumZwyMbDLrKSYEzDHT5ddO6ELDJUU+5x3q2ko/GF83NiaJM6 0iRm9SYujsR0awFbtUonHoA7hLYDyJuHgXo56tQ/PSdRvA5MQREKYLL1s9j8QHYGMMih KHZiPhcy5EUHZp67ZupBaWuHl9eIwD54Te+hu0ywz5go6IeqwzV7Tlw+9QG9xOMwBYjB 0Kqg== MIME-Version: 1.0 X-Received: by 10.43.67.3 with SMTP id xs3mr25876626icb.39.1424031378907; Sun, 15 Feb 2015 12:16:18 -0800 (PST) Sender: nicolas.boulay@gmail.com Received: by 10.50.132.194 with HTTP; Sun, 15 Feb 2015 12:16:18 -0800 (PST) In-Reply-To: References: Date: Sun, 15 Feb 2015 21:16:18 +0100 X-Google-Sender-Auth: vRHLlL6K6UvT0FcqB0yaF2-FXTY Message-ID: From: Nicolas Boulay To: David Allsopp Cc: OCaml Mailing List Content-Type: multipart/alternative; boundary=001a11c2162e7d288f050f262488 X-Validation-by: nicolas@boulay.name Subject: Re: [Caml-list] problem to use gadt --001a11c2162e7d288f050f262488 Content-Type: text/plain; charset=UTF-8 2015-02-15 15:44 GMT+01:00 David Allsopp : > 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 > > Is this definitely what you mean - the "_" is not itself a distinct type > variable so all three underscores in this instance are different types. cf > the signature of the constructor: > > Or : 'b t * 'c -> 'a t > > > | Int : int t > > | Float : float t > > > > let a = Or (Int, Float) (*is ok*) > > But again, does it have the type you mean, in this case 'a t? > > > let (||) a b = Or (a, b) > > let aa = Int || Float (*Error: '_a t, contains type variable that cannot > be generalized*) > > This is a consequence of the value restriction, I think. > > > 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 ? > > So you're saying that you don't care what the type of the two halves of an > Or is? I don't see the problem you're trying to solve, but I wonder if your > issue is that you need to pick a concrete type representation for the Or > constructor. For example, does > > Or : _ t * _t -> unit t > > solve your problem? > > Not really. "t" is only a part of my complete type. It also have an "And" | And : 'a t * 'a t -> 'a t This "and" works well for "Float or Int" but not for "Or". let aa = And ((Int || Float), Int) (*won't compile, int t != any t*) > HTH, > > > David > --001a11c2162e7d288f050f262488 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable


2015-02-15 15:44 GMT+01:00 David Allsopp <dra-news@metastack.com= >:
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 oc= aml one.
>
> This tiny example did not compile:
> type _ t =3D
>=C2=A0 | Or: _ t * _ t -> _ t

Is this definitely what you mean - the "_" is not itself a= distinct type variable so all three underscores in this instance are diffe= rent types. cf the signature of the constructor:

Or : 'b t * 'c -> 'a t

>=C2=A0 | Int : int t
> =C2=A0| Float : float t
>
> let a =3D Or (Int, Float)=C2=A0 (*is ok*)

But again, does it have the type you mean, in this case 'a t?

> 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*)

This is a consequence of the value restriction, I think.

> 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 cou= ld
> be nice if "('a | 'b) t" worked :) Should i use norm= al sum type, and
> make all type check by a function ?

So you're saying that you don't care what the type of the tw= o halves of an Or is? I don't see the problem you're trying to solv= e, but I wonder if your issue is that you need to pick a concrete type repr= esentation for the Or constructor. For example, does

Or : _ t * _t -> unit t

solve your problem?


Not really.

"t&= quot; is only a part of my complete type. It also have an "And"
| And : 'a t * 'a t -> 'a t

This "and" works well for "Float or Int" but not for= "Or".

let aa =3D And ((Int || Float), Int) (*w= on't compile, int t !=3D any t*)
=C2=A0
HTH,


David

--001a11c2162e7d288f050f262488--