Implementing a category-theoretic Hask-monad in Haskell

Monad law 1: µ • (µ . F) = µ • (F . µ)
Monad law 2: µ • (η . F) = µ • (F . η) = I
f :: Int -> Int
f x = x + 1
g :: Int -> Int
g 0 = 142857
g _ = 0
 — | The identity functor on Hask as it behaves on objects.
iObj :: a -> a
iObj = id
— | The identity functor on Hask as it behaves on arrows.
iArr :: (a -> b) -> (a -> b)
iArr = id
 — | F, a Hask endofunctor, as it behaves on objects.
fObj :: (Applicative f) => a -> f a
fObj = pure
— | F, a Hask endofunctor, as it behaves on arrows.
fArr :: (Applicative f) => (a -> b) -> (f a -> f b)
fArr = fmap
— | F^2 = F . F, a Hask endofunctor, as it behaves on objects.
f2Obj :: (Applicative f) => a -> f (f a)
f2Obj = fObj . fObj
— | F^2 = F . F, a Hask endofunctor, as it behaves on arrows.
f2Arr :: (Applicative f) => (a -> b) -> (f (f a) -> f (f b))
f2Arr = fArr . fArr
Fig. 1. A transformation (not natural without condition shown in Fig. 2)
Fig. 2. A natural transformation γ
Fig. 3. µ : F^2 →. F, a natural transformation
µ :: a -> ([[a]] -> [a])
µ _ = concat
µ :: a -> (Maybe (Maybe a) -> Maybe a)
µ _ (Just (Just a)) = Just a
µ _ (Just Nothing) = Nothing
µ _ Nothing = Nothing
Fig. 4. η : I →. F, a natural transformation
η :: a -> (a -> [a])
η _ = \a -> [a]
η :: a -> (a -> Maybe a)
η _ = \a -> Just a
η :: (Applicative f) => a -> (a -> f a)
η _ = fObj
Fig. 5. The (natural) transformation η
> ghci
λ let plus :: Int -> Int -> Int; plus x y = x + y
λ quickCheck (\x y -> x `plus` y == y `plus` x)
+++ OK, passed 100 tests.
{- 
I h
I a -------> I b
| |
| η a | η b
| |
v v
F a -------> F b
F h
-}
testη :: (Monad' m, Eq (m HV)) => MonadImpl m -> Fun HaskellValue HaskellValue -> [HaskellValue] -> Bool
testη fArr' (Fun _ h) = all
(\a -> let b = h a in
(η b . iArr h $ iObj a) == (fArr' h . η a $ iObj a))
{-
F^2 h
F^2 a ----> F^2 b
| |
| µ a | µ b
| |
v v
F a ------> F b
F h
-}
testµ :: (Monad' m, Eq (m HV)) => MonadImpl m -> Fun HV HV -> [m (m HV)] -> Bool
testµ _ (Fun _ h) = all
(\mma ->
(µ undefined . f2Arr h $ mma) == (fArr h . µ undefined $ mma))
{"elephant"->1, "monkey"->1, _->0}
Fig. 2 (reproduced)
testη :: Fun a b -> [a] -> Bool
data HaskellValue
= A String
| B Int
| C Bool
| D Char
| E (Either (Bool, Char, [Bool]) [Maybe (Maybe Int)])
deriving (Show, Eq)
{D 'x'->C True, D 'a'->C True, D 'n'->C False, _->C False}
Monad Law 1: µ • (µ . F) = µ • (F . µ)
Monad Law 2: µ • (η . F) = µ • (F . η) = I
Fig. 6. Vertical composition of the functions µ and η
(•) :: (a -> (ga -> ha)) -> (a -> (fa -> ga)) -> (a -> (fa -> ha))
µ • η = \a -> µ a . η a
-- Monad law 1: µ • (µ . F) = µ • (F . µ)
testLaw1 :: (Monad' m, Eq (m HV)) => MonadImpl m -> m (m (m HaskellValue)) -> Bool
testLaw1 _ mmma
= (µ • (µ . fObj)) undefined mmma == (µ • (fArr . µ)) undefined mmma
-- Monad law 2: µ • (η . F) = µ • (F . η) = I
testLaw2 :: (Monad' m, Eq (m HV)) => MonadImpl m -> m HV -> Bool
testLaw2 _ ma = and
[ iObj ma == (µ • (η . fObj)) undefined ma
, iObj ma == (µ • (fArr . η)) undefined ma ]
-- (transitively µfη = µηf)
class (Applicative m) => Monad’ m where
µ :: a -> (m (m a) -> m a)
instance (Monad' m) => Monad m where
return :: (Monad m) => a -> m a
return = pure -- can also use `η undefined`
(>>=) :: (Monad m) => m a -> (a -> m b) -> m b
ma >>= f = µ undefined . fmap f $ ma
λ (Fun _ h) <- generate (arbitrary :: Gen (Fun HaskellValue HaskellValue))
λ h (B 5)
D ‘f’
λ h (B 6)
C False
λ h (B 7)
B 3
λ h (B 8)
C True

--

--

Love podcasts or audiobooks? Learn on the go with our new app.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store