Algebraic Effects in Haskell

gistfile1.hs

{-# OPTIONS -Wall #-}

{-# LANGUAGE GADTs, DataKinds, TemplateHaskell, KindSignatures,
    MultiParamTypeClasses, RankNTypes, PolyKinds, FlexibleContexts,
    TypeFamilies, UndecidableInstances, FlexibleInstances #-}

module Effects where

import Data.Singletons

-- kind Effect = * > * -> * -> *
$(singletons [d|
    
    data Effect res res' t = Effect res res' t

    |])

class Handler (e :: * -> * -> * -> *) (m :: * -> *) where
    handle :: res -> e res res' t -> (res' -> t -> m a) -> m a

data EFFECT :: * where
    MkEff :: (res :: *) -> SEffect e -> EFFECT

{- Effect -}
data State :: * -> * -> * -> * where
    Get :: State a a a
    Put :: b -> State a b ()

instance Handler State m where
    handle n Get      k = k n n
    handle _ (Put n') k = k n' ()

-- everything get's a bit funky when i try to figure out EFFECT
type STATE t = MkEff t State
-- Effects.hs:35:16:
--     `MkEff' of type `forall (k :: BOX)
--                             (k :: BOX)
--                             (k :: BOX)
--                             res
--                             (e :: Effect k k k).
--                             res -> SEffect k k k e -> EFFECT' is not promotable
--                           In the type `MkEff t State'
--                         In the type declaration for `STATE'
--