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 A99187EE6B for ; Mon, 2 Dec 2013 16:05:53 +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.44; 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.44 as permitted sender) identity=mailfrom; client-ip=209.85.215.44; 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-f44.google.com) identity=helo; client-ip=209.85.215.44; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dboulytchev@gmail.com"; x-sender="postmaster@mail-la0-f44.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AusFAGShnFLRVdcslWdsb2JhbABZvG8CAoElFg4BAQEBBw0JCRIqgiUBAQQBJxEIARscAQEDAQsGBQsNCRYPCQMCAQIBEREBBQEcBg0BBwEBF4dTAQMJBgQBo2yMWYMJhDMKGScNZIZhAQUMjkkzB4QzA4k8jliGRYlhQYRa X-IPAS-Result: AusFAGShnFLRVdcslWdsb2JhbABZvG8CAoElFg4BAQEBBw0JCRIqgiUBAQQBJxEIARscAQEDAQsGBQsNCRYPCQMCAQIBEREBBQEcBg0BBwEBF4dTAQMJBgQBo2yMWYMJhDMKGScNZIZhAQUMjkkzB4QzA4k8jliGRYlhQYRa X-IronPort-AV: E=Sophos;i="4.93,811,1378850400"; d="scan'208";a="38940573" Received: from mail-la0-f44.google.com ([209.85.215.44]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Dec 2013 16:05:53 +0100 Received: by mail-la0-f44.google.com with SMTP id ep20so8281243lab.17 for ; Mon, 02 Dec 2013 07:05:52 -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:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; bh=OSj2F4A6/9wUADKxUjwv68K81rOlDkFbMeesYwUvWEM=; b=tpc+eJuKnl5TfUm9BrEpP9M+Hw7y2apidlaLXZVRU9I7UzFcZyzwDxyGhGE7dUU2HZ ZKFwAl+VCdkmOCrWdw9806v0jFjeoSIpIFTC998eRjnQHuL9ILM5VnCXipk9SMi08tLn gj3MCKAz+ZU03zO1ohFB7cmX6idbl0jWxaZ5hUiIuhqYhinU8UJF+41cUDpDnlXMx0Jr GsRYkHq2+IeSMI0VhXCAPRZ+b4OSjkRBBSXljgDNTrMetunM/EOMuen8WyBBeDhpOSO6 up3GG6FuRhGsU5saujCEg4yMJnzVcBrs/CL79n4JsHjkyTAW1YV0RJGrCLsAK6Ow3wjP cfgQ== X-Received: by 10.112.201.167 with SMTP id kb7mr1205492lbc.32.1385996752174; Mon, 02 Dec 2013 07:05:52 -0800 (PST) Received: from [192.168.1.76] ([89.112.60.68]) by mx.google.com with ESMTPSA id rb4sm3506421lbb.1.2013.12.02.07.05.50 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Mon, 02 Dec 2013 07:05:51 -0800 (PST) Message-ID: <529CA1C9.2050203@gmail.com> Date: Mon, 02 Dec 2013 19:05:45 +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: Goswin von Brederlow CC: caml-list References: <529BAB43.3080105@gmail.com> <20131202144100.GA24602@frosties> In-Reply-To: <20131202144100.GA24602@frosties> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Confusing behaviour of type inference for polymorphic classes. > I think this is caused by the recursion. The type inference assumes > that the recursive call will have the same type as the parent. Since > you switch 'a and 'b in the recursive call the compiler inferes that > 'a == 'b. > I don't think we have a recursive call here since we call a method from *another* object. BR, DB > On Mon, Dec 02, 2013 at 01:33:55AM +0400, Dmitri Boulytchev wrote: >> 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 > I think this is caused by the recursion. The type inference assumes > that the recursive call will have the same type as the parent. Since > you switch 'a and 'b in the recursive call the compiler inferes that > 'a == 'b. > >> 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 :) > Try using a self type or #m but this might not be solvable. > >> Best regards, >> Dmitry Boulytchev, >> St.Petersburg State University, >> Russia. > MfG > Goswin >