xnning / EvEff

Efficient Haskell effect handlers based on evidence translation.
BSD 3-Clause "New" or "Revised" License
81 stars 5 forks source link

handlerHide2? #3

Open noughtmare opened 3 years ago

noughtmare commented 3 years ago

I'm trying to implement the effect-zoo scenarios to learn how to use this library. I'm stuck on the reinterpretation scenario. The scenario is that there is a Zooit effect that should be decomposed into a HTTP and a Logging effect. It is straightforward to write a naive solution:

{-# language FlexibleContexts #-}
module EffectZoo.Scenario.Reinterpretation.EvEff.Zooit where

import           Control.Ev.Eff
import           EffectZoo.Scenario.Reinterpretation.EvEff.HTTP
import           EffectZoo.Scenario.Reinterpretation.EvEff.Logging

newtype Zooit e ans = Zooit { listScenariosOp :: Op () [String] e ans }

listScenarios :: Zooit :? e => Eff e [String]
listScenarios = perform listScenariosOp ()

toLoggedHTTP :: (HTTP :? e, Logging :? e) => Eff (Zooit :* e) a -> Eff e a
toLoggedHTTP = handler Zooit
  { listScenariosOp = function
                        (\() -> do
                          logMsg "Fetching a list of scenarios"
                          lines <$> httpGET "/scenarios"
                        )
  }

But now the HTTP and Logging effects "leak" to the argument of toLoggedHTTP. If you only want to replace an effect by a single other effect, then you can use handlerHide, but I haven't been able to make that work with replacing one effect by two new effects. Is there a way to do this or do we need a handlerHide2 function?

noughtmare commented 3 years ago

I have been able to implement it like this:

data ContextT e e' where
  CTCons :: !(Marker ans) -> !(h e' ans) -> !(ContextT e e') -> ContextT e (h :* e)
  CTId   :: ContextT e e
  CTCompose :: ContextT e' e'' -> ContextT e e' -> ContextT e e''
  -- CTFun :: !(Context e -> Context e') -> ContextT e e'

-- apply a context transformer
applyT :: ContextT e e' -> Context e -> Context e'
applyT (CTCompose f g) ctx = applyT f (applyT g ctx)
applyT (CTCons m h g) ctx = CCons m h g ctx
applyT (CTId) ctx         = ctx
--applyT (CTFun f) ctx = f ctx

{-# INLINE handlerHide2 #-}
handlerHide2
  :: h (h' :* h'' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* h'' :* e) ans
handlerHide2 h action = Eff
  (\(CCons m1 h1 g1 (CCons m2 h2 g2 ctx')) -> prompt
    (\m -> under
      (CCons m h (CTCompose (CTCons m1 h1 g1) (CTCons m2 h2 g2)) ctx')
      action
    )
  )

Then you can also make it an instance of Category:

instance Category ContextT where
  id = CTId
  (.) = CTCompose

{-# INLINE handlerHide2 #-}
handlerHide2
  :: h (h' :* h'' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* h'' :* e) ans
handlerHide2 h action = Eff
  (\(CCons m1 h1 g1 (CCons m2 h2 g2 ctx')) ->
    prompt
      (\m -> under (CCons m h (CTCons m1 h1 g1 . CTCons m2 h2 g2) ctx') action)
  )

With this definition the original example can be written as:

toLoggedHTTP :: Eff (Zooit :* e) a -> Eff (HTTP :* Logging :* e) a
toLoggedHTTP = handlerHide2 Zooit
  { listScenariosOp = function
                        (\() -> do
                          logMsg "Fetching a list of scenarios"
                          lines <$> httpGET "/scenarios"
                        )
  }

Now the HTTP and Logging are not implicitly added to e.

noughtmare commented 3 years ago

I have been able to make a handlerHideN, but it is not very pretty:


type family xs :++ ys where
  () :++ ys = ys
  (x :* xs) :++ ys = x :* xs :++ ys

data CLenSing c where
  CLZero :: CLenSing ()
  CLSucc :: CLenSing a -> CLenSing (b :* a)

class    KnownCLen c                         where contextLength :: CLenSing c
instance KnownCLen ()                        where contextLength = CLZero
instance KnownCLen xs => KnownCLen (x :* xs) where contextLength = CLSucc (contextLength @xs)

handlerHideN :: forall hs h e ans. KnownCLen hs => h (hs :++ e) ans -> Eff (h :* e) ans -> Eff (hs :++ e) ans
handlerHideN h action = Eff (go (contextLength @hs) CTId) where
  go :: CLenSing hs' -> ContextT (hs' :++ e) (hs :++ e) -> Context (hs' :++ e) -> Ctl ans
  go CLZero ct ctx' = prompt (\m -> under (CCons m h ct ctx') action)
  go (CLSucc cl') ct (CCons m' g' h' ctx') = go cl' (CTCompose ct (CTCons m' g' h')) ctx'

If you want the CTCompose to be associated to the right then you can use:

handlerHideN :: forall hs h e ans. KnownCLen hs => h (hs :++ e) ans -> Eff (h :* e) ans -> Eff (hs :++ e) ans
handlerHideN h action = Eff
  $ (\(ct,ctx') -> prompt (\m -> under (CCons m h ct ctx') action))
  . go (contextLength @hs)
  where
    go :: CLenSing hs' -> Context (hs' :++ e) -> (ContextT e (hs' :++ e), Context e)
    go CLZero ctx' = (CTId, ctx')
    go (CLSucc cl') (CCons m' g' h' ctx') = (CTCompose (CTCons m' g' h') ct, ctx'') where
      ~(ct, ctx'') = go cl' ctx'
xnning commented 3 years ago

The solution with CTCompose for handlerHide2 seems quite neat. Essentially with CTCompose we should be able to write handlerHideN when N is fixed.

I am not sure about the general handlerHideN. It feels quite heavy with type families and GADTs for doing math on types.