Haskell is not category theory

Re:Haskell is not category theory by gowld on Friday February 03, 2023 @02:55PM (#34646896)

What is an example of category-theory functor in Haskell, that isn't just an endofunctor?

A functor F from C to D is a mapping that associates each object X in C to an object F(X) in D.

In Haskell, C and D are both the same (Hask types), hence endofunctor (functor into self).

In general a functor could be something like `prime_factorizaton:: Int -> [(Prime Int, Mulitplicity Int)]`, with morphisms being things like the operation

  a => square :: a -> a
  square (n::Integer) = n^2
  square (factorization::[(Prime Int, Mulitplicity Int)]) = map (\(a,b) -> (a, 2*b)))

prime_factorizaton (square) x === square (prime_factorization(x))

[ Parent | on HN ]

Re:Haskell is not category theory by Iceland_jack on Sunday February 05, 2023 @12:22PM (#34666658)

  Either a :: Type -> Type

is a Haskell Functor (endofunctor), mapping (->) to (->).

  Either :: Type -> (Type -> Type)

is not an endofunctor, it maps a type to a type constructor and thus maps (->) to (~>) (natural transformations).

If you uncurried Either, you would also get a non-endofunctor which maps from (-×>) (product category) to (->).

  Either' :: (Type, Type) -> Type

Every function is a functor between equality, since equality satisfies congruence:

  isPrime :: Integer -> Bool

is a functor between (:~:) @Integer an (:~:) @Bool. Boolean negation is a function between "less than or equal" to "greater than or equal" categories; mapping (<=) to (>=):

  not :: Bool -> Bool

[ Parent | on HN ]