IntroElim3.hs

{-# LANGUAGE LiberalTypeSynonyms #-}

module ElimAgainAgain where

import Control.Applicative
import Control.Category
import Control.Lens hiding (cons)
import Data.Generics.Labels ()
import GHC.Generics
import Prelude hiding (either, head, id, tail, (.))

-- | Natural transformation
type f ~> g = forall t. f t -> g t

type From = (->)

type To b a = a -> b

-- What is an eliminator of 'a'
type Elim a f = f ~> From a

-- infix version
type f -< a = f ~> From a

-- What is an introducer of 'a'
type Intro a f = f ~> To a

-- infix version
type f >- a = f ~> To a

-- The functor 'To a' is the most obvious eliminator for a:
canonicalElim :: From a -< a
canonicalElim = id

-- The contravariant functor 'From a' is the most obvious introducer for a:
canonicalIntro :: To a >- a
canonicalIntro = id

-- Eliminators can be extended backways via a natural transformation, using (>>>):
extendBack :: (g ~> f) -> (f -< a) -> (g -< a)
extendBack u v = u >>> v

-- Introducers can be extended forwards via a natural transformation, using (>>>) too:
extendForward :: (g ~> f) -> (f >- a) -> (g >- a)
extendForward u v = u >>> v

type PairI a b t = (t -> a, t -> b)

pair :: PairI a b >- (a, b)
pair (f, g) x = (f x, g x)

type From2 a b t = a -> b -> t

-- | 'uncurry' is the eliminator for pairs
usePair :: From2 a b -< (a, b)
usePair = uncurry

data Role = Admin | Normal

data Role' admin normal = Role' {admin :: admin, normal :: normal}
  deriving stock (Generic)

type RoleE t = Role' t t

-- Note that here we rely on Haskell's laziness.
useRole :: RoleE -< Role
useRole Role' {..} = \case
  Admin -> admin
  Normal -> normal

-- small example of using an eliminator:
printRole :: Role -> String
printRole = useRole Role' {admin = "admin", normal = "normal"}

-- A natural transformation, essentially saying how booleans can represent roles.
isAdmin :: From Bool ~> RoleE
isAdmin b =
  Role'
    { admin = b True,
      normal = b False
    }

accessMessage :: Role -> String
accessMessage = isAdmin >>> useRole $ ("has access: " ++) . show

data User' name age rol = User
  { name :: name,
    age :: age,
    role :: rol
  }

type User = User' String Int Role

-- Here we make a design choice that when creating users, they should always
-- start as 'Normal'.

type UserI t = User' (t -> String) (t -> Int) ()

mkUser :: UserI >- User
mkUser User {..} t =
  User
    { name = name t,
      age = age t,
      role = Normal
    }

-- Here we make a design choice that when processing a 'User', one should always
-- pay special attention to the user's role.
--
-- One can read this as:
-- - to eliminate a User
-- - first eliminate a Role
-- - then eliminate a String and an Int
type UserE t = RoleE (String -> Int -> t)

-- We do this by using 'useRole' in the implementation of 'useUser':
useUser :: UserE -< User
useUser roleE User {..} = useRole roleE role name age

-- E.g. to write the following function, use of 'useUser' makes us fill in two
-- cases, one for normal users, and one for admins.
decideAccess :: User -> Bool
decideAccess =
  useUser
    Role'
      { normal = const . ("bill" ==),
        admin = const (const True)
      }

-- In essence we have given the product type 'User' the API of a sum-type, as if
-- we had defined the original 'User' type like:

data RoledUser
  = AdminUser {name :: String, age :: Int}
  | NormalUser {name :: String, age :: Int}

-- The walking sum type

data Either' left right = Either'
  { left :: left,
    right :: right
  }
  deriving stock (Generic)

type EitherElim a b t = Either' (a -> t) (b -> t)

useEither :: EitherElim a b -< Either a b
useEither Either' {..} = \case
  Left x -> left x
  Right x -> right x

data Foo = Foo Int String | Bar Int

data Foo' foo bar = Foo'
  { foo :: foo,
    bar :: bar
  }
  deriving stock (Generic)

type FooE t = Foo' (Int -> String -> t) (Int -> t)

useFoo :: FooE -< Foo
useFoo Foo' {..} = \case
  Foo x y -> foo x y
  Bar x -> bar x

-- How does one use this to "pattern match" on an Either of Foos?
flom1 :: Either Foo Foo -> Int
flom1 =
  useEither
    Either'
      { left =
          useFoo
            Foo'
              { foo = const,
                bar = id
              },
        right =
          useFoo
            Foo'
              { foo = const length,
                bar = (+ 1)
              }
      }

-- we can use lenses to move the 'useFoo' calls out:

flom2 :: Either Foo Foo -> Int
flom2 =
  Either'
    { left = Foo' {foo = const, bar = id},
      right = Foo' {foo = const length, bar = (+ 1)}
    }
    & #left %~ useFoo
    & #right %~ useFoo
    & useEither

-- We can extract this transformation we did, which was just application of a
-- function, and package it up as its own function. It's simply another
-- eliminator, this time specialsed to eliminating 'Either Foo Foo':

type EitherFoosE t = Either' (FooE t) (FooE t)

eitherFoos :: EitherFoosE -< Either Foo Foo
eitherFoos = #left %~ useFoo >>> #right %~ useFoo >>> useEither

flom3 :: Either Foo Foo -> Int
flom3 =
  eitherFoos
    Either'
      { left = Foo' {foo = const, bar = id},
        right = Foo' {foo = const length, bar = (+ 1)}
      }

-- "Domain specific" eliminators

-- consider a type which is essentially a pair of real numbers:

data Plane = Plane {planeX :: Double, planeY :: Double}

-- We can provide an eliminator which cuts the plane up into two parts:
-- - The diagonal,
-- - The rest

data DiagE t = DiagE
  { diagonal :: Double -> t,
    nonDiagonal :: Double -> Double -> t
  }

diag :: DiagE -< Plane
diag DiagE {..} Plane {..} =
  if planeX == planeY
    then diagonal planeX
    else nonDiagonal planeX planeY

-- Let's play with lists.

data List' nil cons = List'
  { nil :: nil,
    cons :: cons
  }
  deriving stock (Functor, Generic)

data ConsCell a = ConsCell {head :: a, tail :: [a]}

type ListE a t = List' t (ConsCell a -> t)

-- This is the most basic way of consuming lists. It is exactly equivalent to
-- the 'list' function in 'Prelude', but adapted to non-nameless style.
useList :: ListE a -< [a]
useList List' {..} = \case
  [] -> nil
  x : xs -> cons (ConsCell x xs)

-- This framework allows "non-nameless" pointfree programming, similar to
-- lawvere-lang.
sum1 :: [Int] -> Int
sum1 =
  useList
    List'
      { nil = 0,
        cons = head +. (tail >>> sum1)
      }

-- here '(+.)' is just the "pointfree (+)", that is: 'liftA2 (+)'.

-- note that the function 'sum1' handles its own recursivity, 'useList' does not
-- dictate any particular recursion pattern.

-- Let's make a recursive eliminator type:

newtype ListRec a t = ListRec (List' t (a -> ListRec a t))

-- Eliminators are always functors (and introducers are always contravariant functors).
instance Functor (ListRec a) where
  fmap f (ListRec List' {..}) =
    ListRec
      List'
        { nil = f nil,
          cons = fmap f . cons
        }

useListRec :: ListRec a -< [a]
useListRec (ListRec (List' {..})) xs = case xs of
  [] -> nil
  x : rest -> useListRec (cons x) rest

-- To use 'useListRec' one therefore builds a recurive eliminator.

-- Note the use of 'fmap': given a 'ListRec a s', one can form a 'ListRec a t'
-- if one has a function 's -> t'. Thankfully GHC derives this functor instance
-- for free.
sum2 :: [Int] -> Int
sum2 = useListRec go
  where
    go =
      ListRec $
        List'
          { nil = 0,
            cons = \x -> fmap (+ x) go
          }

-- Again sum2 manages its own recursion, but not quite in the same way. This
-- time it must recurse by providing a recursive elimnator to 'useListRec'.

-- This does not mean the same recursion needs to happen at each level however.
-- Consider the following function which handles the first two items of the list
-- specially:

sayList :: [Int] -> String
sayList = useListRec firstly
  where
    firstly = go "Nothing at all!" "First comes" secondly
    secondly = go ", all alone." ", secondly comes" thenly
    thenly = go "." ", then comes" thenly
    go e t next =
      ListRec
        List'
          { nil = e,
            cons = \x -> ((t ++ " " ++ show x) ++) <$> next
          }

-- Finally we have fully managed recursion:

type FoldList a t = List' t (a -> t -> t)

-- This is just an equivalent of 'foldr'
foldList :: FoldList a -< [a]
foldList folder = \case
  [] -> nil folder
  x : xs -> cons folder x (foldList folder xs)

sum3 :: [Int] -> Int
sum3 = foldList List' {nil = 0, cons = (+)}

-- Let's use 'foldList' to print out a list of 'Foo's:

showListOfFoos1 :: [Foo] -> String
showListOfFoos1 =
  foldList
    List'
      { nil = "",
        cons =
          useFoo
            Foo'
              { foo = \i x s -> show i ++ " " ++ x ++ " " ++ s,
                bar = \i s -> show i ++ " " ++ s
              }
      }

-- Again we can lift out the various 'use' calls:

showListOfFoos2 :: [Foo] -> String
showListOfFoos2 =
  List'
    { nil = "",
      cons =
        Foo'
          { foo = \i x s -> show i ++ " " ++ x ++ " " ++ s,
            bar = \i s -> show i ++ " " ++ s
          }
    }
    & #cons %~ useFoo
    & foldList

-- And package this up as an eliminator in its own right:

type ListOfFooE t = List' t (FooE (t -> t))

foldListFoos :: ListOfFooE -< [Foo]
foldListFoos = #cons %~ useFoo >>> foldList

showListOfFoos3 :: [Foo] -> String
showListOfFoos3 =
  foldListFoos
    List'
      { nil = "",
        cons =
          Foo'
            { foo = \i x s -> show i ++ " " ++ x ++ " " ++ s,
              bar = \i s -> show i ++ " " ++ s
            }
      }

-- Here is another eliminator, which sees if the items of a list can be paired up:

data Parity even odd = Parity
  { even_ :: even,
    odd_ :: odd
  }
  deriving stock (Generic)

type Pairwise a t = Parity ([(a, a)] -> t) t

pairwise :: Pairwise a -< [a]
pairwise Parity {..} = \case
  [] -> even_ []
  [_] -> odd_
  x : y : rest -> pairwise Parity {even_ = even_ . ((x, y) :), ..} rest

-- Let's imagine we are interested in the "first class pattern matching" which
-- consists of matching for either a list a things which can be paired up twice,
-- or a Foo.

type PairsOfPairsOrFoo a t = Either' (Parity (Pairwise (a, a) t) t) (FooE t)

pairsOfPairsOrFoo :: PairsOfPairsOrFoo a -< Either [a] Foo
pairsOfPairsOrFoo =
  #left . #even_ %~ pairwise
    >>> #left %~ pairwise
    >>> #right %~ useFoo
    >>> useEither

-- The result gives us an eliminator with all the cases we should consider:
weird :: Either [Foo] Foo -> String
weird =
  pairsOfPairsOrFoo
    Either'
      { left =
          Parity
            { even_ =
                Parity
                  { even_ = length >>> show >>> ("number of pairs of pairs: " ++),
                    odd_ = "couldn't form pairs of pairs"
                  },
              odd_ = "couldn't form pairs"
            },
        right =
          Foo'
            { foo = const (const "some foo"),
              bar = const "some bar"
            }
      }

-- Pointfree versions of common functions

(+.) :: Num n => (a -> n) -> (a -> n) -> (a -> n)
(+.) = liftA2 (+)