5 ms·

Neither Haskell's nor OCaml's functors are the same as the mathematical one I believe, but both are similar in some way that the word makes sense to be used for

Neither Haskell's nor OCaml's functors are the same as the mathematical one I believe, but both are similar in some way that the word makes sense to be used for their respective feature. In OCaml, functors map between an abstract module and some concrete one. And in Haskell functors are structures that can have a function that maps over their elements. In math a functor is a map between categories. So you can see how all three kinda make sense as functors, but also are different in exactly what they are.

tome 6y ago
Both Haskell's and OCaml's functors are special cases of the general mathematical one.
- sweeneyrod 6y ago
  How? What are the categories that OCaml's Hashtbl.Make maps between? What are the morphisms in those categories and how are they mapped?
  - tome 6y ago
    It maps between a category with HashedType implementations as objects and a category with Make implementations as objects. Unfortunately it's not a very interesting functor because to satisfy the functor laws I think the categories have to be discrete. It's basically a function! (And functions are indeed a special case of functors.) https://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.Make.html https://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.M...
    - sweeneyrod 6y ago
      Right, in other words it is just a function. I don't think the categories have to be discrete just to satisfy the functor laws; even ignoring that, what would the morphisms be in principle? I don't think there is an obvious choice, at least. I think in OCaml, "functor" basically just means "like a function but for modules". They might technically be categorical functors, but it seems quite different to the meaning in Haskell where they are plainly categorical functors (modulo Hask technically not being a category).
      - tome 6y ago
        Agreed, I'm not sure it's a terribly interesting functor.
      - Iceland_jack 6y ago
        Here is one way one might implement a categorical Functor (https://www.reddit.com/r/haskell/comments/eoo16m/base_category_polymorphic_functor_and_functorof/ https://www.reddit.com/r/haskell/comments/eoo16m/base_catego...). A function S -> T maps a S(ource) type to a T(arget) type, like FunctorOf (-S>) (-T>) does between the source category (-S>) and target category (-T>) type Functor :: forall (s :: Type) (t :: Type). (s -> t) -> Constraint class (Category (Src f), Category (Tgt f)) => Functor (f :: s -> t) where type Src (f :: s -> t) :: Cat s type Tgt (f :: s -> t) :: Cat t fmap :: Src f a1 a2 -> Tgt f (f a1) (f a2) type FunctorOf :: forall (s :: Type) (t :: Type). Cat s -> Cat t -> (s -> t) -> Constraint type FunctorOf src tgt f = (Functor f, Src f ~ src, Tgt f ~ tgt) The usual endofunctor type EndofunctorOf :: forall (ob :: Type). Cat ob -> (ob -> ob) -> Constraint type EndofunctorOf @ob cat f = FuntorOf @ob @ob cat cat f we have in Haskell can be defined as FunctorOf @Type @Type (->) (->), or type OldFunctor :: (Type -> Type) -> Constraint type OldFunctor f = EndofunctorOf @Type (->) f
        Iceland_jack 6y ago
        For simplicity written with a type synonym, but it cannot be partially applied. So I would use constraint synonym encoding (https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#constraint-synonym-encoding-or-class-synonym https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025...) type FunctorOf :: forall (s :: Type) (t :: Type). Cat s -> Cat t -> Constraint class (Functor f, Src f ~ src, Tgt f ~ tgt) => FunctorOf src tgt f instance (Functor f, Src f ~ src, Tgt f ~ tgt) => FunctorOf src tgt f The other definitions can be eta reduced type EndofunctorOf cat = FunctorOf cat cat type OldFunctor = EndofunctorOf (->)

tome 6y ago

Both Haskell's and OCaml's functors are special cases of the general mathematical one.

sweeneyrod 6y ago
How? What are the categories that OCaml's Hashtbl.Make maps between? What are the morphisms in those categories and how are they mapped?
- tome 6y ago
  It maps between a category with HashedType implementations as objects and a category with Make implementations as objects. Unfortunately it's not a very interesting functor because to satisfy the functor laws I think the categories have to be discrete. It's basically a function! (And functions are indeed a special case of functors.) https://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.Make.html https://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.M...
  - sweeneyrod 6y ago
    Right, in other words it is just a function. I don't think the categories have to be discrete just to satisfy the functor laws; even ignoring that, what would the morphisms be in principle? I don't think there is an obvious choice, at least. I think in OCaml, "functor" basically just means "like a function but for modules". They might technically be categorical functors, but it seems quite different to the meaning in Haskell where they are plainly categorical functors (modulo Hask technically not being a category).
    - tome 6y ago
      Agreed, I'm not sure it's a terribly interesting functor.
    - Iceland_jack 6y ago
      Here is one way one might implement a categorical Functor (https://www.reddit.com/r/haskell/comments/eoo16m/base_category_polymorphic_functor_and_functorof/ https://www.reddit.com/r/haskell/comments/eoo16m/base_catego...). A function S -> T maps a S(ource) type to a T(arget) type, like FunctorOf (-S>) (-T>) does between the source category (-S>) and target category (-T>) type Functor :: forall (s :: Type) (t :: Type). (s -> t) -> Constraint class (Category (Src f), Category (Tgt f)) => Functor (f :: s -> t) where type Src (f :: s -> t) :: Cat s type Tgt (f :: s -> t) :: Cat t fmap :: Src f a1 a2 -> Tgt f (f a1) (f a2) type FunctorOf :: forall (s :: Type) (t :: Type). Cat s -> Cat t -> (s -> t) -> Constraint type FunctorOf src tgt f = (Functor f, Src f ~ src, Tgt f ~ tgt) The usual endofunctor type EndofunctorOf :: forall (ob :: Type). Cat ob -> (ob -> ob) -> Constraint type EndofunctorOf @ob cat f = FuntorOf @ob @ob cat cat f we have in Haskell can be defined as FunctorOf @Type @Type (->) (->), or type OldFunctor :: (Type -> Type) -> Constraint type OldFunctor f = EndofunctorOf @Type (->) f
      - Iceland_jack 6y ago
        For simplicity written with a type synonym, but it cannot be partially applied. So I would use constraint synonym encoding (https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#constraint-synonym-encoding-or-class-synonym https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025...) type FunctorOf :: forall (s :: Type) (t :: Type). Cat s -> Cat t -> Constraint class (Functor f, Src f ~ src, Tgt f ~ tgt) => FunctorOf src tgt f instance (Functor f, Src f ~ src, Tgt f ~ tgt) => FunctorOf src tgt f The other definitions can be eta reduced type EndofunctorOf cat = FunctorOf cat cat type OldFunctor = EndofunctorOf (->)