Dear all,

With the advent of first-class modules, I find myself more and more wanting to write functors with only one (value) component, just to benefit from type dependencies. Here is an example (randomly) extracted from Oleg Kiselyov and Jeremy Yallop:

type a and b
module type TC = sig type 'a t end
module type Subst = functor (A:TC) -> sig val x : a A.t -> b A.t end

If this pattern had to become widespread, it would be worth agreeing for a name on the single component, though it's a bit unnecessary to need a name at all.
It get very verbose, though, when trying to applying the functor. Supposing I have a module Subst:Subst :

let module S = Subst(sig type 'a t = 'a list) in
S.x …

Nothing terrible really, but it sort of gets in the way. I can see benefit in having a special syntax for this sort of definition. I think we could take advantage of first-class functors to get something quite modular, here is a mockup syntax:

We could have the type

(X:A) => t

stand for (something like)

module F = functor (X:A) -> sig val x : t end

(module F)

and the definition

let f {{X:A}} = e

stand for

let f = let module F (X:A) -> struct let x = e end

and finally we'd need an application

e {{M}}

would stand for (something like)

let module F = (val e) in let module F' = F(M) in F'.x

Clearly the application needs something like OCaml 4.0 and the type definition some kind of cleverness (I don't know, by the way, why the syntax for F cannot be inlined in the type).

In this example syntax the above example would look like

type a and b
module type TC = sig type 'a t end
val subst : (A:TC) => a A.t -> b B.t

subst {{sig type 'a t = 'a list end}} …

I believe this would be something cool to have, so I came with two questions:
1/ Is there some demand for this kind of things (if not, I'm not sure it's worth pursuing, though of course demand could appear after supply)
2/ I don't see how to define the type syntax in camlp4, because of the inlining thing, could it be done?
(an alternative may be to have (X:A) => t be a module type, but then (X:A) => (Y:B) => t is not a valid type, so we would need syntaxes for n-ary abstraction/applications)