{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Profunctors where
import Data.Either
import Data.Maybe
import Data.Functor
import Data.Function ((.), ($))
class Iso a b where
to :: a -> b
from :: b -> a
-- law: a = from . to a
type Lens s t a b
= forall p. Strong (p :: * -> * -> *) => p a b -> p s t
type Prism s t a b
= forall p. Choice (p :: * -> * -> *) => p a b -> p s t
class Profunctor (p :: * -> * -> *) where
dimap :: (a -> b) -> (c -> d) -> (p b c -> p a d)
-- laws:
-- dimap identity identity = identity
-- dimap (f' . f) (g . g') = dimap f g · dimap f' g'
instance Profunctor (->) where
dimap f g h = g . h . f
class Profunctor p => Strong (p :: * -> * -> *) where
first' :: p a b -> p (a, c) (b, c)
class Profunctor p => Choice (p :: * -> * -> *) where
left' :: p a b -> p (Either a c) (Either b c)
class Profunctor p => Cartesian (p :: * -> * -> *) where
first :: p a b -> p (a, c) (b, c)
second :: p a b -> p (c, a) (c, b)
-- laws:
-- dimap runit runit' h = first h
-- dimap assoc assoc' (first (first h)) = first h
-- where
-- runit :: (a, ()) -> a
-- runit' :: a -> (a, ())
-- assoc :: (a, (b, c)) -> ((a, b), c)
-- assoc' :: ((a, b), c) -> (a, (b, c))
instance Cartesian (->) where
first f (a, c) = (f a, c)
second f (c, a) = ( c, f a)
class Profunctor p => Monoidal p where
par :: p a b -> p c d -> p (a, c) (b, d)
empty :: p () ()
-- laws:
-- dimap assoc assoc' (par (par h j) k) = par h (par j k)
-- dimap runit runit' h = par h empty
-- dimap lunit lunit' h = par empty h
-- where
-- lunit :: ((), a) -> a
-- lunit' :: a -> ((), a)
-- runit :: (a, ()) -> a
-- runit' :: a -> (a, ())
instance Monoidal (->) where
par f g (a, c) = (f a, g c)
empty = identity
-- Natural transformations
type f ~> g = forall x. f x -> g x
-- Examples of natural transformations
-- safeHead :: [a] -> Maybe a
safeHead :: [] ~> Maybe
safeHead [] = Nothing
safeHead (a: _) = Just a
-- singletonList :: Maybe a -> [a]
singletonList :: Maybe ~> []
singletonList Nothing = []
singletonList (Just a) = [a]
-- Reader and the Yoneda Lemma
newtype Reader a x
= Reader { runReader :: a -> x }
instance Functor (Reader a) where
fmap f x = Reader (f . runReader x)
newtype Yoneda f a = Yoneda {
runYoneda :: Functor f => Reader a ~> f
}
toYoneda :: Functor f => f a -> Yoneda f a
toYoneda fa = Yoneda (\x -> fmap (runReader x) fa)
fromYoneda :: Functor f => Yoneda f a -> f a
fromYoneda yo = runYoneda yo (Reader identity)
-- auxilliary functions
identity :: a -> a
identity a = a
flip :: (b -> a -> c) -> a -> b -> c
flip f a b = f b a
If you enjoyed this content, please consider sharing this link with a friend, following my GitHub, Twitter/X or LinkedIn accounts, or subscribing to my RSS feed.