3 ms·

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

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