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

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

>
> 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. Even if they were mappings from
paths, paths are still simple labels.

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.

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

> 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 don't think this is correct. Not listing a "with-constraint" on a
package type *does* mean that the "with-constraint" is
absent. 

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

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

As I said above, I am only proposing the row types for the package
types, not for actual module types. `(S with ..) < S` could not arise
(which is good because I agree that it is nonsense).

> Hope those are enough open questions for now. :)

Thank you for the list :).

Obviously I have only outlined why I don't think those questions would
be difficult to address. To be sure that it would work someone would
need to have a more formal look at giving it a static semantics. But I
still don't see any reason why we could not use row-polymorphism for the
with-constraints of package types.

Regards,

Leo