>However, if F is an ML functor, then there are no "maps" between the modules F(A) and F(B).
Yes there is, the functor. Just repeating a false statement won't make it come true.
Yes there is, the functor. Just repeating a false statement won't make it come true.
What we have is a functor F, which would be defined as in:
module F =
functor (X: S) -> ....
> Just repeating a false statement won't make it come true.
Exactly!
If you want to claim a relation between OCaml functors and category-theoretic functors, then you must be able to justify your claims. Saying "functors represent functions from a module to a module. Oh hey, that sounds just like the standard definition of a functor." is just not a convincing argument.
That is literally the functor. Seriously, read the chapter on modules.
That would be an answer for Haskell (though a proper one would refer to fmap), but it does not work like that in OCaml. You do know some OCaml, right?
But if it's so obvious, then you can say how it works for the following concrete example:
module type S = sig
type t
val f: t -> int
end
module F = functor (X: S) -> struct
type s = X.t * X.t
let g x = X.f x + X.f x
end
module A : S = struct
type t = float
let f x = int_of_float x
end
module B : S = struct
type t = int
let f x = 2*x
end
module X = F(A)
module Y = F(B)
The point is: In the ML module system there is no equivalent to fmap: (A -> B) -> (F A -> F B), i.e. the functor action on morphisms. So, functors in Haskell and OCaml are different things. If you want to claim otherwise, you'll have to make an actual argument for it.
NB You only need to get from X to Y in ways that arise from getting from A to B. Since there doesn't seem to be any relevant concept of morphism it's hard to see how ML functors are anything other than trivially category theoretical.