{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Polysemy.Several
  ( HList (..),
    TypeMap,
    Append,
    runSeveral,
  )
where

import Data.Kind
import Polysemy

------------------------------------------------------------------------------

-- | A list capable of storing values of different types. Creating an HList
-- looks like.
--
-- > 1 ::: "test" ::: True ::: HNil
infixr 5 :::

data HList a where
  HNil :: HList '[]
  (:::) :: a -> HList (b :: [Type]) -> HList (a ': b)

------------------------------------------------------------------------------

-- | A map function over type level lists. For example, the following two
-- lines are equivalent:
--
-- > TypeMap Reader [Int, String, False]
-- > [Reader Int, Reader String, Reader Bool]
type family TypeMap (f :: a -> b) (xs :: [a]) where
  TypeMap _ '[] = '[]
  TypeMap f (x ': xs) = f x ': TypeMap f xs

------------------------------------------------------------------------------

-- | Type-level append.
--
-- > Append [Int, String] [Bool]
-- > [Int, String, Bool]
type family Append (a :: [t]) (b :: [t]) where
  Append '[] b = b
  Append (a ': as) b = a ': Append as b

------------------------------------------------------------------------------

-- | A helper function for building new runners which accept HLists intsead of
-- individual elements. If you would normally write
--
-- > f 5 . f "Text" . f True
--
-- then this function can turn that into
--
-- > runSeveral f (True ::: "Text" ::: 5 ::: HNil)
--
-- For example, a runReaders function could be implemented as:
--
-- > runReaders :: HList t -> Sem (TypeConcat (TypeMap Reader t) r) a -> Sem r a
-- > runReaders = runSeveral runReader
--
-- @since 0.1.0.0
runSeveral ::
  (forall r' k x. k -> Sem (e k ': r') x -> Sem r' x) ->
  HList t ->
  Sem (Append (TypeMap e t) r) a ->
  Sem r a
runSeveral f (a ::: as) = runSeveral f as . f a
runSeveral _ HNil = id