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

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

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