Having fun with universal constructions for And and Or types and the correspondance of pairs (fanout, bimap) and (either, fanin) for each.

CatTheory.UniversalConstructions.purs

-- Module to demonstrate simple applications of the concept of universal construtions
module CatTheory.UniversalConstructions
       -- * Types
       ( And (..)
       , Or (..)
       -- * Introducers
       , and
       , left
       , right
       , fanin
       -- * Eliminators
       , fanout
       , first
       , second
       -- * Combinators
       , bimap
       , either
       ) where

import Control.Category ((>>>))
import Data.Show (class Show, show)
import Data.Semigroup ((<>))

-- | Represents data that contains both a value of type `a` and type `b`
data And a b = And a b

instance showAnd :: (Show a, Show b) => Show (And a b) where
  show (And a b) = "(" <> show a <> " , " <> show b <> ")"

-- | Represents data that either holds a value of type `a` or type `b`
data Or a b = Left a | Right b

instance showOr :: (Show a, Show b) => Show (Or a b) where
  show (Left a) = "Left " <> show a
  show (Right b) = "Right " <> show b

-- | non-infix smart constructor for And
and = And

-- | Alias for `Left` data constructor which creates a value of `Or a b` from an `a` value
-- >>> left 42
-- Left 42 :: Or Int _
left :: forall a b. a -> Or a b
left = Left

-- | Alias for `Right` data constructor which creates a value of `Or a b` from a `b` value
-- >>> right "meaning of life"
-- Right "meaning of life" :: Or _ String
right :: forall a b. b -> Or a b
right = Right

-- | Produces the first element of an `And` value of type `a`
-- >>> first (And 42 "meaning of life")
-- 42 :: Int
first :: forall a b. And a b -> a
first (And a _) = a

-- | Produces the second element of an `And` value of type `b`
-- >>> second (And 42 "meaning of life")
-- "meaning of life" :: String
second :: forall a b. And a b -> b
second (And _ b) = b

-- | Given a function taking a value of type `c` that produces a value of `And a b`
-- we can produce the equivalent repesentation of an `And` with the correspondly
-- scoped functions in each element
fanin
  :: forall a b c
  .  (c -> And a b)
  -> And (c -> a) (c -> b)
fanin h = And (h >>> first) (h >>> second)
-- Beginner friendly version below; the above and below lines are equivalent:
-- fanin h = And (\c -> first (h c)) (\c -> second (h c))

-- | Given a value of type `And` containing functions from `c` to each respective component
-- wecan produce a function from `c` to an `And` value of the corresponding constituent results.
fanout
  :: forall a b c
  .  And (c -> a) (c -> b)
  -> (c -> And a b)
fanout (And f g) = \c -> And (f c) (g c)

-- | Map over both parts of the `And` value using different functions in the same structure.
bimap
  :: forall a b a' b'
  .  And (a -> a') (b -> b')
  -> (And a b -> And a' b')
bimap (And f g) = \(And a b) -> And (f a) (g b)

-- | Function version of pattern matching over both data constructors of `Or a b` (namely `Left`, `Right`).
either
  :: forall a b c
  .  (a -> c)
  -> (b -> c)
  -> (Or a b -> c)
either f _ (Left a)  = f a
either _ g (Right b) = g b