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

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

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

> Even if they were mappings from
> paths, paths are still simple labels.

Only if you squint real hard, IMHO.

> The with-constraints in package types map to types not type
> constructors, as evidenced by the existence of types like:
>
>    (module D with type t = 'a) -> 'a
>
>> Moreover, the domain of type paths is bounded by
>> what actually occurs in the signature.
>
> I don't think that row polymorphism has particular difficulty with such
> bounding. Consider the type:
>
>   [< `Foo of int | `Bar of float > `Foo]
>
> this type contains a row variable (well something very similar to a row
> variable) that is quite constrained in how it can be instanciated. This
> essentially involves to a simple kind system that is hidden from the
> programmer.
>
> I think a similar approach would be fairly easy for with-constraints,
> each module type would basically entail the existance of a kind of row
> variable.

I've heard things like "fairly easy" far too often in contexts like this. ;)

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


> Certainly, unpacking a first-class module introduces an abstract
> type if there is no "with-constraint" on the module type that it is
> being unpacked with. But the module type that it is unpacked under, and
> the package type that it has are *not* the same thing.
>
> To be clear, I am only proposing the existence of row types for
> first-class modules not for module types in general. So the following
> code:
>
>    let module M = (val x : S) in ..
>
> would give module M the module type `S`, but unify the type of `x` with
> `(module S with ..)`. Similarly,
>
>    let module M = (val x : S with type t = int) in ..
>
> would give module M the module type `S with type t = int`, and unify the type of `x` with
> `(module S with type t = int and ..)`. But the following would be invalid:
>
>    let module M = (val x : S with type t = int and ..) in ..

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

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?

/Andreas