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

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

On 08/12/2013 01:37 PM, Leo White wrote:
>>> 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 don't see what is hard to imagine. The row variable represents
> possible extra with-constraints. The type above can be unified with any
> package type with signature D.
>
> With-constraints are essentially sets of label and type pairs, row
> polymorphism provides a mechanism for typing sets of label and type
> pairs. I don't see where they differ "semantically".

With constraints generally map _type paths_ to _type constructors_. 
Moreover, the domain of type paths is bounded by what actually occurs in 
the signature. That already sets them apart from rows on a basic 
syntactic and semantic level. (Mind you, OCaml doesn't currently allow 
revealing type constructors in package types, but that is a limitation 
that seems much more important to lift than what we are discussing here.)

More importantly, unlike for rows, not listing a type in a constraint 
doesn't mean that it's absent. It means that it is kept abstract. That's 
quite different, and it would require some notion of implicit 
existential type introduction based on the instantiation, for which I 
have no idea how it should work. Some form of skolemisation perhaps? How 
does that integrate with the rest of core typing and inference? Type 
inference with existentials is known to be very tricky.

I also wouldn't know how exactly the row idea ties in with signature 
matching. What does (S with ..) < S mean? The only interpretation I can 
see is by expanding ".." into a list of equations for all types abstract 
in S -- but that would notably _not_ be a row-polymorphic interpretation.

Hope those are enough open questions for now. :)

/Andreas