ADT Algebra

ADTAlgebra.hs

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}

module ADTAlgebra where

type Algebra f a = f a -> a
type Coalgebra f a = a -> f a

type Bialgebra f a = (Algebra f a, Coalgebra f a)

newtype Fix f = Fx (f (Fix f))

-- Algebraic data type functor
data ADTF a b = Unit
              | a :|: b
              | a :&: b
              deriving Functor

type (a :+: b) = Either a b
data (a :*: b) = Pair a b

type ADT a = Fix (ADTF a)

alg :: ADTF a b -> (a :+: b)
alg Unit      = Right ()
alg (a :|: b) = 
alg (a :&: b) = Right (a :*: b)

eitherMaybe.hs

module EitherMaybe where

-- Prove: Maybe a ~ Either () a ~ Either a ().
--
-- data Maybe a = Nothing | Just a
-- data Either a b = Left a | Right b
--
-- We have the following equivalences:
--  Maybe a
--    N ~ 1
--    Just a ~ a,
--  Either a b
--    Left a ~ a
--    Right b ~ b
--
-- We also have the following definitions:
--   Maybe a = 1 + a.
--
-- Either a b  = a + b
--             let a = () = 1
-- Either () b = 1 + b
--             = Maybe b
--

type Maybe' a = Either () a

f :: Maybe a -> Maybe' a
f x = case x of
        Nothing -> Left ()
        Just x' -> Right x'

g :: Maybe' a -> Maybe a
g x = case x of
        Left ()  -> Nothing
        Right x' -> Just x'

NOOB.hs

-- Nothing, One, or Both

data NOOB a b = N | L a | R b | LR a b

--
-- Prove that NOOB a b ~ NOOB' a b.
-- 
-- We have the following equivalences:
--   N ~ 1
--   L a ~ a
--   R b ~ b
--   LR a b ~ a * b
--
-- We also have the following at our disposal:
--   Either a b = a + b,
--   (,) a b = a * b,
--   Maybe a = a + 1.
--
-- Now we do some type arithmetic:
--   NOOB a b = 1 + a + b + a * b = 1 + a + b + ab
--            = a + ab + b + 1
--            = a * (1 + b) + b + 1
--            = 1 + b + a * (1 + b)
--            let c = b + a * (1 + b)
--                  let d = a * (1 + b)
--                        = (a, Maybe b) in
--                  expand d
--                  = b + d
--                  = b + (a, Maybe b)
--                  = Either b (a, Maybe b) in
--            expand c
--            = 1 + c
--            = 1 + Either b (a, Maybe b)
--            = Maybe (Either b (a, Maybe b))
--            rearrange and replace for simplicity
--            => Maybe (Either a (Maybe a, b))
--            
type NOOB' a b = Maybe (Either a (Maybe a, b))

f :: NOOB a b -> NOOB' a b
f x = case x of
        N    -> Nothing
        L x' -> Just $ Left x'
        R x' -> Just $ Right (Nothing, x')
        LR x' y' -> Just $ Right (Just x', y')

g :: NOOB' a b -> NOOB a b
g x = case x of
        Nothing -> N
        Just (Left x') -> L x'
        Just (Right (Nothing, x')) -> R x'
        Just (Right (Just x', y')) -> LR x' y'

-- (f . g) = id, (g . f) = id

OOB.hs

-- One or Both

data OOB a b = L a | R b | LR a b

--
-- Prove that OOB a b ~ OOB' a b.
--
-- L a    ~ a
-- R b    ~ b
-- LR a b ~ a + b
--
-- OOB a b = a + b + a * b
--         = a + ab + b
--         = a * (1 + b) + b
--         let c = a * (1 + b)
--               = a * Maybe b
--               = a * Either () b
--               = (a, Either () b)
--         = c + b
--         = Either c b
--         expand c
--         = Either (a, Either ()  b) b
--
--
-- 1 + b = Maybe b
-- Maybe b ~ Either () b.
-- 1 + b = Either () b
--
-- Either () b = a + 1
-- Either a b = a + b
--
type OOB' a b = Either (a, Either () b) b

f :: OOB a b -> OOB' a b
f x = case x of
        L x' -> Left (x', Left ())
        R x' -> Right x'
        LR x' y' -> Left (x', Right y')

g :: OOB' a b -> OOB a b
g x = case x of
        Left (x', Left ()) -> L x'
        Right x' -> R x'
        Left (x', Right y') -> LR x' y'