gistfile1.txt

{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances, TypeFamilies, PolyKinds, GADTs, MultiParamTypeClasses, FunctionalDependencies, RankNTypes, DataKinds #-}
import Data.Kind
import Prelude hiding (id, (.), Functor(..), Monad(..), Monoid(..))

-- 'Category k' is a category whose objects are 'Ob k a => a' and whose
-- morphisms (of kind *) are '(Ob k a, Ob k b) => k a b'
class Category (k :: o -> o -> *) where
	type Ob (k :: o -> o -> *) (a :: o) :: Constraint
	id :: Ob k a => k a a
	(.) :: (Ob k a, Ob k b, Ob k c) => k b c -> k a b -> k a c

-- The Hask category
instance Category (->) where
	type Ob (->) a = ()
	id = \x -> x
	f . g = \x -> f (g x)

-- 'Functor f k l' is the functor from 'k' to 'l' such that 'a' is mapped
-- to 'f a' and morphism 'm' is mapped to 'fmap m'
class Functor (f :: o -> q) (k :: o -> o -> *) (l :: q -> q -> *) | f -> k l where
	fmap :: k a b -> l (f a) (f b)

-- A natural transformation between two functors from 'k' to 'l':
-- from 'Functor f k l' to 'Functor g k l'
data NT k l f g where
	NT :: (Functor f k l, Functor g k l) => { runNT :: forall a. f a -> g a } -> NT k l f g

-- The category of functors: [k, l]. Objects here are functors and morphisms
-- are natural transformations between them
instance Category (NT k l) where
	type Ob (NT k l) a = Functor a k l
	id = NT $ \x -> x
	NT f . NT g = NT $ \x -> f (g x)

-- A composition of two functors
data Compose fg a where
	Compose :: { getCompose :: f (g a) } -> Compose '(f, g) a

-- A composition of two functors is a functor
instance (Functor f l (->), Functor g k l) => Functor (Compose '(f, g)) k (->) where
	fmap f (Compose x) = Compose (fmap (fmap f) x)

data Cartesian (k :: o -> o -> *) (l :: q -> q -> *) (ac :: (o, q)) (bd :: (o, q)) where
	Cartesian :: { first :: k a b, second :: l c d } -> Cartesian k l '(a, c) '(b, d)

type family Fst p where Fst '(a, b) = a
type family Snd p where Snd '(a, b) = b

instance (Category k, Category l) => Category (Cartesian k l) where
	type Ob (Cartesian k l) x = (x ~ '(Fst x, Snd x), Ob k (Fst x), Ob l (Snd x))
	id = Cartesian id id
	Cartesian ff fs . Cartesian gf gs = Cartesian (ff . gf) (fs . gs)

-- Composition is an endobifunctor in the category of endofunctors (of Hask)
instance Functor Compose (Cartesian (NT (->) (->)) (NT (->) (->))) (NT (->) (->)) where
	fmap (Cartesian (NT f) (NT g)) = NT $ \(Compose x) -> Compose $ f (fmap g x)

-- A monoidal category is a category equipped with an endobifunctor and an
-- identity object such that there exist associative and unit natural
-- isomorphisms
class Functor p (Cartesian k k) k => Monoidal k p | p -> k where
	type Id p :: o -> o
	assoc :: (Ob k a, Ob k b, Ob k c) => k (p '(p '(a, b), c)) (p '(a, p '(b, c)))
	coassoc :: (Ob k a, Ob k b, Ob k c) => k (p '(a, p '(b, c))) (p '(p '(a, b), c))
	leftUnit :: Ob k a => k (p '(Id p, a)) a
	coleftUnit :: Ob k a => k a (p '(Id p, a))
	rightUnit :: Ob k a => k (p '(a, Id p)) a
	corightUnit :: Ob k a => k a (p '(a, Id p))

newtype Identity a = Identity { runIdentity :: a }

instance Functor Identity (->) (->) where
	fmap f (Identity x) = Identity $ f x

-- The category of endofunctors is monoidal under composition and the identity
-- functor
instance Monoidal (NT (->) (->)) Compose where
	type Id Compose = Identity
	assoc = NT $ Compose . fmap Compose . getCompose . getCompose
	coassoc = NT $ Compose . Compose . fmap getCompose . getCompose
	leftUnit = NT $ runIdentity . getCompose
	coleftUnit = NT $ Compose . Identity
	rightUnit = NT $ fmap runIdentity . getCompose
	corightUnit = NT $ Compose . fmap Identity

data Proxy a = Proxy

-- Object f is a monoid in a monoidal category if there is a pair of morphisms
-- from f*f to f, and from the identity to f
class Monoidal k p => Monoid f k p | f p -> k where
	mappend :: k (p '(f, f)) f
	-- Id can be noninjective so we have to pass p, the monoidal structre
	-- bifunctor in some way
	mempty :: Proxy p -> k (Id p) f

-- A monad is just a monoid in the category of endofunctors
return :: Monoid f (NT (->) (->)) Compose => a -> f a
return = runNT (mempty (Proxy :: Proxy Compose)) . Identity

join :: Monoid f (NT (->) (->)) Compose => f (f a) -> f a
join = runNT mappend . Compose

-- Maybe is an object in End(Hask)
instance Functor Maybe (->) (->) where
	fmap f = maybe Nothing (Just . f)

-- Maybe is a monoid
instance Monoid Maybe (NT (->) (->)) Compose where
	mappend = NT $ maybe Nothing id . getCompose
	mempty _ = NT $ Just . runIdentity

-- Now if we pick a different endobifunctor:
data Apply fg a where
	Apply :: f x -> g y -> (x -> y -> a) -> Apply '(f, g) a

instance (Functor f (->) (->), Functor g (->) (->)) => Functor (Apply '(f, g)) (->) (->) where
	fmap f (Apply fx gy xya) = Apply fx gy ((f .) . xya)

instance Functor Apply (Cartesian (NT (->) (->)) (NT (->) (->))) (NT (->) (->)) where
	fmap (Cartesian (NT f) (NT g)) = NT $ \(Apply fx gy xya) -> Apply (f fx) (g gy) xya

-- It creates a different monoidal structure on the same End(Hask) category:
instance Monoidal (NT (->) (->)) Apply where
	type Id Apply = Identity
	assoc = NT $ \(Apply (Apply fx gy xyz) hw zwa) -> Apply fx (Apply (fmap (flip xyz) gy) (fmap (flip zwa) hw) (flip (.))) (flip id)
	coassoc = NT $ \(Apply fx (Apply gy hz yzw) xwa) -> Apply (Apply (fmap xwa fx) (fmap yzw gy) (.)) hz id
	leftUnit = NT $ \(Apply (Identity x) gy xya) -> fmap (xya x) gy
	coleftUnit = NT $ \ga -> Apply (Identity ()) ga (const id)
	rightUnit = NT $ \(Apply fx (Identity y) xya) -> fmap (flip xya y) fx
	corightUnit = NT $ \fa -> Apply fa (Identity ()) const

-- Applicative is, too, just a monoid in the category of endofunctors:
pure :: Monoid f (NT (->) (->)) Apply => a -> f a
pure = runNT (mempty (Proxy :: Proxy Apply)) . Identity

(<*>) :: Monoid f (NT (->) (->)) Apply => f (a -> b) -> f a -> f b
f <*> k = runNT mappend $ Apply f k id

instance Monoid Maybe (NT (->) (->)) Apply where
	mappend = NT $ \(Apply mx my xya) -> maybe Nothing (\x -> fmap (xya x) my) mx
	mempty _ = NT $ Just . runIdentity