{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators #-}
{-# LANGUAGE DataKinds, PolyKinds, FlexibleContexts, FlexibleInstances #-}

module WhyNot
  ( type (?)
  , Handles (..)
  , Result
  , Return
  , handle
  , whynot
  ) where

import Data.Kind (Type)
import CPS (CPS(..))

-- | The result of the effect.
type family Result (h :: Type) :: Type

-- | Girard's "why not?" monad parameterized by an effect 'h'andler.
-- @((->) h)@ is equivalent to the @Reader@ monad where computations have
-- access to effect handlers.
-- The purpose of the 'Handles' typeclass is to keep track of the accumulated
-- constraints imposed on 'h' as an effect computation is evaluated.
-- Since 'CPS' is a control-flow monad which can 'lift' any arbitrary effects
-- from 'm' (when 'm' is a monad) we are effectively have constructed an effect
-- routing monad which may not be able to actually perform all the effects, but
-- nonetheless account for them in the types in the form of constraints.
type h ? a = CPS (Result h) ((->) h) a

-- | The immediate value returned from an effect invocation.
type family Return (opApp :: Type) :: Type

-- | A predicate indicating that the handler type 'h' can perform the side-
-- effects of the action 'op'.
class Handles (h :: Type) (op :: j -> k -> Type) where
  -- | tbd this removes the need for a fundep
  type Ex h op :: j
  -- | Handles an action and applies the continuation to it.
  clause
    :: (e ~ Ex h op)
    => op e u
    -> ( Return (op e u) -> ( h -> Result h ) )
    -> ( h -> Result h )

-- | A synonym of '(#)' for clarity.
handle :: (h ? a) -> (a -> (h -> Result h)) -> (h -> Result h)
handle :: forall h a. (h ? a) -> (a -> h -> Result h) -> h -> Result h
handle = forall k (result :: k) (m :: k -> *) answer.
CPS result m answer -> (answer -> m result) -> m result
(#)

-- | Action constructor.
-- In delimited continuations terms, this is similar to 'shift'.
whynot
  :: (h `Handles` op, e ~ Ex h op)
  => op e u
  -> h ? Return (op e u)
whynot :: forall {k} {k} h (op :: k -> k -> *) (e :: k) (u :: k).
(Handles h op, e ~ Ex h op) =>
op e u -> h ? Return (op e u)
whynot op e u
op = forall k (result :: k) (m :: k -> *) answer.
((answer -> m result) -> m result) -> CPS result m answer
CPS (\Return (op e u) -> h -> Result h
k h
h -> forall j k h (op :: j -> k -> *) (e :: j) (u :: k).
(Handles h op, e ~ Ex h op) =>
op e u -> (Return (op e u) -> h -> Result h) -> h -> Result h
clause op e u
op Return (op e u) -> h -> Result h
k h
h)