Re: [Caml-list] First-class Functor Forgetting for Free

[Andreas Rossberg <rossberg@mpi-sws.org>]

On Aug 11, 2013, at 03:55 , David Sheets <sheets@alum.mit.edu> wrote:

> What issue prevents functions over first-class modules from forgetting
> the first-class modules' type constraints?
> 
> That is, given:
> 
> ###############
> 
> module type D = sig
>  type t
> 
>  val x : t
>  val f : t -> int
> end
> 
> module type C = sig
>  val q : int
> end
> 
> module F(X : D) : C = struct
>  let q = X.(f x)
> end
> 
> let f x =
>  let module X = (val x : D) in
>  let module Q = struct
>    let q = X.(f x)
>  end in
>  (module Q : C)
> 
> let x =
>  let module X = struct
>    type t = int
> 
>    let x = 2
>    let f x = x * 3
>  end in
>  (module X : D with type t = int)
> 
> ;;
> let module X = (val x : D with type t = int) in
> let module M = F(X) in
> (* let x = (module (val x : D with type t = int) : D) in*)
> let module M' = (val f x : C) in
> 
> Printf.printf "M.q  is %d\n%!" M.q;
> Printf.printf "M'.q is %d\n%!" M'.q;
> ()
> 
> ###############
> 
> Why must I uncomment (* let x = (module (val x : D with type t = int)
> : D) in*) to compile?
> 
> I understand why structural subtyping requires a module cast but I
> don't see why type relaxation would.
> I looked at the generated assembly and this line seems to disappear.
> 
> Why is it needed?

There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply?

  let g x = let module X = (val x : D) in X.(f x)

That said, as usual in OCaml, you can force subtyping explicitly. That is, you are able to just say

  let module M' = (val f (x :> (module D)) : C) in …

in your example. (Explicit subtyping on package types is still very limited, though, i.e. only allows forgetting type equations on the same named signature.)

/Andreas