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 3DE797FC24 for ; Tue, 20 Oct 2015 13:58:01 +0200 (CEST) IronPort-PHdr: 9a23:CfPx0hestlfMQcOWGXyW04GdlGMj4u6mDksu8pMizoh2WeGdxc+6Zx7h7PlgxGXEQZ/co6odzbGG7ua4ASdavd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcWLKF8UzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQza7XIZViASkwFUKwnD9hDzGJnr9mPBrutn3zLSEMn3SqgzRDCl9O8/UxLsiSAfMCMR/2Tei8g2h6Ve9kGPvRt6lqvVY4GcNf42W6rbcckLRmtHFpJUXipNGJK/bo0nDvEZJ+9D6ZPg8Qhd5SCiDBWhUbu8ggRDgWX7iOhji7ws Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mandrykin@ispras.ru; spf=None smtp.mailfrom=mandrykin@ispras.ru; spf=None smtp.helo=postmaster@smtp.ispras.ru Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.79; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=mailfrom; client-ip=83.149.199.79; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp.ispras.ru) identity=helo; client-ip=83.149.199.79; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="postmaster@smtp.ispras.ru"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0D2DADaKyZW/0/HlVNVCSgBgw1Ub4UOr1GLJR2DF4JqAoE9PBABAQEBAQEBAYEJgiaCCAEBBCcTPxALGAkVEA8BRwYBEog0xAMBAQEBAQUBAQEBH4t1hDEpMweELgWOA4ghhRmJXkiGaI8qg284K4QGb4VnAQEB X-IPAS-Result: A0D2DADaKyZW/0/HlVNVCSgBgw1Ub4UOr1GLJR2DF4JqAoE9PBABAQEBAQEBAYEJgiaCCAEBBCcTPxALGAkVEA8BRwYBEog0xAMBAQEBAQUBAQEBH4t1hDEpMweELgWOA4ghhRmJXkiGaI8qg284K4QGb4VnAQEB X-IronPort-AV: E=Sophos;i="5.17,707,1437429600"; d="scan'208";a="183626950" Received: from smtp.ispras.ru ([83.149.199.79]) by mail2-smtp-roc.national.inria.fr with ESMTP; 20 Oct 2015 13:57:59 +0200 Received: from molnar.localnet (unknown [83.149.199.91]) by smtp.ispras.ru (Postfix) with ESMTP id DBF89204FF; Tue, 20 Oct 2015 14:57:56 +0300 (MSK) From: Mikhail Mandrykin To: caml-list@inria.fr, Spiros Eliopoulos Cc: Jeremy Yallop Date: Tue, 20 Oct 2015 14:57:56 +0300 Message-ID: <2885279.d7QpSRfKLJ@molnar> User-Agent: KMail/4.14.6 (Linux/3.19.0-30-generic; KDE/4.14.6; x86_64; ; ) In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 7Bit Content-Type: text/plain; charset="us-ascii" Subject: Re: [Caml-list] "map"-ing parameterized class types On Monday, October 19, 2015 04:15:54 PM Spiros Eliopoulos wrote: > Thank, Jeremy, for the great explanation and possible work around. > Unfortunately for me, the workaround won't be possible to use for the > js_of_ocaml use case I have in mind. At least not without sprinkling > Obj.magic everywhere, which is what I'm trying to avoid. > > Based on your workaround, I thought I might be able to create my own > workaround with code that looked something like this: > > module rec R : sig > class type ['a] container1 = object > method map : ('a -> 'b) -> 'b R.container2 > end > class type ['a] container2 = object > method op : 'a R.container1 > end > end = struct > ... > end > > But of course the type system complained that: > > Error: In the definition of R.container2, type > 'b R.container1 > should be > 'a R.container1 > > I thought this might be for a different than the one you mentioned, but > upon further reflection and a single unrolling of the types, it seems to be > the regular type constraint that's causing this error as well. It seems this is essentially not the workaround that was pointed out, as the suggestion was: >> One approach is to > > arrange things so that the recursion passes through a *non-structural > > type*, such as a variant or record. And an object type 'a container2 is a structural type. As far as I understand, the semantics for type-checking of structural type abbreviations is the same as if all those abbreviations were expanded. So introducing a new class ['a] container2 doesn't help, because its corresponding object type ends up being expanded while type-checking ['a] container1 anyway and leads to essentially the same error. The regularity restriction seems to also arise from the same expansion semantics where we would need to infinitely expand the structural type abbreviation while checking itself and therefore would be unable to write recursive structural types altogether, but the issue is addressed by replacing the whole abbreviated type application with a type variable e.g. 'a container1 = 'self and using this 'self in place of all regular self-references. Thus the type can remain structural (it's still possible to write it down without naming it) despite the self-references e.g. ( < get : 'a; map : 'self > as 'self). For irregular self-references this doesn't work (if 'a container = 'self then what's 'b container or how to designate it to avoid infinite expansion?). Just in case an another possible work-around would be to use an abstract type instead of a concrete nominal type as a proxy. This can be a little bit more suitable as an abstract type can be later bound to the same structural type and wrapping/unwrapping would become identity in the implementation. This is more heavyweight, though, e.g: module type S = sig type 'a c' val new_c : 'a -> 'a c' end module rec F' : functor (M : S) -> sig class ['a] c : 'a -> object method get : 'a method map : 'b. ('a -> 'b) -> 'b M.c' end end = functor (M : S) -> struct class ['a] c (a : 'a) = object method get = a method map : 'b. (_ -> 'b) -> 'b M.c' = fun f -> M.new_c (f a) end end module rec F : sig type 'a c' class ['a] c : 'a -> object method get : 'a method map : 'b. ('a -> 'b) -> 'b F.c' end val new_c : 'a -> 'a F.c' val self_cast : 'a c' -> 'a c end = struct module F' = F'(F) class ['a] c = ['a] F'.c type 'a c' = 'a c let new_c a = new F.c a let self_cast (x : 'a c') = (x : 'a c) end let () = let c1 = new F.c 1 in Printf.eprintf "%d\n" c1#get; let c2 = F.self_cast @@ c1#map (string_of_int) in Printf.eprintf "%s\n" c2#get Here F.self_cast is actually an identity function an is only used to help type-checking. -- Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru