Explicit intro and elim pattern

IntroElim.hs

{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-partial-fields #-}

module Elim where

import Data.Kind
import Prelude

-- | A typeclass for introducing a type.
--
-- This is just a "smart constructor pattern".
class Intro b where
  type To b a :: Type
  produce :: To b a -> a -> b

-- | A typeclass for eliminating a type.
--
-- This is a "smart destructor" pattern, something which is less seen.
class Elim a where
  type From a (c :: Type) :: Type
  use :: From a c -> a -> c

-- Example: eliminator for Either:
data Either' a b c = Either'
  { left :: a -> c,
    right :: b -> c
  }

instance Elim (Either a b) where
  type From (Either a b) c = Either' a b c
  use Either' {..} = \case
    Left x -> left x
    Right x -> right x

-- Using it is like using the 'either' function:
example :: Either Int String -> String
example = use Either' {left = show, right = id}

data Foo
  = Foo1 Int String
  | Foo2 Int Int

data Foo' c = Foo'
  { foo1 :: Int -> String -> c,
    foo2 :: Int -> Int -> c
  }

instance Elim Foo where
  type From Foo c = Foo' c
  use Foo' {..} = \case
    Foo1 x y -> foo1 x y
    Foo2 x y -> foo2 x y

jam :: Either (Either Foo Foo) Foo -> String
jam =
  use
    Either'
      { left =
          use
            Either'
              { left =
                  use
                    Foo'
                      { foo1 = \x y -> show x ++ y,
                        foo2 = const (const "hello")
                      },
                right =
                  use
                    Foo'
                      { foo1 = const (const "world"),
                        foo2 = \x y -> show (x + y)
                      }
              },
        right =
          use
            Foo'
              { foo1 = \x y -> show x ++ y,
                foo2 = \x y -> show x ++ show y
              }
      }

-- In the above cases the types we gave for `From a t` have just been isomorphic
-- to the type `a -> t`.
--
-- Things are more interesting when the type is /not/ isomorphic.

data Role = Admin | Regular

data Role' t = Role'
  { admin :: t,
    regular :: t
  }

instance Elim Role where
  type From Role c = Role' c
  use Role' {..} = \case
    Admin -> admin
    Regular -> regular

-- Internal user type, constructor not exported.
data User = User
  { name :: String,
    role :: Role
  }

instance Elim User where
  -- By giving this type as the eliminator, we "force" users of our type to
  -- discriminate on the role.
  type From User c = From Role (String -> c)
  use fromUser User {..} = use fromUser role name

-- E.g. in order to write this function, the user must use the 'use' function,
-- which requires them to give two different cases, one for each role.
giveAccess :: User -> Bool
giveAccess =
  use $
    Role'
      { admin = const True,
        regular = (== "bill")
      }

-- Since we don't export 'User', we better also provide a ToIntro:
instance Intro User where
  type To User t = t -> String

  -- this is a smart constructor where we enforce that all new users start off
  -- as 'Regular'.
  produce namer t =
    User
      { name = namer t,
        role = Regular
      }

-- Another example where we hide implementation details:

-- unexported type
data Zim = Zim
  { zim :: Int,
    zam :: Int,
    zimzam :: Int -- this is an internal optimisation detail.
  }

-- exported
data Zim' = Zim'
  { zim :: Int,
    zam :: Int
  }

instance Elim Zim where
  type From Zim c = Zim' -> c
  use f Zim {..} = f Zim' {..}

instance Intro Zim where
  type To Zim t = t -> Zim'
  produce f x =
    let Zim' {..} = f x
     in Zim {zimzam = zim + zam, ..}

fooo :: Zim -> String
fooo = use $ \Zim' {..} -> show zim ++ " and " ++ show zam

-- Another example:
-- quotient types, i.e. types which need to be normalised sometimes.
--
-- - internal code: normalise when needed
--
-- - 'use' and 'produce', which represent the interface to the outside world,
-- - normalise.

-- Another example:

data Bar = Bar Int Int

-- In this case we declare that there are two usual ways to eliminate a 'Bar':
--
-- One can think of this as a declarative way to give all "covering"
-- pattern-match collections a user should use.
data Bar' t
  = -- | One case where you are mainly interested in if they sum to 100, in
    -- which case only one field is relevant:
    Sum100
      { yes :: Int -> t,
        no :: Int -> Int -> t
      }
  | -- | And another case where you are interested in if they are equal:
    Diag
      { equal :: Int -> t,
        unequal :: Int -> Int -> t
      }

instance Elim Bar where
  type From Bar t = Bar' t
  use Sum100 {..} (Bar x y)
    | x + y == 100 = yes x
    | otherwise = no x y
  use Diag {..} (Bar x y)
    | x == y = equal x
    | otherwise = unequal x y

-- We can choose how to build a 'Bar':

example2 :: Bar -> String
example2 =
  use
    Diag
      { equal = \x -> "both are " ++ show x,
        unequal = \x y -> show x ++ "/=" ++ show y
      }

example3 :: Bar -> String
example3 =
  use
    Sum100
      { yes = \x -> "yay 100! : " ++ show x,
        no = \_ _ -> "still some ways to go.."
      }