From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1AMKBMM017717 for ; Fri, 10 Feb 2012 23:20:11 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AusAAC2XNU9KfVM2kGdsb2JhbABDDgiEfqpOCCIBAQEBCQkNBxQEI4FyAQEBBBICDwQZARsdAQMMBgMCCw0CAiYCAiEBAREBBQEcBhMih2OdVQqLJkuCcIR6P4ELAgULgSSHC4MvBQoDAwUCBAMECgECBwUGAQMChxOBFgSISYxnixCDFT2DS1U X-IronPort-AV: E=Sophos;i="4.73,398,1325458800"; d="scan'208";a="130934399" Received: from mail-ee0-f54.google.com ([74.125.83.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Feb 2012 23:20:11 +0100 Received: by eekb47 with SMTP id b47so1290679eek.27 for ; Fri, 10 Feb 2012 14:20:11 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=qYpqtPtNs/bvwO+HQYqVyBjsOHTimlSdS8VkTYRh73M=; b=u15nvOigomH+8HM94M3yZYzpdIvPCWDzMkosLahtDRi/72piCUJbDI8IWmiWN6g9Tc 6/qgGik0X2QiIaQgW1W5vu2rF2dP9PdUt+1joH6Xk3ENTYbXuyhyf5zjxVcNIhjfijIG 0mAOl6vXBAvoRWYSIfhMBmwfJbSm+er0opNpg= MIME-Version: 1.0 Received: by 10.213.2.74 with SMTP id 10mr1361901ebi.11.1328912409604; Fri, 10 Feb 2012 14:20:09 -0800 (PST) Received: by 10.14.27.200 with HTTP; Fri, 10 Feb 2012 14:20:09 -0800 (PST) In-Reply-To: References: <2FA31185-B4C7-48D3-8C3C-771756CB26AA@math.nagoya-u.ac.jp> Date: Fri, 10 Feb 2012 17:20:09 -0500 Message-ID: From: =?UTF-8?Q?Milan_Stanojevi=C4=87?= To: Jacques Garrigue Cc: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q1AMKBMM017717 Subject: Re: [Caml-list] polymorphic variants in match statements A small follow-up question Polymorphic variant types are not allowed to have non-regular recursion, i.e. the following type definition gives an error type 'a t = [ `A of 'a | `B of ('a * 'a) t ] Error: In the definition of t, type ('a * 'a) t should be 'a t I guess the reason why this is not allowed has something to do with our previous discussion, but I'm struggling to connect the dots. Can you please explain this restriction? 2012/1/24 Milan Stanojević : > Thanks a lot, Jacques! > This helped my understanding a lot. > > I only wonder if maybe this (and other type checking issues) could be > documented in a better way. For example I couldn't find any links to > your papers on OCaml website > > > 2012/1/23 Jacques Garrigue : >> On 2012/01/24, at 9:53, Milan Stanojević wrote: >> >>> Hi, we're trying to understand the type inference with polymorphic >>> variants in match statements. This is a simplification of an actual >>> case that happened in practice. >>> >>> 1) >>> let f i a = >>>  match i, a with >>>  | true, `A -> `B >>>  | false, x -> x >>> >>> fails with >>> File "foo.ml", line 4, characters 16-17: >>> Error: This expression has type [< `A ] >>>       but an expression was expected of type [> `B ] >>>       The first variant type does not allow tag(s) `B >>> >>> 2) changing false to _ >>> let f i a = >>>  match i, a with >>>  | true, `A -> `B >>>  | _, x -> x >>> >>> this succeeds with >>> val f : bool -> ([> `A | `B ] as 'a) -> 'a >>> >>> 3) changing x in (1) to _ , and using a on the right side >>> let f i a = >>>  match i, a with >>>  | true, `A -> `B >>>  | false, _ -> a >>> >>> this fails in the same way as (1) >>> >>> 4) finally adding another case to match statement >>> let f i a = >>>  match i, a with >>>  | true, `A -> `B >>>  | false, x -> x >>>  | true, x -> x >>> >>> this succeeds with the same type as (2) >>> >>> >>> So it seems there is some interaction between type inference and >>> exhaustivnest of the match statements. >>> >>> Can someone shed some light on what is going on here? >> >> Indeed. The basic idea is to close variant types when leaving them >> open would make the pattern matching non-exhaustive. >> Here, if we assume that a has type [`A | `B], then the pattern-matching >> becomes non-exhaustive, so the type inferred is just [`A] >> (i.e. the list of all constructors appearing inside the patterns at this position). >> >> Actually, the theory is a bit more complicated, and the full details are >> in the following paper, but you should just expect the above behavior >> in practice. >> >>        Typing deep pattern-matching in presence of polymorphic variants. >>        http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html >> >> Note that there is also another way to make (1) type, without adding >> new cases >> >>  let f i a = >>    match i, a with >>    | true, `A -> `B >>    | false, (`A as x) -> x;; >>  val f : bool -> [< `A ] -> [> `A | `B ] = >> >> Here we have removed the connection between a and the output, >> allowing `A to be combine with `B without changing the type of a. >> >> Hope this helps. >> >> Jacques Garrigue >>