[Caml-list] Locally abstract type with type parameters

[Caml-list] Locally abstract type with type parameters

[Dario Teixeira]

Hi,

Consider the signature LOGGER below, to be implemented by any module that
supposedly logs something wrapped under a custom monad:

  module type LOGGER =
  sig
      module Monad:
      sig
          type 'a t
          val return: 'a -> 'a t
          val bind: 'a t -> ('a -> 'b t) -> 'b t
      end

      val log: unit -> unit Monad.t
  end


We now define a functor that takes a LOGGER and defines a 'process' function
that operates under the monad.  But here's the twist: suppose that the function
that actually does the processing is defined elsewhere, in a module 'Foo'.
Moreover, instead of passing it the functions of the logger as independent
parameters, we deem it more convenient to pass the logger as a first-class
module:

  module Make (Logger: LOGGER) =
  struct
      let process x = Foo.actually_process (module Logger: LOGGER) x
  end


To avoid type-escaping-its-scope errors, we need to define a locally abstract
type in the implementation of 'actually_process'.  Something like this:

  let actually_process (type u) (module Logger: LOGGER with type 'a Monad.t = 'a u) x =
      let open Logger in
      let (>>=) t f = Monad.bind t f in
      Logger.log () >>= fun () ->
      Monad.return x


Which does not actually compile.  Is it at all possible to use a locally
abstract type when that type has type parameters?  And is there a solution
to this problem that does not require a) moving the implementation of
'actually_process' to the inside of a functor, or b) pass each function
of the first-class module as a separate parameter to 'actually_process'?

Thanks in advance for your time!
Best regards,
Dario Teixeira

Re: [Caml-list] Locally abstract type with type parameters

[John F. Carr]

I hit the same limitation last year:

https://sympa.inria.fr/sympa/arc/caml-list/2013-04/msg00159.html

The inability to constrain parameterized types in packed module
types is a documented restriction.  You will have to ask the type
theory experts whether it is a necessary restriction.

A followup message offered a workaround for some cases.

https://sympa.inria.fr/sympa/arc/caml-list/2013-04/msg00160.html

 > To avoid type-escaping-its-scope errors, we need to define a locally abstract
 > type in the implementation of 'actually_process'.  Something like this:
 > 
 >   let actually_process (type u) (module Logger: LOGGER with type 'a Monad.t = 'a u) x =
 >       let open Logger in
 >       let (>>=) t f = Monad.bind t f in
 >       Logger.log () >>= fun () ->
 >       Monad.return x
 > 
 > 
 > Which does not actually compile.  Is it at all possible to use a locally
 > abstract type when that type has type parameters?  And is there a solution
 > to this problem that does not require a) moving the implementation of
 > 'actually_process' to the inside of a functor, or b) pass each function
 > of the first-class module as a separate parameter to 'actually_process'?
 > 
 > Thanks in advance for your time!
 > Best regards,
 > Dario Teixeira

Re: [Caml-list] Locally abstract type with type parameters

[Benjamin Greenman]

[-- Attachment #1: Type: text/plain, Size: 395 bytes --]

I agree with the solution in the second link: if you want a certain
condition to hold on the parameter, it needs to be made explicit. As for
whether this restriction is necessary, I believe it is because I don't see
any way of deciding the question 'a Monad.t = 'a u without examining the
abstract type hidden in a particular Logger.

What if you made LOGGER a functor parameterized on a Monad?

[-- Attachment #2: Type: text/html, Size: 613 bytes --]

Re: [Caml-list] Locally abstract type with type parameters

[Leo White]

Hi Dario,

> To avoid type-escaping-its-scope errors, we need to define a locally abstract
> type in the implementation of 'actually_process'.  Something like this:
>
>   let actually_process (type u) (module Logger: LOGGER with type 'a Monad.t = 'a u) x =
>       let open Logger in
>       let (>>=) t f = Monad.bind t f in
>       Logger.log () >>= fun () ->
>       Monad.return x
>

This function relies on higher-kinded polymorphism (i.e. it is
polymorphic in type `u` which has type parameters). Since OCaml's core
language does not provide direct support for higher-kinded polymorphism
the usual solution is to make `actually_process` into a functor. A
possible alternative solution, which may suit your use case, is outlined
in the paper "Lightweight higher-kinded polymorphism" [1] using the
"higher" library available on OPAM.

Regards,

Leo

[1] Lightweight higher-kinded polymorphism
    Jeremy Yallop and Leo White   FLOPS 2014
    http://www.lpw25.net/flops2014.pdf

Re: [Caml-list] Locally abstract type with type parameters

[Dario Teixeira]

Hi,

> This function relies on higher-kinded polymorphism (i.e. it is

> polymorphic in type `u` which has type parameters). Since OCaml's core
> language does not provide direct support for higher-kinded polymorphism
> the usual solution is to make `actually_process` into a functor. A
> possible alternative solution, which may suit your use case, is outlined
> in the paper "Lightweight higher-kinded polymorphism" [1] using the
> "higher" library available on OPAM.

Ah... It makes sense now -- thanks for the explanation!
I ended up making actually_process also part of a functor.
Still, it's nice to know about this limitation and of
the alternative offered by your Higher library.

Best regards,
Dario Teixeira