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

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

> Your row variables will inevitably be higher-order, AFAICS.
>

I don't think they will be. To be higher order wouldn't they need to
have parameters? I don't see how they could end up with parameters.

Looked at another way, package types are essentially a pair of a module
type and a set of with-constraints. The row variables would simply stand
for these same sets of with-constraints. Just as the package type is not
higher order neither would the row variables be.

>
> I don't think that there would be any higher-order unification involved in this example, because you'd only unify the
> RHSs, which are ground, and all unification variables would still be ground as well. I'm less convinced that the same
> can be assumed about unification with row variables for constraints (although it could be).
>

I don't see how row variables could possibly affect this.

>
> I disagree completely. Packages wrap modules, so package types _are_ module types. The point of package types is to
> embed module types into the core type system, not to create a parallel module type system. I think it would be a real
> bad idea to invent a separate typing mechanism for this purpose, since that is bound to create complexity, friction, and
> confusion.
>

I also disagree completely. Packages wrap modules, so package types
_wrap_ module types. The core type system provides mechanisms that are
not available in the module type system. We should not rule out using
these mechanisms with package types to make then easier to use. 

Embeding module types into the core type system should mean allowing the
mechanisms provided by the core type system to operate on module types,
not just allowing the core type system to treat module types as
black-boxes that can be passed around and given back to the module
system.

Regards,

Leo