Module subtyping in higher-rank-polymorphic functions

[pxeger]

(Functor and Applicative are defined here)

The following code fails to compile, because the compiler doesn't consider Applicative a subtype of Functor, and possibly also because the compiler doesn't know that {M} -> t is contravariant in M.

type accepts_functor = {F: Functor} -> int F.t -> int F.t
let accepts_functor {F: Functor} x = F.fmap ((+) 1) x

type accepts_applicative = {F: Applicative} -> int F.t -> int F.t
let accepts_applicative {F: Applicative} x = F.fmap ((+) 1) x

let use (f: accepts_applicative) = f [1; 2; 3]

let () =
  ignore (use accepts_applicative);
  ignore (use accepts_functor)   (* errors here *)

Error: This expression has type
         {F : Functor} -> int F.t -> int F.t
       but an expression was expected of type
         accepts_applicative =
           {F : Applicative} -> int F.t -> int F.t
       Type (module Functor) is not compatible with type
         (module Applicative)

This came up while trying to implement composition of lenses in lens.

The corresponding code in Haskell works fine.

Unlike in Haskell, Functor may not necessarily be a subtype of Applicative in OCaml, I think because of something to do with the scoping flexibility OCaml gives you in modules, compared to Haskell's typeclasses? (TODO: find out exactly why, ideally with a counterexample)

@yallop suggested that it might at least be allowed when Functor's signature is a strict prefix of Applicative's (which it is, in this case).

[yallop]

possibly also because the compiler doesn't know that {M} -> t is contravariant in M.

I think the variance of {...} -> is handled correctly, since this is accepted:

module type S = sig type t end
module type T = sig include S type u end
let f (t : {X:S} -> int) = (t :> {X:T} -> int)

but there's a very restrictive notion of subtyping allowed for implicit arguments

[clementblaudeau]

Do you reuse the subtyping check of first-class modules ? Type (module Functor) is not compatible with type (module Applicative) This looks like the type of the first-class module (module Functor) is checked against (module Applicative), but I might be wrong.

The subtyping check for first-class modules is a subset of the normal subtyping check between signatures, with a restriction to code-free subtyping (same value fields in the same order).

[samsa1]

I just checked the code and I confirm what clement stated. Subtyping is done by using the same comparison than the one used with first-class modules : ie same runtime representation. Modifying the way it currently works could be done by :

• either an eta expansion of the function (but it would have an impact on performances)
• or allowing the runtime to handle modules containing more fields than expected (but would allows only a few more cases)