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

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

On 08/11/2013 04:58 PM, Leo White wrote:
>>>> 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 don't think type inference for polymorphic variants works the way you think it does. Inference for both variants and objects is based on row polymorphism, not subtyping. A type like [< A] is actually a polymorphic type with a hidden type variable, not a subtype bound, even though the surface syntax intentionally hides that fact (which isn't always helpful). Module signatures are totally different beasts, where matching _is_ a form of subtyping.
>
> I think David is suggesting that "with-constraints" on first-class
> modules could be handled with row polymorphism, and I don't know of any
> reason why they couldn't. It would certainly be a more flexible way to
> type them. So,
>
>    let g x = let module X = (val x : D) in X.(f x)
>
> would have a type:
>
>    (module D with ..) -> int

This certainly is a nice suggestive syntax, but it is assuming an 
underlying semantic similarity that does not exist. Semantically, the 
type sharing equations on signatures have very little in common with 
rows, and I have a hard time imagining what interpreting the above as a 
row would even mean, or how it would fit in with either core or module 
typing. (I could go into boring technical details here, but I'll leave 
it at that. :) )

/Andreas