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

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

[David Sheets]

What issue prevents functions over first-class modules from forgetting
the first-class modules' type constraints?

That is, given:

###############

module type D = sig
  type t

  val x : t
  val f : t -> int
end

module type C = sig
  val q : int
end

module F(X : D) : C = struct
  let q = X.(f x)
end

let f x =
  let module X = (val x : D) in
  let module Q = struct
    let q = X.(f x)
  end in
  (module Q : C)

let x =
  let module X = struct
    type t = int

    let x = 2
    let f x = x * 3
  end in
  (module X : D with type t = int)

;;
let module X = (val x : D with type t = int) in
let module M = F(X) in
(* let x = (module (val x : D with type t = int) : D) in*)
let module M' = (val f x : C) in

Printf.printf "M.q  is %d\n%!" M.q;
Printf.printf "M'.q is %d\n%!" M'.q;
()

###############

Why must I uncomment (* let x = (module (val x : D with type t = int)
: D) in*) to compile?

I understand why structural subtyping requires a module cast but I
don't see why type relaxation would.
I looked at the generated assembly and this line seems to disappear.

Why is it needed?

Thanks,

David

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

[Andreas Rossberg]

On Aug 11, 2013, at 03:55 , David Sheets <sheets@alum.mit.edu> wrote:

> What issue prevents functions over first-class modules from forgetting
> the first-class modules' type constraints?
> 
> That is, given:
> 
> ###############
> 
> module type D = sig
>  type t
> 
>  val x : t
>  val f : t -> int
> end
> 
> module type C = sig
>  val q : int
> end
> 
> module F(X : D) : C = struct
>  let q = X.(f x)
> end
> 
> let f x =
>  let module X = (val x : D) in
>  let module Q = struct
>    let q = X.(f x)
>  end in
>  (module Q : C)
> 
> let x =
>  let module X = struct
>    type t = int
> 
>    let x = 2
>    let f x = x * 3
>  end in
>  (module X : D with type t = int)
> 
> ;;
> let module X = (val x : D with type t = int) in
> let module M = F(X) in
> (* let x = (module (val x : D with type t = int) : D) in*)
> let module M' = (val f x : C) in
> 
> Printf.printf "M.q  is %d\n%!" M.q;
> Printf.printf "M'.q is %d\n%!" M'.q;
> ()
> 
> ###############
> 
> Why must I uncomment (* let x = (module (val x : D with type t = int)
> : D) in*) to compile?
> 
> I understand why structural subtyping requires a module cast but I
> don't see why type relaxation would.
> I looked at the generated assembly and this line seems to disappear.
> 
> Why is it needed?

There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply?

  let g x = let module X = (val x : D) in X.(f x)

That said, as usual in OCaml, you can force subtyping explicitly. That is, you are able to just say

  let module M' = (val f (x :> (module D)) : C) in …

in your example. (Explicit subtyping on package types is still very limited, though, i.e. only allows forgetting type equations on the same named signature.)

/Andreas

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

[David Sheets]

On Sun, Aug 11, 2013 at 8:53 AM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> On Aug 11, 2013, at 03:55 , David Sheets <sheets@alum.mit.edu> wrote:
>> I understand why structural subtyping requires a module cast but I
>> don't see why type relaxation would.
>> I looked at the generated assembly and this line seems to disappear.
>>
>> Why is it needed?
>
> There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply?
>
>   let g x = let module X = (val x : D) in X.(f x)

Something like val g : [< (module D)] or simply val g : (module D)
where the type constraint relation is implicit seems reasonable. I
don't know if you consider polymorphic variant types as part of the
core language (or perhaps they aren't implicit because they propagate
inequalities?).

I guess the module system isn't part of the core as it does implicit
structural subtyping. This makes the embedding of the module type
system into the value type system surprising.

> That said, as usual in OCaml, you can force subtyping explicitly. That is, you are able to just say
>
>   let module M' = (val f (x :> (module D)) : C) in …

Good to know! I looked briefly and did not see this mentioned in the manual.

> in your example. (Explicit subtyping on package types is still very limited, though, i.e. only allows forgetting type equations on the same named signature.)

This seems somewhat strange. Why are aliases not followed?

David

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

[Andreas Rossberg]

On Aug 11, 2013, at 15:29 , David Sheets <sheets@alum.mit.edu> wrote:
> On Sun, Aug 11, 2013 at 8:53 AM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
>> On Aug 11, 2013, at 03:55 , David Sheets <sheets@alum.mit.edu> wrote:
>>> I understand why structural subtyping requires a module cast but I
>>> don't see why type relaxation would.
>>> I looked at the generated assembly and this line seems to disappear.
>>> 
>>> Why is it needed?
>> 
>> There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply?
>> 
>>  let g x = let module X = (val x : D) in X.(f x)
> 
> Something like val g : [< (module D)] or simply val g : (module D)
> where the type constraint relation is implicit seems reasonable. I
> don't know if you consider polymorphic variant types as part of the
> core language (or perhaps they aren't implicit because they propagate
> inequalities?).

I don't think type inference for polymorphic variants works the way you think it does. Inference for both variants and objects is based on row polymorphism, not subtyping. A type like [< A] is actually a polymorphic type with a hidden type variable, not a subtype bound, even though the surface syntax intentionally hides that fact (which isn't always helpful). Module signatures are totally different beasts, where matching _is_ a form of subtyping.

> I guess the module system isn't part of the core as it does implicit
> structural subtyping. This makes the embedding of the module type
> system into the value type system surprising.

Essentially, the fundamental technical differences (and different trade-offs) between core and module typing are the reason why you need the stratification between core and modules and the explicit embedding at all. If type inference modulo signature matching worked, modules probably wouldn't need to be a separate language layer. But there are fundamental limitations preventing that, e.g. completeness and decidability concerns.


>> That said, as usual in OCaml, you can force subtyping explicitly. That is, you are able to just say
>> 
>>  let module M' = (val f (x :> (module D)) : C) in …
> 
> Good to know! I looked briefly and did not see this mentioned in the manual.
> 
>> in your example. (Explicit subtyping on package types is still very limited, though, i.e. only allows forgetting type equations on the same named signature.)
> 
> This seems somewhat strange. Why are aliases not followed?

Typing of first-class modules in OCaml essentially reinterprets signature bindings as nominal type definitions, in order to side-step a number of technical implications that would arise with a more structural interpretation. Arguably, that's a bit of a hack (I hope that I don't offend anybody :) ). Unfortunately, it is not easy to be substantially more flexible without modifications to the innards of the module type system.

/Andreas

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

[Leo White]

>>> There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply?
>>> 
>>>  let g x = let module X = (val x : D) in X.(f x)
>> 
>> Something like val g : [< (module D)] or simply val g : (module D)
>> where the type constraint relation is implicit seems reasonable. I
>> don't know if you consider polymorphic variant types as part of the
>> core language (or perhaps they aren't implicit because they propagate
>> inequalities?).
>
> I don't think type inference for polymorphic variants works the way you think it does. Inference for both variants and objects is based on row polymorphism, not subtyping. A type like [< A] is actually a polymorphic type with a hidden type variable, not a subtype bound, even though the surface syntax intentionally hides that fact (which isn't always helpful). Module signatures are totally different beasts, where matching _is_ a form of subtyping.

I think David is suggesting that "with-constraints" on first-class
modules could be handled with row polymorphism, and I don't know of any
reason why they couldn't. It would certainly be a more flexible way to
type them. So,

  let g x = let module X = (val x : D) in X.(f x)

would have a type:  

  (module D with ..) -> int

and something like:

  module type S = sig type t type s val x: t val y: s end

  let h (module X : S) = X.x 

could have type:

  (module S with type t = 'a and ..) -> 'a

(which I also think should be expressable as "(module X : S) -> X.t" )

Regards,

Leo

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

[Andreas Rossberg]

On 08/11/2013 04:58 PM, Leo White wrote:
>>>> There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply?
>>>>
>>>>   let g x = let module X = (val x : D) in X.(f x)
>>>
>>> Something like val g : [< (module D)] or simply val g : (module D)
>>> where the type constraint relation is implicit seems reasonable. I
>>> don't know if you consider polymorphic variant types as part of the
>>> core language (or perhaps they aren't implicit because they propagate
>>> inequalities?).
>>
>> I don't think type inference for polymorphic variants works the way you think it does. Inference for both variants and objects is based on row polymorphism, not subtyping. A type like [< A] is actually a polymorphic type with a hidden type variable, not a subtype bound, even though the surface syntax intentionally hides that fact (which isn't always helpful). Module signatures are totally different beasts, where matching _is_ a form of subtyping.
>
> I think David is suggesting that "with-constraints" on first-class
> modules could be handled with row polymorphism, and I don't know of any
> reason why they couldn't. It would certainly be a more flexible way to
> type them. 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 could go into boring technical details here, but I'll leave 
it at that. :) )

/Andreas

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

[Leo White]

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

> (I could go into boring technical details here, but I'll leave it at
> that. :) )

I would prefer it if you did (off-list if you prefer).

Regards,

Leo

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

[Andreas Rossberg]

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

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

[Leo White]

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

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

[Andreas Rossberg]

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

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

[Leo White]

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

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

[Andreas Rossberg]

On 08/12/2013 05:17 PM, Leo White wrote:
> Andreas Rossberg <rossberg@mpi-sws.org> writes:
>> On 08/12/2013 03:06 PM, Leo White wrote:
>>>> (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.

I'm not sure what you mean, impredicativity and higher-orderness are 
different dimensions in the type system space, with different properties.

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


> 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

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

That said, I wasn't aware that OCaml actually allows unification 
variables in package constraints. I am not sure that's a wise design 
choice. It's a way of painting yourself into a corner with the type 
system, because it could make the generalisation to a more complete 
signature language for package types hard or impossible. Moreover, I'm 
not aware of any work investigating the formal implications it has.

All you _should_ need to check when unifying package types is that both 
denote equivalent signatures (i.e., mutual subtypes). I strongly believe 
that you do not want unification to be required for matching type 
components. (With local modules, it may be needed for matching value 
components, but that is fine.)


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

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.


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

Well, obviously, anything you can express with module signatures should 
be possible in package types. Ideally, the syntax would just be (module 
<module-type>), reusing the expressiveness you already have, and with a 
consistent semantics.


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

You assume the current syntax, which already is highly restricted. Also, 
the price involves the added complexity, too. Seems quite significant to 
me. ;)

/Andreas

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

[Leo White]

> 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

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

[Andreas Rossberg]

On 08/12/2013 06:46 PM, Leo White wrote:
>> 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.

Their instantiation would _contain_ type constructors, which makes them 
higher-order. Whether that would be a problem or not I'm not sure 
(probably not as long as these row variables cannot be used in any other 
context). It definitely is an extension over the kind of polymorphism 
OCaml currently supports.


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

I don't follow that line of reasoning. The primary reason why we have a 
two-layered language is that most of the core typing mechanisms simply 
_don't work_ for modules. Packages are a clean way of escaping the 
stratification without mixing up the layers and running into a wealth of 
potential problems.

It's unfortunate enough that programmers need to understand 2 separate 
sublanguages and type systems. Extending that to 2 + 1/2 and blurring 
the boundary with rather subtle and limited mechanisms would seem to 
have a negative net effect on language usability. I'd argue that less is 
more here (as is often the case in language design).

Best,
/Andreas