Could functors be more like functions?

Learning
#1

I’d like to be able to write things like this:

module F(X) = struct
  module Y = X
end

module Param = struct let x = 123 end
module M = F(Param)

let () = print_int M.Y.x

i.e. I want the argument passed to F to keep its original signature. I want M.Y to be known as an alias for Param, so I can jump to the documentation of Param when looking at occurrences of Y.

Is this something we might want to have in OCaml one day or is it fundamentally incompatible with existing features?

Any recommendations for achieving similar effects? (a solution is to use a macro/template instead of a functor).

1 Like
#2

Do you mean that you want the parameter X of your functor could have any signature? Id est having something like a module type variable 'S to mean any signature, in the same way we have type variable 'a to mean any type?

If so I guess this is not possible, it will be unsound and lead to paradox analogous to Russell’s paradox.

#3

Note that we can already define a cppo macro that somewhat does the job:

#define F(X) struct \
  module Y = X \
end

module Param = struct let x = 123 end
module M = F(Param)

This expands into:

# 5 "functor.ml"
module Param = struct let x = 123 end
module M = 
# 6 "functor.ml"
            struct 
  module Y = Param 
end

I’d rather avoid this for a few reasons:

  • The macro itself is not typechecked until the point where it’s used. It can be mitigated by writing a test suite but it’s not great.
  • It can’t be distributed as a library or without its source code.
  • It duplicates code, which can be wasteful.
  • The cppo tool itself imposes backslashes at end of lines and tends to break IDEs. It’s just awful in already complex applications where functors make sense.
#4

Here’s the equivalent of my original functor example, using objects:

let f x =
  object
    method y = x
  end

let param = object method x = 123 end
let m = f param

let () = print_int m # y # x

This illustrates that the type of param is passed along, without f having to know about it.

If a more specific structure is expected from the argument of f, everything works just fine too:

let f x =
  object
    method y = x
    method s = x # name
  end

let param = object
  method name = "abc"
  method x = 123
end

let m = f param

let () =
  Printf.printf "%i\n%s\n%!"
    m # y # x
    m # s
;;
val f : (< name : 'b; .. > as 'a) -> < s : 'b; y : 'a > = <fun>
val param : < name : string; x : int > = <obj>
val m : < s : string; y : < name : string; x : int > > = <obj>
123
abc

The signature of f really has no unnecessary constraints. It’s great. Except that object interfaces don’t contain type definitions like module interfaces do.

#5

That works with objects because an object cannot contains a type definition, which is not the case with a module. For instance in 1ML:

there is a distinction between small and large types: small types cannot contain type definitions (as objects in OCaml) and large types contains type definition (as most of modules signatures). For soundness reason, we cannot universally quantify over large types but only over small types (as in OCaml). And in this language functors are ordinary functions, since the module and the core language have been fused, but we cannot define the generic function you’re searching for.

3 Likes
#6

I’m afraid this is the only solution to your problem due to its generality. This kind of macro language are untyped functional language, but as 1ML shows it seems impossible if you want static type checking.

1 Like
#7

@kantian do you think it’s possible to get some static type checking via a ppx style extension?

#8

This is totally possible:

module type Type = sig module type T end

module F(T : Type)(X : T.T) = struct
  module Y = X
end

it’s not unsound, although it does lead to Girard’s paradox (people seem to confuse it with Russel’s paradox but they are not the same). There’s an implementation of Girard’s paradox in OCaml here.

However, this isn’t sufficient to get what @mjambon is after. It also requires allowing module aliases of functor parameters. This is not currently supported. It will probably be supported at some point but requires some additions to the module system to work safely. I’m aiming to get it in for 4.09.

5 Likes
#9

Indeed I did a confusion between “paradox = unsoundness” and “paradox = non termination”.

I need to reread the 1ML article to better understand why he do a distinction between small an big type (it reminds me the distinction between set and proper classes in ZF, or the distinction between small and big categories in category theory).

By the way, even if there is no module aliases of functor parameters @mjambon can still use your encoding:

module type Type = sig module type T end

module F (T : Type) (X : T.T) = struct
  module Y = X
end

module Param = struct let x = 123 end

module M = F (struct module type T = module type of Param end) (Param);;
module M : sig module Y : sig val x : int end end

M.Y.x;;
- : int = 123

in the general case he may need to use the module type of struct include Param end trick to have the strengthened signature of Param, or did you merge the patch on module type of you wanted to do?

2 Likes
#10

Honest question, how can a mere mortal like myself begin to understand your implementation of Girard’s paradox? I remember encountering it a while ago and thinking to myself, “this seems significant, but I don’t even know where to start”. I suppose one could always start from the top…?

#12

The code itself is very hard to read, since all polymorphism has to be explicit and limitations of the module system force it to be in continuation-passing style. I don’t personally have a deep understanding of Girard’s paradox, so I used this paper as a template – it has a good description of the paradox and its encoding in a lambda calculus with dependent function types.

The overall approach is basically just classic dependently typed programming, so just try learning some Coq or Agda and you should get the basic idea of how that code works.

I think “significant” is probably a bit strong. The fact that you can implement Girard’s paradox is basically an obvious side-effect of having dependent functions (in the form of functors) and Type : Type (in the form of abstract module types). It demonstrates that OCaml’s module system is theoretically in some sense a dependently typed language – although the convoluted nature of the code also shows that it is not really a dependently typed language in practice. This means, for example, that you could not elaborate OCaml to System Fomega (unlike the SML module system which does have an elaboration to System Fomega described in this paper).

3 Likes
#13

Wow, now I understand why people say that module language is dependently typed, thanks for that example.

#14

If you want more specific structure on your module parameter X (as in your second example with objects) then you have to adapt @lpw25 solution: you need a third parameter constrained with your specific needs.

Example with an adaptation of your second object cases:

module type Type = sig module type T end

(* here the specific constraints on your module *)
module type S = sig type t val name : t end

(* the functor F *)
module F (A : Type) (X : A.T) (M : S) = struct
  module Y = X
  type t = M.t
  let name = M.name
end

(* a module similar to your object *)
module P1 = struct
  type t = string
  let name = "abc"
  let x = 123
end

(* the same module but its inner type is made abstract *)
module P2 : (sig include S val x : int end) = P1

(* use of the functor F *)
module M = F (struct module type T = module type of P1 end) (P1) (P1);;
module M :
  sig
    module Y : sig type t = string val name : t val x : int end
    type t = string
    val name : t
  end

let () =
  Printf.printf "%i\n%s\n"
    M.Y.x
    M.name
;;
123
abc

(* use with P2 and its abstract type *)
module N =
  F  (struct module type T = module type of P2 with type t = P2.t end)
     (P2) (P2)
;;
module N :
  sig
    module Y : sig type t = P2.t val name : t val x : int end
    type t = Y.t
    val name : t
  end

N.name;;
- : N.t = <abstr>

N.name = P2.name;;
- : bool = true
1 Like