CODEWITHSUNDEEP
ocaml
jenga
jenga

Reputation: 33

Can I define an OCaml function only for certain functor parameters?

I would like to do something like this:

module Make (M: MInt) (N: MInt) : T = struct
    (* always defined *)
    let foo = 42

    (* only defined when M == N or M.x == N.x, something like that *)
    let bar a b = a * b
end

Is this possible?

Obviously I can check at runtime, but I'm curious how to do it at compile-time. Thanks!

Upvotes: 2

Views: 91

Answers (3)

Thomas Leonard
Thomas Leonard

Reputation: 7196

You could have a second functor that extends the first but requires the modules to be equal:

module Make (M: MInt) (N: MInt) : T = struct
    let foo = 42
end

module Make2 (M: MInt) : T2 = struct
    include Make(M)(M)

    let bar a b = a * b
end

Upvotes: 1

ivg
ivg

Reputation: 35210

To encode such kind of things one need a language with dependent typing. Dependent typing is a powerful feature of a type system, but, unfortunately it complicates a language and makes type inference undecidable. Usually, this is much more, than average programmer would be ready to pay. If you really want a language that will allow you to write such specifications, then you need to try Coq.

OCaml still have a support to somewhat restricted dependent typing via Generalized Algebraic Data types. So, theoretically, in OCaml you can encode a function, which type ensures, that two arguments are equal integers. For this you need to use Peano numerals instead of built-in integers, or to annotate built-in integers with phantom type, describing its size. But all this would be rather impractical. It is much easier to write this in Coq, and then extract the definition as an OCaml program.

To summarize, it is impossible to do what you want on a functor level. It is possible, to express such thing using OCaml type system. But it is better to use Coq for this, and keep things simple in OCaml.

Upvotes: 1

antron
antron

Reputation: 3847

No, I don't believe it is possible for the list of fields (of the signature) of the result module of a functor to depend on the argument modules in this way. I think the only kind of dependency you can get is type substitution.

Upvotes: 0

Related Questions