Hacker News Reader

Comment by Y_Y | Hacker News Reader

Haskell isn't the functor police! It's on you to define good functors, proving them so would be a totally different endeavour and far more difficult.

I would like to understand better the issue with product types though. What do you want to do that you can't currently.

By the way, most of my knowledge about the connection between Haskell and Category Theory comes from here: https://bartoszmilewski.com/2014/10/28/category-theory-for-p...

View on HN

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

  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

Hmm, well calling it a problem might be a bit much, but it means that functions with more than argument require some additional care, and technically a stronger notion of functor.

Say you have a multivariate function a: X x Y -> Z, and a functor F. This would give you a function F(a): F(X x Y) -> F(Z). Now this is not really multivariate any more as F(X x Y) is not a product, but products behave quite well in category theory so this is not usually that big a problem, and it turns out that quite a few functors are 'continuous' which means they preserve 'limits' and a product is one such limit, in which case F(X) x F(Y) ~= F(X x Y). In particular all right adjoint functors have this property, which is why adjointness is such an important concept.

Now in Haskell things get slightly more difficult, because you don't have a function a: X x Y -> Z, you've got a function a: X -> (Y => Z). Where Y => Z is an object representing all maps from Y to Z (such an object may or may not exist for any particular category). And to use currying you need something like (X * Y) -> Z and X -> (Y => Z) to be isomorphic. So you don't just need F(X x Y) = F(X) x F(Y), which is fairly innocuous, you need to deal with monoidal categories and monoidal functions between them, which is a heck of a lot more complex. This is where the Applicative stuff comes from.

Now some of the stuff you don't get as easily in Haskell is the stuff relying on basic properties of sum and product types, such as

    # The following are the obvious projections for a 2-tuple
    proj1 :: (X x Y) -> X
    proj2 :: (X x Y) -> Y

    # Assuming F(X) x F(Y) exists we get the following for free
    (F(proj1) x F(proj2)) :: F(X x Y) -> F(X) x F(Y)

No clue how you'd state that in Haskell. And the following

    # The following are the obvious projections for a 2-tuple
    anX :: X -> (X + Y)
    anY :: Y -> (X + Y)

    # Assuming F(X) + F(Y) exists we get the following for free
    (F(anX) + F(anY)) :: F(X) + F(Y) -> F(X + Y)

where you can interpret X + Y as an 'Either X Y'.

Sure you could probably write a function

    forall Functor f. Either (f a)  (f b) -> f (Either a b)

but it's not that obvious that it should exist, whereas in category theory it's one of the most obvious constructions imaginable and its existence is clear from the definition. And in Haskell you wouldn't think about using products so the first property is probably barely used anywhere (there's probably a right inverse for zip somewhere: unzip :: [(a,b)] -> ([a],[b]) but Haskell generally doesn't seem to like functions with multiple outputs.

"you don't have a function a: X x Y -> Z, you've got a function a: X -> (Y => Z)"

Haskell has products. What's the problem with f':

ghci> f x y = x + y

ghci> f' (x,y) = x + y

ghci> f 1 2

ghci> f' (1,2)

ghci> :t f'

f' :: Num a => (a, a) -> a

ghci> :t f

f :: Num a => a -> a -> a

Reply on news.ycombinator.com