Category theory in Haskell

Category.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Prelude (($), Either(..), Eq(..), Ord(..))

-- https://www.youtube.com/watch?v=Klwkt9oJwg0

type family (~>) :: i -> i -> *
type instance (~>) = (->)
type instance (~>) = Nat
type instance (~>) = Nat
type instance (~>) = (:-)

-- Without `PolyKinds` the kind of `Category` is `(* -> * -> *) -> Constraint`
-- while with `PolyKinds` it is `(k -> k -> *) -> Constraint`.
class h ~ (~>) => Category (h :: k -> k -> *) where
  id :: h a a
  (.) :: h b c -> h a b -> h a c

instance Category (->) where
  id x = x
  (.) f g x = f (g x)

-- When defined with `->` and without `PolyKinds` the kind of `Nat` is
-- `(* -> *) -> (* -> *) -> *` while with `PolyKinds` it is
-- `(k -> *) -> (k -> *) -> *`. When defined with `~>` its kind is 
-- `(i -> j) -> (i -> j) -> *`.
newtype Nat (f :: i -> j) (g :: i -> j) =
  Nat { runNat :: forall a. f a ~> g a }

-- This instance doesn't work without `PolyKinds`.
instance Category ((~>) :: j -> j -> *) =>
  Category (Nat :: (i -> j) -> (i -> j) -> *) where
  id = id
  Nat f . Nat g = Nat (f . g)

class Functor (f :: i -> j) where
  fmap :: (a ~> b) -> f a ~> f b

instance Functor (Either a) where
  fmap f (Left a) = Left a
  fmap f (Right b) = Right (f b)

instance Functor Either where
  fmap f = Nat $ \case
    Left a -> Left (f a)
    Right b -> Right b

class Contravariant (f :: i -> j) where
  contramap :: (a ~> b) -> f b ~> f a

-- The kind of `Dict` is `Constraint -> *`.
data Dict p where
  Dict :: p => Dict p

newtype a :- b = Sub (a => Dict b)

(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r

instance Category (:-) where
  id = Sub Dict
  f . g = Sub $ Dict \\ f \\ g

foo :: Ord a :- Eq a
foo = Sub Dict

bar :: Eq a :- Eq [a]
bar = Sub Dict

baz :: Ord a :- Eq [a]
baz = bar . foo