{-# LANGUAGE KindSignatures, TypeFamilies, ConstraintKinds, PolyKinds, MultiParamTypeClasses #-}

module Control.Effect where 

import Prelude hiding (Monad(..))
import GHC.Prim


{-| Specifies "parametric effect monads" which are essentially monads but
     annotated by a type-level monoid formed by 'Plus' and 'Unit' -}
class Effect (m :: k -> * -> *) where

   {-| Effect of a trivially effectful computation |-}
   type Unit m :: k
   {-| Cominbing effects of two subcomputations |-}
   type Plus m (f :: k) (g :: k) :: k

   {-| 'Inv' provides a way to give instances of 'Effect' their own constraints for '>>=' -}
   type Inv m (f :: k) (g :: k) :: Constraint
   type Inv m f g = ()

   {-| Effect-parameterised version of 'return'. Annotated with the 'Unit m' effect, 
    denoting pure compuation -}
   return :: a -> m (Unit m) a

   {-| Effect-parameterise version of '>>=' (bind). Combines 
    two effect annotations 'f' and 'g' on its parameter computations into 'Plus' -}
   (>>=) :: (Inv m f g) => m f a -> (a -> m g b) -> m (Plus m f g) b

   (>>) :: (Inv m f g) => m f a -> m g b -> m (Plus m f g) b
   x >> y = x >>= (\_ -> y)
  
fail = undefined

{-| Specifies subeffecting behaviour -}
class Subeffect (m :: k -> * -> *) f g where
    sub :: m f a -> m g a