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

[Leo White <lpw25@cam.ac.uk>]

Andreas Rossberg <rossberg@mpi-sws.org> writes:

> On 08/12/2013 03:06 PM, Leo White wrote:
>>>
>>> With constraints generally map _type paths_ to _type constructors_.
>>
>> OCaml doesn't allow deep with-constraints (e.g. with type M.t = foo) so
>> they are actually mappings from names.
>
> That's not correct. It has been supported since 4.0 (IIRC).
>

Somehow I managed to miss that change. It should probably be added to
the manual.

>>> (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.)
>>
>> Allowing type constructors to be revealed by package types would
>> complicate things, but I don't think it would be hard to
>> accomodate. There is a fairly obvious analogy between:
>>
>>    (module S with type 'a t = 'a list and ..)
>>
>> and
>>
>>    < t: 'a. 'a list; .. >
>
> No, that's not the same at all. One is a quantified type, the other a parameterised type (constructor). When you allow
> higher-order type variables, you get into the business of higher-order unification, which is complicated, and
> undecidable in the general case. You'd need to investigate very carefully what restrictions to impose to avoid being
> pulled down that rabbit hole.

I think The required type-checking is quite similar for these two cases,
although the comparison is possibly not that useful. Note that I have
not suggested adding any higher-order type variables.

This is besides the point anyway, as this problem is entirely orthogonal
to the addition of row polymorphism. If you want to allow revealing type
constructors in package types then you need to solve this issue. For
example, type-checking this:

let f 
    (x: (module S with type 'a t = 'a foo * 'b)) 
    (y: (module S with type 'a t = 'a bar * int)) = [x; y];;

requires you to know how to unify:

  module S with type 'a t = 'a foo * 'b

with

  module S with type 'a t = 'a bar * int

>
> OK, I see. But all that would make package typing even more ad-hoc, and divorce its semantics from that of proper
> signatures and signature matching even more. 

I disagree. The point of a package type is to ensure that the module
type that the package was packed with matches the module type that the
package is unpacked with. There is no reason to assume that this is best
done by a carbon copy of the module types. 

Row polymorphism would make first-class modules significantly less
awkward to use (in the same way that it makes objects significantly less
awkward to use). If anything it would be less ad-hoc than the current
system, which uses forward type propagation to try to infer the correct
with-constraints for a package expression.

> That's the opposite of the direction I'd like the package feature to go. It
> would be fairly hostile to future generalisations of packages.

Again, I disagree. I see no reason that it would be hostile to future
generalisations. Do you have anything particular in mind? 

> So, yes, perhaps you could make something work along the lines you sketch, assuming enough restrictions are in
> place. But the price seems way too high for the minor convenience it provides. Wouldn't you agree?

I don't think that any restrictions are needed, so obviously I don't
agree that there is a high price.

Regards,

Leo