Conditional effects

[isovector]

I just realized we can use the typeclass machinery to determine whether or not an effect exists in our stack. The machinery (with crap names is this):

data Has e r where
  Has   :: MemberNoError e r => Has e r
  Hasnt :: Has e r

class HasHas (e :: Effect) (r :: EffectRow) where
  hasHas :: Has e r

instance HasHas e '[] where
  hasHas = Hasnt

instance {-# OVERLAPPING #-} HasHas e r => HasHas e (e ': r) where
  hasHas = Has

instance ( HasHas e r
         , IndexOf (e2 ': r) (Found (e2 ': r) e) ~ e
         , Found (e2 ': r) e ~ 'S (Found r e)
         ) => HasHas e (e2 ': r) where
  hasHas =
    case hasHas @e @r of
      Has   -> Has
      Hasnt -> Hasnt

and can be used thusly:

tryGet :: forall s r. HasHas (State s) r => Sem r (Maybe s)
tryGet =
  case hasHas @(State s) @r of
    Has   -> pure <$> get
    Hasnt -> pure Nothing

> run $ runState "hello" $ tryGet @String
("hello",Just "hello")

> run $ tryGet @String
Nothing

I'm not sure what to do with this, but it's pretty neat.

[isovector]

In fact, this generalizes:

try :: forall e r a. HasHas e r => (Member e r => Sem r a) -> Sem r (Maybe a)
try e =
  case hasHas @e @r of
    Has   -> pure <$> e
    Hasnt -> pure Nothing

[KingoftheHomeless]

This kind of power can also be derived from Typeable r. Of course, we don't want that much power, but perhaps it's possible to generalize HasHas in a similar way, like this:

class Concrete r where
  checkMembership :: forall e. Typeable e => Has e r

I'll look into it.

Edit: Actually, I think that would need the more precise proof of #110, because with the current representation, you run into this problem (representing Has through Maybe Membership below):

data Membership e r where
  Membership :: MemberNoError e r => Membership e r

instance (Typeable e, Concrete r) => Concrete (e ': r) where
  checkMembership :: forall e'. Typeable e' => Maybe (Membership e' (e ': r))
  checkMembership = case eqT @e @e' of
    Just Refl -> Just Membership
    _         -> (\Membership -> Membership) <$> checkMembership @r @e'

* Could not deduce: IndexOf (e : r) (Found (e : r) e') ~ e'
    arising from a use of `Membership'
  from the context: Member e' r

Which follows from that the type system can't deduce that e is not e' (which can't be represented anyway).

With HasHas, the fix for this is the number of type equality constraints on the inductive step, but you can't have those when you're working over any effect.
If we were to work with Elem instead, (such that checkMembership :: Typeable e => Maybe (Elem r e) you'd only have to slap a In over the result of the recursive call and be done with it.

[KingoftheHomeless]

Actually, #110 wouldn't help with this: you can't deduce Member e r from Elem r e, since Member e r always targets the first occurrence of e in r, while Elem r e could serve as a proof for a later occurrence. The best you can do is:

sendUsing :: Elem r e -> e (Sem r) a -> Sem r a

or

subsumeUsing ::  Elem r e -> Sem (e ': r) a -> Sem r a

What a pain. Perhaps the second variant is good enough?

[expipiplus1]

Looks a little similar to what was being discussed here: #315