Eliminators and Introducers, again

ElimIntro2.hs

{-# LANGUAGE TypeFamilies #-}

module ElimAgain where

import Control.Lens
import Data.Generics.Labels ()
import Data.Kind
import GHC.Generics
import Prelude hiding (either)

type From a = (->) a

-- It's annoying this can't be a type synonym
newtype To b a = To {ap :: a -> b}

type Elim f a = forall t. f t -> a -> t

type Intro f a = forall t. f t -> t -> a

-- The functor ((->) a) is the most obvious eliminator for a:
canonicalElim :: Elim (From a) a
canonicalElim = id

canonicalIntro :: Intro (To a) a
canonicalIntro (To f) = f

data Pair a b t = Pair (a t) (b t)

pair :: Intro (Pair (To a) (To b)) (a, b)
pair (Pair (To f) (To g)) x = (f x, g x)

data User = User
  { name :: String,
    age :: Int
  }

data User' name age t = User'
  { name :: name t,
    age :: age t
  }

toUser :: Intro (User' (To String) (To Int)) User
toUser User' {..} t =
  User
    { name = ap name t,
      age = ap age t
    }

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

useEither :: Either' (From a) (From b) t -> Either a b -> t
useEither Either' {left} (Left x) = left x
useEither Either' {right} (Right x) = right x

data Foo = Foo Int String | Bar Int

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

useFoo :: Elim (Foo' (From (Int, String)) (From Int)) Foo
useFoo Foo' {..} (Foo x y) = foo (x, y)
useFoo Foo' {..} (Bar x) = bar x

flom1 :: Either Foo Foo -> Int
flom1 =
  useEither
    Either'
      { left =
          useFoo
            Foo'
              { foo = fst,
                bar = id
              },
        right =
          useFoo
            Foo'
              { foo = fst,
                bar = id
              }
      }

flom3 :: Either Foo Foo -> Int
flom3 =
  Either'
    { left = Foo' {foo = fst, bar = id},
      right = Foo' {foo = fst, bar = id}
    }
    & #left %~ useFoo
    & #right %~ useFoo
    & useEither

eitherFoos ::
  Elim
    ( Either'
        (Foo' (From (Int, String)) (From Int))
        (Foo' (From (Int, String)) (From Int))
    )
    (Either Foo Foo)
eitherFoos = useEither . (#right %~ useFoo) . (#left %~ useFoo)

flom4 :: Either Foo Foo -> Int
flom4 =
  eitherFoos
    Either'
      { left = Foo' {foo = fst, bar = id},
        right = Foo' {foo = fst, bar = id}
      }

-- summing a list

data List' a empty cons t = List'
  { empty_ :: empty t,
    cons_ :: cons t
  }

emptyCons :: Elim (List' a (From ()) (From (a, [a]))) [a]
emptyCons List' {empty_} [] = empty_ ()
emptyCons List' {cons_} (x : xs) = cons_ (x, xs)

data PairedList a odd empty consPair t = PairedList
  { odd_ :: odd t,
    empty_ :: empty t,
    consPair :: consPair t
  }

pairedList :: Elim (PairedList a (From ()) (From ()) (From ((a, a, [a])))) [a]
pairedList PairedList {empty_} [] = empty_ ()
pairedList PairedList {odd_} [_] = odd_ ()
pairedList PairedList {consPair} (x : y : rest) = consPair (x, y, rest)

-- This framework encourages "non-nameless" pointfree programming, similar to
-- lawvere-lang.
sum' :: [Int] -> Int
sum' =
  emptyCons
    List'
      { empty_ = const 0,
        cons_ = fst +. (sum' . snd)
      }

-- A type class to say how you expect consumers of your type to consume it properly:

data UseList a t
  = Simple (List' a (From ()) (From (a, [a])) t)
  | Paired (PairedList a (From ()) (From ()) (From ((a, a, [a]))) t)

class Eliminated a where
  type Eliminator a :: Type -> Type
  with :: Elim (Eliminator a) a

instance Eliminated [a] where
  type Eliminator [a] = UseList a
  with (Simple x) = emptyCons x
  with (Paired x) = pairedList x

sum'' :: [Int] -> Int
sum'' =
  with $
    Simple $
      List'
        { empty_ = const 0,
          cons_ = fst +. (sum' . snd)
        }

pairSum :: [Int] -> Maybe [Int]
pairSum =
  with $
    Paired $
      PairedList
        { empty_ = const (Just []),
          odd_ = const Nothing,
          consPair = \(x, y, rest) -> (x + y :) <$> pairSum rest
        }

-- Pointfree versions of common functions

(+.) :: Num n => (a -> n) -> (a -> n) -> (a -> n)
(+.) f g x = f x + g x