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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 89C447EE6B for ; Sun, 1 Dec 2013 22:34:02 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of dboulytchev@gmail.com) identity=pra; client-ip=209.85.215.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dboulytchev@gmail.com"; x-sender="dboulytchev@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of dboulytchev@gmail.com designates 209.85.215.54 as permitted sender) identity=mailfrom; client-ip=209.85.215.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dboulytchev@gmail.com"; x-sender="dboulytchev@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-la0-f54.google.com) identity=helo; client-ip=209.85.215.54; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dboulytchev@gmail.com"; x-sender="postmaster@mail-la0-f54.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsACAEyqm1LRVdc2lGdsb2JhbABZjGixGhYOAQEBAQcLCwkSKoJTGQEbHAIDEhAWFhgDAgECARERAQUBIg0IAQEXh1MBAw8EAZ9zgwWMWYMJg3AKGScNZIZhAQUMkzYDiTyGdYExhjKGRYlhQYJogXI X-IPAS-Result: AsACAEyqm1LRVdc2lGdsb2JhbABZjGixGhYOAQEBAQcLCwkSKoJTGQEbHAIDEhAWFhgDAgECARERAQUBIg0IAQEXh1MBAw8EAZ9zgwWMWYMJg3AKGScNZIZhAQUMkzYDiTyGdYExhjKGRYlhQYJogXI X-IronPort-AV: E=Sophos;i="4.93,807,1378850400"; d="ml'?scan'208";a="38811001" Received: from mail-la0-f54.google.com ([209.85.215.54]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 01 Dec 2013 22:34:01 +0100 Received: by mail-la0-f54.google.com with SMTP id b8so1727514lan.41 for ; Sun, 01 Dec 2013 13:34:01 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=message-id:date:from:user-agent:mime-version:to:subject :content-type; bh=XTSv+MfTZXtP9n1MDCMMcixAt0lxa5vMBNsFaOsZRHY=; b=V6VWFOelSCFPwyjxteIToYTmArqdTpQqrkpgd/aq5My30ygW/9xNuv6R40FGLUw2Eq 9egYEGadUQkU9SV7gw7AptbPIwHZgChXlD+aeEu13KBta4UgCwFLouYOH6Yd/YXQq9g1 87bwv1p1ex7rJrN0xqyTsSt2jvPLuCLqtqm2V2ivgiMgs9OHl3DeIYczPA4X5v9GLY+J 5WsAXiq3blWKo29MhCl2g5payJLb7JUxxhc9NPcgKFLVVHz91njReX6sNPKN/pgy6c6j 9zhR7IHsY6hLZBbHZtI8pMKsBZVbxOd2bTlwlIRhWM+hwMVxFnz8wgnozV8L0/kIbRy4 aLXQ== X-Received: by 10.152.184.35 with SMTP id er3mr15822lac.23.1385933640920; Sun, 01 Dec 2013 13:34:00 -0800 (PST) Received: from [192.168.1.76] ([89.112.60.68]) by mx.google.com with ESMTPSA id r10sm72470816lag.7.2013.12.01.13.33.59 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Sun, 01 Dec 2013 13:33:59 -0800 (PST) Message-ID: <529BAB43.3080105@gmail.com> Date: Mon, 02 Dec 2013 01:33:55 +0400 From: Dmitri Boulytchev User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.1 MIME-Version: 1.0 To: caml-list Content-Type: multipart/mixed; boundary="------------040503090003030009020406" Subject: [Caml-list] Confusing behaviour of type inference for polymorphic classes. This is a multi-part message in MIME format. --------------040503090003030009020406 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Hello everyone, 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 Perhaps some explicit annotation is needed here (like that for the polymorphic recursion for functions). I found the following workaround: first we abstract the instance creation ("new m") away: class ['a, 'b, 'ta, 'tb] m' f = 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, (f ())#t fb fa bat) | B a -> B (fa a) end which gives us the unconstrained type class ['a, 'b, 'ta, 'tb] m' : (unit -> < t : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) t; .. >) -> object method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t end Then we construct the instance creation explicitly polymorphic function: let rec f : 'a 'b 'ta 'tb . unit -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t> = fun () -> new m' f and finally the class we're looking for: class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] m' f The complete annotated source file is attached. This workaround however does not solve everything: we cannot actually inherit from the m since it calls hardcoded "new m"; we should inherit from m' (with additional parameter) instead and "tie the knot" on the toplevel. Are there better solutions? Please help :) Best regards, Dmitry Boulytchev, St.Petersburg State University, Russia. --------------040503090003030009020406 Content-Type: text/x-ocaml; name="sample.ml" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="sample.ml" type ('a, 'b) t = A of 'a * ('b, 'a) t | B of 'a (* The initial definition 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 gives us the following type: 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 *) (* The modified version with the "new" abstracted away: *) class ['a, 'b, 'ta, 'tb] m' f = 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, (f ())#t fb fa bat) | B a -> B (fa a) end (* Inferred type with no artificial constraints: class ['a, 'b, 'ta, 'tb] m' : (unit -> < t : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) t; .. >) -> object method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t end *) (* Instance creation function: *) let rec f : 'a 'b 'ta 'tb . unit -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t> = fun () -> new m' f class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] m' f (* Ok now: class ['a, 'b, 'ta, 'tb] m' : ['a, 'b, 'ta, 'tb] m *) --------------040503090003030009020406--