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 5F6BD7EE6D for ; Mon, 2 Dec 2013 15:41:07 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.15.14; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=mailfrom; client-ip=212.227.15.14; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.15.14; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AigCANqanFLU4w8OnGdsb2JhbABZtyWFToEkFg4BAQEBAQYNCQkUKIIlAQEEAScTPwULCw4KCSUPBSghLodTAQwKt3ofiAOPCAeDIIETA5gThi8Sjn0 X-IPAS-Result: AigCANqanFLU4w8OnGdsb2JhbABZtyWFToEkFg4BAQEBAQYNCQkUKIIlAQEEAScTPwULCw4KCSUPBSghLodTAQwKt3ofiAOPCAeDIIETA5gThi8Sjn0 X-IronPort-AV: E=Sophos;i="4.93,811,1378850400"; d="scan'208";a="46540940" Received: from mout.web.de ([212.227.15.14]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 02 Dec 2013 15:41:03 +0100 Received: from frosties.localnet ([37.49.32.119]) by smtp.web.de (mrweb103) with ESMTPSA (Nemesis) id 0MRCjL-1WBVpq2qqN-00UYF2 for ; Mon, 02 Dec 2013 15:41:01 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.80) (envelope-from ) id 1VnUgH-0006Tz-2S; Mon, 02 Dec 2013 15:41:01 +0100 Date: Mon, 2 Dec 2013 15:41:01 +0100 From: Goswin von Brederlow To: Dmitri Boulytchev Cc: caml-list Message-ID: <20131202144100.GA24602@frosties> References: <529BAB43.3080105@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <529BAB43.3080105@gmail.com> User-Agent: Mutt/1.5.21 (2010-09-15) X-Provags-ID: V03:K0:pWRJOOU/XB0UgF+24dc8axznr5XbXHupa/1XgL+2PYWzexfS/9z Kmy0xtdpRPPWl/sny0JLzX4vewWjVPVLiotD4peGdrF8vsZ1Yr0CYABCWPv1Y4k/ZuJYxJ0 GwvyR16gaJy+CTgy+lZh/XzmKmpj4KR8bH1OHyFv5aMJdd2b6rWjoW+GYxnRcTRuKI37kAi z4ooPP5+GErwheA1d+UfA== Subject: Re: [Caml-list] Confusing behaviour of type inference for polymorphic classes. 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