Profunctor exploration in less than 100 lines of Haskell

Date: October 30, 2018 Last modified: October 30, 2018
{-# 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