4 ms·

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 t

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

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 (->)