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

[David Sheets <sheets@alum.mit.edu>]

On Sun, Aug 11, 2013 at 8:53 AM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> On Aug 11, 2013, at 03:55 , David Sheets <sheets@alum.mit.edu> wrote:
>> 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)

Something like val g : [< (module D)] or simply val g : (module D)
where the type constraint relation is implicit seems reasonable. I
don't know if you consider polymorphic variant types as part of the
core language (or perhaps they aren't implicit because they propagate
inequalities?).

I guess the module system isn't part of the core as it does implicit
structural subtyping. This makes the embedding of the module type
system into the value type system surprising.

> 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 …

Good to know! I looked briefly and did not see this mentioned in the manual.

> 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.)

This seems somewhat strange. Why are aliases not followed?

David