Re: [Caml-list] "map"-ing parameterized class types

[Mikhail Mandrykin <mandrykin@ispras.ru>]

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