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 5C6A87EE6B for ; Mon, 2 Dec 2013 16:24:10 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.212.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yallop@gmail.com designates 209.85.212.172 as permitted sender) identity=mailfrom; client-ip=209.85.212.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-wi0-f172.google.com) identity=helo; client-ip=209.85.212.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-wi0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ar8CAImlnFLRVdSslGdsb2JhbABZhAYMgnq1aYEdCBYOAQEBAQcLCwkSKoIlAQEEASMEGQEbHQEDAQsGBQsDCgICJgICIQEBEQEFARwGExqHVAEDCQajeYwGU4MJhDcKGScNZIZQEQEFDIEdi06CEQeCa4FIA5YpgWuMWoNMGCmEVTw X-IPAS-Result: Ar8CAImlnFLRVdSslGdsb2JhbABZhAYMgnq1aYEdCBYOAQEBAQcLCwkSKoIlAQEEASMEGQEbHQEDAQsGBQsDCgICJgICIQEBEQEFARwGExqHVAEDCQajeYwGU4MJhDcKGScNZIZQEQEFDIEdi06CEQeCa4FIA5YpgWuMWoNMGCmEVTw X-IronPort-AV: E=Sophos;i="4.93,811,1378850400"; d="scan'208";a="46550828" Received: from mail-wi0-f172.google.com ([209.85.212.172]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Dec 2013 16:24:09 +0100 Received: by mail-wi0-f172.google.com with SMTP id en1so4953133wid.11 for ; Mon, 02 Dec 2013 07:24:09 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=LQZDsRCjGC+SCEQG873LzVCza52zEQq2kXM1B83QXIM=; b=XavI13PzDMbXhhFVkBbAhIFTpGoCCyqBzzzzT36pRRLsb04aAZ64OgKde62AWNEGrI marWU4aYi8a51iPkgsJF5q8S8cizRrI3tXur0G303ALwhenSTU8l5i31KPUo5W5dhAvK edtryTSnuQToV87yb1kequDwP4ZSrGkZfWlxIUwvvIXOex+DjsVsqamORHK8LpIm/dmn 7GVA4SXJRqvkcGl4dPLVo1BTQhOWg21Ws7w9dtXIBDvUyBCl2dtLwkHSg4KIR4YGRyG7 E1CRuTwFzkM5e4OlTmZWWO7hBNYYavqmyg5+knWIv2oSz64dKZ1n6tJM6bLfuIAIgSYX ih/g== MIME-Version: 1.0 X-Received: by 10.180.12.70 with SMTP id w6mr18977164wib.4.1385997849714; Mon, 02 Dec 2013 07:24:09 -0800 (PST) Received: by 10.216.185.65 with HTTP; Mon, 2 Dec 2013 07:24:09 -0800 (PST) In-Reply-To: <529BAB43.3080105@gmail.com> References: <529BAB43.3080105@gmail.com> Date: Mon, 2 Dec 2013 15:24:09 +0000 Message-ID: From: Jeremy Yallop To: Dmitri Boulytchev Cc: caml-list Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Confusing behaviour of type inference for polymorphic classes. Hi Dmitri, On 1 December 2013 21:33, Dmitri Boulytchev wrote: > I stumbled on the following confusing behaviour of the type checker: > given the definitions > > type ('a, 'b) t = > A of 'a * ('b, 'a) t > | B of 'a > > class ['a, 'b, 'ta, 'tb] m = > object > method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t = > fun fa fb s -> > match s with > | A (a, bat) -> A (fa a, (new m)#t fb fa bat) > | B a -> B (fa a) > end > > the following type is inferred for the class m: > > class ['a, 'b, 'ta, 'c] m : > object > constraint 'b = 'a <--- why? > constraint 'c = 'ta <--- why? > method t : ('a -> 'ta) -> ('a -> 'ta) -> ('a, 'a) t -> ('ta, 'ta) t > end There's good news and bad news. The good news is that the problem can be solved for your particular example. The bad news is that the approach doesn't work in the general case. On to the details... First, let's get some definitions out of the way. A parameterised type definition "('a1, 'a2, ... 'an) t" is *regular* if all occurrences of "t" within its definition are instantiated with the parameters from the lhs of the '=' (i.e. it occurs exactly as "('a1, 'a2, ... 'an) t"). Here are some regular data types definitions: type 'a list = Nil | Cons of 'a * 'a listapproach type ('a, 'b) altlist = Nil | Cons of 'a * 'b * ('a, 'b) altlist In each of these the type constructor being defined is only instantiated with the exact parameter list from the lhs of the '='. In contrast, here are some non-regular data type definitions: type 'a nested = Empty | Branch of 'a * ('a * 'a) nested type ('a, 'len) vec = Nil : ('a, zero) vec | Cons : 'a * ('a, 'n) vec -> ('a, 'n succ) vec In each of these the type constructor being defined is instantiated with parameter lists that are different from the lhs of the definition: "('a * 'a) nested" is different from "'a nested" in the first case, and "('a, zero) vec" and "('a, 'n succ)" vec are different from "('a, 'len) vec" in the second case. The analogue of non-regular types for functions is polymorphic recursion. A function is *polymorphic-recursive* if some calls to the function in its own definition instantiate the type variables differently from the definition itself. Here's a polymorphic recursive function let rec depth : 'a. 'a nested -> int = function | Empty -> 0 | Branch (_, n) -> 1 + depth n The call to "depth" on the last line uses it at type "('a * 'a) nested -> int", which is different from the defined type "'a nested -> int". If you call "depth" on a value of type "int nested" of depth 3 then the recursive calls will have the following types: int nested -> int (int * int) nested -> int ((int * int) * (int * int)) nested -> int (((int * int) * (int * int)) * ((int * int) * (int * int))) nested -> int It's also worth noting that the type annotation can't be omitted, since polymorphic-recursive types can't be inferred, although they can be checked. In contrast, here's a function that's polymorphic and recursive but not polymorphic-recursive: let rec length : 'a. 'a list -> int = function | Nil -> 0 | Cons (_, l) -> 1 + length l In this case the call to "length" uses it at type "'a list -> int" -- just the same type as the definition. If you call "length" on a value of type "int list" of length 3 then the recursive calls will have the following types: int list -> int int list -> int int list -> int int list -> int In this case the type annotation is unnecessary, and if you omit it then OCaml will infer the same type, "'a list -> int". It'll probably come as no surprise that non-regular types and polymorphic recursion are closely related: traversals over non-regular types generally involve polymorphic recursion. In your example the type 't' is non-regular: it's defined to take parameters "('a, 'b)", but used in its definition as "('b, 'a) t": > type ('a, 'b) t = > A of 'a * ('b, 'a) t > | B of 'a Traversals over values of type "t" therefore need to be polymorphic-recursive. Since you've exposed the type parameters as class parameters you need the class type to be non-regular as well: you've defining "m" with parameters "['a, 'b, 'ta, 'tb]", but trying to instantiate it with parameters "['b, 'a, 'tb, 'ta]". This isn't possible in OCaml: class and object types (like other structural types such as polymorphic variants) can only be regular. The approach you're trying therefore won't work in general for defining traversals over non-regular types. As you've noted, you can work around the problem using open recursion and typing the knot yourself, but you lose the ability to subtype in the process. On to the good news. Unlike "nested" and "vec", your type "t" is only a little bit non-regular. The non-regularity is a simple flip of the type parameters, so a recursive traversal of a value of "t" involves calling the traversal function at the following types ('a, 'b) t -> 'result ('b, 'a) t -> 'result ('a, 'b) t -> 'result ('b, 'a) t -> 'result ... This gives us a clue as to how we might attack the typing problem. Unfolding the traversal methods one level gives us a pair of mutually-recursive methods, neither of which is polymorphic-recursive, and neither of which instantiates the class with different parameters: class ['a, 'b, 'ta, 'tb] m = object method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t = fun fa fb s -> match s with | A (a, bat) -> A (fa a, (new m)#t' fb fa bat) | B a -> B (fa a) method t' : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) t = fun fa fb s -> match s with | A (a, bat) -> A (fa a, (new m)#t fb fa bat) | B a -> B (fa a) end In fact, instead of repeatedly creating new instances you can now use a "self" binding, which will give you more scope for overriding behaviour with subtyping: class ['a, 'b, 'ta, 'tb] m = object (self) method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t = fun fa fb s -> match s with | A (a, bat) -> A (fa a, self#t' fb fa bat) | B a -> B (fa a) method t' : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) t = fun fa fb s -> match s with | A (a, bat) -> A (fa a, self#t fb fa bat) | B a -> B (fa a) end Of course, unfolding in this way doesn't work for general non-regular types, since unfolding "nested" or "vec" would go on forever. You might also consider unfolding the type "t" itself, at which point traversals become more straightforward. If you can expand the definition of "t" to a pair of mutually recursive (and regular!) types: type ('a, 'b) t = A of 'a * ('a, 'b) s | B of 'a and ('a, 'b) s = C of 'b * ('a, 'b) t | D of 'b then you can use your current approach without any changes. Hope this helps, Jeremy.