Having types as possible module arguments

[samsa1]

A proposed design for having types as module arguments.

Rendered version

In summary :

module List (type a) = struct
    type t = a list
    let size : t -> int = List.length
    let fold : ('acc -> a -> 'acc) -> 'acc -> t -> 'acc = List.fold_left

module M = List(type int)

let f (x : List(type int).t) = ...

[gasche]

The RFC is lacking the part where you argue why this feature is desirable/useful. Do you have compelling examples? (I know from private communication that there are some examples coming from modular implicits, and I think that it would be interesting to explain them, but maybe there are also compelling examples without them today?)

One way to look for examples would be to look for uses of sig type t end in OCaml codebases in the wild. Here is for example a Github search URL, I have not looked at the results much.

[gasche]

typo: to simplify cases

[gasche]

restrictions

[gasche]

I find the wording of this paragraph obscure. I'm not fully sure what you mean by "type path", and "inside a type path" is also not clear. I believe that you are talking about type-functor applications that show up inside type expressions: M(type foo).t; but can you give more details on the restriction on foo, for example by listing the allowed constructions?

[gasche]

(cc @yallop who may be interested in this feature)

[clementblaudeau]

You can look at example also via this sherlocode search
Regarding applicativity, I should stress that modules taking types as arguments are indeed applicative functors : no generative call or unpacking of first class module should be allowed in their body.
[EDIT] *unpacking of first class module is not allowed only when it creates fresh types

[diremy]

The counter example

module F (type a) = struct let r : a option ref = ref None end

is indeed a counter example if the compilation would not be compiled as a function.
Still, this functor should not be defined as applicative, since it allocates a reference.
Hence, two successive applications to the same type still returns structures that are not equal. Hence, it should rather be make generative and defined as

module F (type a) () = struct let r : a option ref = ref None end

[diremy]

I asume that the encoding is :

1:    module F (type a) = BODY [a]
2:    F (type P) 

stand for

1:      module F (A : Type)  = BODY [A.t]
2:     F (struct type t = P end)

where Type is either predefined or inlined as sig type t end.
Shouldn't this be added to the RFC as It shows that the proposal does not add expressiveness, just conciseness. And removes any possible ambiguity for its meaning.

[yallop]

If we could avoid giving the type arguments at runtime for modules like with functions we would have soundness issues.

This isn't clear to me. Have you considered the alternative of using a value restriction?

In current OCaml, type arguments to functions, like this

let f (type a) = ...

don't have run-time representations, and type arguments to constructors, like this

let f (T (type a) (x : a)) = ...

don't have run-time representations, so it's a bit non-uniform for type arguments to modules to have run-time representations. Type arguments to functions don't delay evaluation

let f (type a) = begin print_endline "ok" end (* prints "ok" *)

so it's rather surprising if type arguments to modules do delay evaluation:

module M (type a) = struct print_endline "ok" end (* prints nothing *)

For type arguments to functions, the usual value restriction applies, so in the following, a is left weak (ungeneralized):

let f (type a) =
   let r : a option ref = ref None in
   ...

Could a similar approach work for type arguments to modules?

Continuing the analogy, type arguments to functions don't need to be supplied explicitly (though perhaps it'd be useful to have the option to do so). Could a similar approach work for type arguments to modules?

[gasche]

Side-note: I find it surprising that (type a) does not force generalizability, and I would prefer the a option ref example to be rejected with an error.

[diremy]

I was actually wondering the same as Jeremy. I understand that the proposal is just syntactic sugar for the encoding I proposed, hence the actual semantics. However, it might be more interesting to not make it syntactic sugar and restric the body to be a value form. If we chose this sematics and restriction, the actual behavior when the body is not a value form can be recovered by passing an extra empty structure strut end to make it applicative or () to make it generative... or using the encoding :-)
The question is then for which kinds of examples would the construct be used in practice? If in most cases, the body is a value, it might be worth considering this as a new construct with a new semantics.
The State example cannot be treated as a value since it generates a new effect whose type depend on the type parameter.
I think this should deserve should more thoughts.

[samsa1]

This isn't clear to me. Have you considered the alternative of using a value restriction?

In the case where we we want to keep the descripted semantic with explicit application by the user, we can remove the application if the functor is pure. Because all applications will give the same result thus it can be pre-computed.

I think the proposal from @diremy of not handling this as syntactic sugar and restricting the body to be a value seems to be a good idea. The biggest argument being that we can still obtain the actual behavior by adding the argument that is currently added at runtime in the proposal.

Continuing the analogy, type arguments to functions don't need to be supplied explicitly (though perhaps it'd be useful to have the option to do so). Could a similar approach work for type arguments to modules?

I think we might have cases where being able to explicitly give the type argument is still beneficial. I agree that sometimes not writing that argument could increase concision (such as M.f instead of M(type t).f. However sometimes it is still better to be able to write explicitly the type argument (such as inside type annotations). Thus treating this as an optional argument might be the best approach.

[gasche]

I don't think that handling this as an optional argument works well. Consider the case where you abstract over several type arguments in sequence, there is no way at application time to indicate which of the arguments you have in mind on explicit application.

I'm of two minds regarding application expliciteness:

1. @yallop makes a good point that all existing instances of the (type a) abstraction have implicit application, so doing this is more consistent. But I expect that users will often want to specify the argument explicitly. In the case of GADT constructors we tried to give a syntax for explicit binding at use-site on GADT patterns : K (type a) ((foo, bar) : a * a baz) -> ..., which was somewhat awkward. We don't have a good, consistent solution to how to pass (type a) arguments explicitly yet preserve their unnamed and order-independent nature expected in ML.

2. I think this may be related to syntactic questions about modular explicits and implicits. Is there a cute syntax to turn an explicit module argument into an implicit module argument, can we reuse the same here? If you use (module A : S) for explicit arguments and {module A : S} for implicit arguments, we could have {type a} here. (But this is inconsistent with existing (type a) constructs.) If you use a keyword, we could say have both (explicit module A : S) and (implicit module A : S), with (module A : S) a suitable default, and then we could have both (explicit type a) and (implicit type a), and possibly decide that the default meaning of (type a) depends on the language construct.
   (I don't remember, is there a proposed syntax to explicitly apply implicit module arguments? Can we reuse the same for types?)

[samsa1]

(I don't remember, is there a proposed syntax to explicitly apply implicit module arguments? Can we reuse the same for types?)

The propose syntax was to write f {M} if we wanted to give explicitly the first implicit argument. However, this was the proposal given in the modular implicits paper and I haven't heard of a proposal to distinguish modular explicits from modular implicits (but I think this should be discussed).

[gasche]

I think that this is a question that is weighting on @diremy's mind.

Note: Coq/Rocq allows the application syntax f (a := foo) to explicit apply the implicit argument a of f (manual > Explicit applications). Maybe we should seriously consider something like this for OCaml. In particular we could enable this syntax for all (type a) abstractions that exist today, in a compatible and consistent way.