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

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

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