From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1B1EGgo020664 for ; Sat, 11 Feb 2012 02:14:16 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4EAH3ANU+FBoIF/2dsb2JhbABDhRCrZoFyAQEEASMdAwE1AQEDCwsaAhgOAgJXBogPpWJtg0GOJAEGgS+KJBsKBgUCBAcCHQEDBwEBEhSDGAVCDIJ7M2OIS4xpknM X-IronPort-AV: E=Sophos;i="4.73,399,1325458800"; d="scan'208";a="143796135" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 11 Feb 2012 02:14:10 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id C9CEF62B9; Sat, 11 Feb 2012 10:14:06 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172.math.nagoya-u.ac.jp [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 8C8E639A2; Sat, 11 Feb 2012 10:14:06 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=SC71PXagAZ8lnluwjHuoxRlfb2w=; b=1ca6N6QEa8oHZ4pRJ8yYWdgJ43t3 Z0JZa1LMEhuV5wRVYG3PJJEy1yDVR1mvSjhhCCoqs7jbdqWUnAOKMEzB3DW/ZQA9 FpS41FGz0ZkY+E4r+vnNvq28385DF9J9y0QON+2YnRlwz0XdtbMxzskcKT3lHXH+ j7+gKQPe+UvUvV8= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=cov9AHGRg9Krw2Y5XyiHzThXDtix4/z1DYxJuNHYpdi19SkVYPuwNj2OUbnlePeuCuiwbyGK9d1+M3nGixMVeqnVvtGtrqZdhXzzwdSClj3D5x1jhRjrMnRWWzzexoI8w+fDThwxTWJE8skVgH0+x/dBWodq2UTT8vTsqaisRl4=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 5806F396B; Sat, 11 Feb 2012 10:14:06 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: Date: Sat, 11 Feb 2012 10:14:05 +0900 Cc: caml-list@inria.fr Message-Id: References: <2FA31185-B4C7-48D3-8C3C-771756CB26AA@math.nagoya-u.ac.jp> To: =?utf-8?Q?Milan_Stanojevi=C4=87?= X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q1B1EGgo020664 Subject: Re: [Caml-list] polymorphic variants in match statements On 2012/02/11, at 7:20, Milan Stanojević wrote: > 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? Actually, this is not directly related. The problem here is with type inference of recursive types. To do that, we need to do type inference on (possibly infinite) recursive trees. This is easy for regular trees (which can be represent as a directed graph), as the usual algorithm for first-order unification works. So what ocaml does is building such a regular tree on the fly, by creating a back edge to a previous ['a t] node when it meets another ['b t] node below it. So for instance, with definition type 'a t = [ `A of 'a | `B of 'a t ] the type [int t] would expand to ([`A of int | `B of 'r] as 'r) However, for this to work, any occurrence of t inside its own definition should have identical parameters. Hence the enforced restriction. Jacques Garrigue