From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 A02127FC18 for ; Sun, 15 Feb 2015 15:47:45 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.213.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.213.181 as permitted sender) identity=mailfrom; client-ip=209.85.213.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-f181.google.com) identity=helo; client-ip=209.85.213.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ig0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BPAgB2sOBUlLXVVdFbg1haBIJ/riiFNYtchW8CgQcHQwEBAQEBARABAQEBBwsLCRIwhA0BAQQSEQQZARsdAQMMBgULDQICJgICIgERAQUBHAYTIod2AQMRDat+PjGLLoFrgneLQQoZJw1UhHIBAQEBBgEBAQEBFwEFDoETiWuEbQeCaIFCBZMPhWCBUI9zEiOBDAmCJByBUT0xAQGCQQEBAQ X-IPAS-Result: A0BPAgB2sOBUlLXVVdFbg1haBIJ/riiFNYtchW8CgQcHQwEBAQEBARABAQEBBwsLCRIwhA0BAQQSEQQZARsdAQMMBgULDQICJgICIgERAQUBHAYTIod2AQMRDat+PjGLLoFrgneLQQoZJw1UhHIBAQEBBgEBAQEBFwEFDoETiWuEbQeCaIFCBZMPhWCBUI9zEiOBDAmCJByBUT0xAQGCQQEBAQ X-IronPort-AV: E=Sophos;i="5.09,581,1418079600"; d="scan'208";a="100128196" Received: from mail-ig0-f181.google.com ([209.85.213.181]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 15 Feb 2015 15:47:44 +0100 Received: by mail-ig0-f181.google.com with SMTP id hn18so19268543igb.2 for ; Sun, 15 Feb 2015 06:47:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=+kYaZ+38Uf/aL+TKLFnfXCopw6Iw+kVD4YBatp4LNgg=; b=EJeP9B15o3/jOOqccVR/tknoQXxsDNY1Nd1dQyfNLh+WtGKWq6ngGMTF4OvaoUEPvL 7vdtu42KcnrRmRmxdzdMgwEtRjTmX1YYeDcIB2YKONVFtn8Ws9JGobZSfQ7KcXmR7qj+ 0c0EroMoHSM37kyuBfDRzW3ncS0aAi4n+nz9zy7j4vCtW3bAfn11qfPnyaLMXcXaPn3I by1QwwW2OqJ+b82o3eJVcdSll/KbiAXYqjpfKCemfZWF3p4wOYuKZI0OComtElOKw44O fgzNuDbwM7Ij2wbHc7NtWZuMD18vfYzGYtu2i9Ebb7tHqPYnOmv1Gg0sB6aUAzDNE/9y wlLg== X-Received: by 10.50.61.201 with SMTP id s9mr24105154igr.0.1424011663576; Sun, 15 Feb 2015 06:47:43 -0800 (PST) MIME-Version: 1.0 Received: by 10.36.13.195 with HTTP; Sun, 15 Feb 2015 06:47:03 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Sun, 15 Feb 2015 15:47:03 +0100 Message-ID: To: Nicolas Boulay Cc: OCaml Mailing List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] problem to use gadt 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