Re: [Caml-list] first class module types with "with type"

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/01/29 08:39, Milan Stanojević wrote:
> 
> My search foo is failing me, I'm pretty sure this was discussed before
> but I can't find it.
> 
> Why is the following disallowed:
> module type A = sig type 'a t end
> type foo = { a : (module A with type 'a t = 'a list)}
> 
> File "z.ml", line 2, characters 29-30:
> Error: Syntax error

This is because ocaml does not have higher-order polymorphism in its
core language.
Namely, the type (module S with type t = texpr) can be seen as
the type (texpr s) where
   type 'a s = (module S with type t = 'a)
However, if t itself has a type parameter, we cannot turn it into a
type variable (which would have to be higher-order).

Technically, it would be possible to allow such equations, if we do not
go through the above intermediate type s. That is, we would have to
require that the type definition contains no free variables, in contrast
with non-parameterized ones for which allowing free variables is
essential.

> But this is ok
> module type A = sig type 'a t end
> module type S = A with type 'a t = 'a list
> type a = (module S)

OCaml has higher-order polymorphism in the module language.
This is what you are using in this case.
Not that from the point of view of theoretical expressivity, there is no
big difference between the two: since 4.02, equality on package types
is structural, so that it will work even if you define S twice in different
places.

Jacques Garrigue