Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

OCaml: higher kinded polymorphism (abstracting over modules?)

Let's say I have a list of options:

let opts = [Some 1; None; Some 4]

I'd like to convert these into an option of list, such that:

  • If the list contains None, the result is None
  • Otherwise, the various ints are collected.

It's relatively straightforward to write this for this specific case (using Core and the Monad module):

let sequence foo =
let open Option in
let open Monad_infix in
  List.fold ~init:(return []) ~f:(fun acc x ->  
    acc >>= fun acc' -> 
    x >>= fun x' -> 
    return (x' :: acc')
    ) foo;;

However, as the question title suggests, I'd really like to abstract over the type constructor rather than specialising to Option. Core seems to use a functor to give the effect of a higher kinded type, but I'm not clear how I can write the function to be abstracted over the module. In Scala, I'd use an implicit context bound to require the availability of some Monad[M[_]]. I'm expecting that there's no way of implicitly passing in the module, but how would I do it explicitly? In other words, can I write something approximating this:

let sequence (module M : Monad.S) foo =
let open M in
let open M.Monad_infix in
  List.fold ~init:(return []) ~f:(fun acc x ->  
    acc >>= fun acc' -> 
    x >>= fun x' -> 
    return (x' :: acc')
    ) foo;;

Is this something that can be done with first class modules?

Edit: Okay, so it didn't actually occur to me to try using that specific code, and it appears it's closer to working than I'd anticipated! Seems the syntax is in fact valid, but I get this result:

Error: This expression has type 'a M.t but an expression was expected of type 'a M.t
The type constructor M.t would escape its scope    

The first part of the error seems confusing, since they match, so I'm guessing the problem is with the second - Is the problem here that the return type doesn't seem to be determined? I suppose it's dependent on the module which is passed in - is this a problem? Is there a way to fix this implementation?

like image 795
Impredicative Avatar asked Feb 26 '13 14:02

Impredicative


People also ask

Does OCaml have higher-Kinded types?

OCaml does not support higher-kinded polymorphism directly: OCaml type variables range over types rather than type constructors, and type constructors may not appear in type expressions without being applied to the right number of arguments.

Why are there high Kinded types?

Higher-kinded types are useful when we want to create a container that can hold any type of items; we don't need a different type for each specific content type.


1 Answers

First, here is a self-contained version of your code (using the legacy List.fold_left of the standard library) for people that don't have Core under hand and still want to try to compile your example.

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

let sequence (module M : MonadSig) foo =
  let open M in
  let (>>=) = bind in
  List.fold_left (fun acc x ->  
    acc >>= fun acc' -> 
    x >>= fun x' -> 
    return (x' :: acc')
  ) (return []) foo;;

The error message that you get means (the confusing first line can be ignored) that the M.t definition is local to the M module, and must not escape its scope, which it would do with what you're trying to write.

This is because you are using first-class modules, that allow to abstract on modules, but not to have dependent-looking types such as the return type depends on the argument's module value, or at least path (here M).

Consider this example:

module type Type = sig
  type t
end

let identity (module T : Type) (x : T.t) = x

This is wrong. The error messages points on (x : T.t) and says:

Error: This pattern matches values of type T.t
       but a pattern was expected which matches values of type T.t
       The type constructor T.t would escape its scope

What you can do is abstract on the desired type before you abstract on the first-class module T, so that there is no escape anymore.

let identity (type a) (module T : Type with type t = a) (x : a) = x

This relies on the ability to explicitly abstract over the type variable a. Unfortunately, this feature has not been extended to abstraction over higher-kinded variables. You currently cannot write:

let sequence (type 'a m) (module M : MonadSig with 'a t = 'a m) (foo : 'a m list) =
  ...

The solution is to use a functor: instead of working at value level, you work at the module level, which has a richer kind language.

module MonadOps (M : MonadSig) = struct
  open M
  let (>>=) = bind

  let sequence foo =
    List.fold_left (fun acc x ->  
      acc >>= fun acc' -> 
      x >>= fun x' -> 
      return (x' :: acc')
    ) (return []) foo;;
end

Instead of having each monadic operation (sequence, map, etc.) abstract over the monad, you do a module-wide abstraction.

like image 168
gasche Avatar answered Oct 21 '22 22:10

gasche