Membership proof rewrite, membership testing, compose effect

[KingoftheHomeless]

Making this a draft since the Compose effect is WIP.

Closes #281 if we're happy with KnownRow+subsumeUsing.

[KingoftheHomeless]

Are subsumeMembership, extendMembership, and weakenList generally interesting enough to warrant a spot in an internal module not named Polysemy.Compose.Internal?

[isovector]

I dream of a day when we can use the same subsume and raise and weaken etc. functions, regardless of whether we're working on a Union, Membership or Sem.

[KingoftheHomeless]

Decided to put these in Polysemy.Bundle.Internal for now.

[isovector]

I quite like this from a casual look through --- it's very elegant and much easier to follow than my original implementation. Thanks for putting it together; I'll go through more closely later today!

[googleson78]

Do you have some source/writeup/blogpost for this - I haven't encountered it before it and it seems rather interesting?(especially the constraints in unconsKnownList)

[KingoftheHomeless]

I adapted a trick I learned ways back (don't remember where from) for pattern-matching on type-level expressions at run-time.
I don't actually know of a writeup for this, but the original pattern came from the following way of encoding type-level naturals:

data Nat = Z | S Nat

class KnownNat (n :: Nat) where
  induceNat :: (n ~ 'Z => a) -> (forall n'. (n ~ ('S n'), KnownNat n') => Proxy n' -> a) -> a

instance KnownNat 'Z where
  induceNat b _ = b

instance KnownNat n => KnownNat ('S n) where
  induceNat _ i = i Proxy

Basically, given a type-level Nat, you can do induction on it by providing what you'll do in case it's 'Z -- and when defining that case, you get to know that n ~ 'Z -- and what you'll do in case it's 'S n' -- and in that case, you get to know that n ~ 'S n'. This is the same pattern, except for lists instead.

I think nowadays this pattern has been replaced by singletons, although I'm not sure.

[TheMatten]

It seems to be this symmetry between existential wrapper/CPS - singleton basically encodes those possible cases as datatype instead of call to continuation.

[KingoftheHomeless]

We probably want a module to expose ElemOf(..), membership, subsumeUsing, KnownRow, tryMembership, and exposeUsing, right? What should it be called? Polysemy.Membership?

[isovector]

Can you walk me through what the Compose effect does?

[KingoftheHomeless]

It's just an effect for collecting a number of effects into one umbrella, mainly so that you can make effect newtypes more powerful.

For example:

newtype Bridge i o m a = Bridge { unBridge :: Compose '[Input i, Output o] m a }

injCompose :: Member e r => e m a -> Compose r m a
injCompose = Compose membership

receive :: Member (Bridge i o) r => Sem r i
receive = transform (Bridge . injCompose) input

deliver :: Member (Bridge i o) r => o -> Sem r ()
deliver o = transform (Bridge . injCompose) (output o) 

runBridge :: Sem r i -> (o -> Sem r ()) -> Sem (Bridge i o ': r) a -> Sem r a
runBridge inp out =
    runOutputSem out
  . runInputSem inp
  . runCompose
  . rewrite unBridge

Haven't checked if this type-checks, but you get the gist. I should actually offer injCompose, didn't think about rewrite/transform.

[isovector]

Thanks, that's super helpful and cool!

[isovector]

Do we have a way to generalize this with the new machinery? I've always hated having to write a few blessed raise functions.

[KingoftheHomeless]

No, there's nothing that the new membership proof machinery can help on this point.

This should be implementable, though:

type family Underneath n r e where
  Underneath 'Z r e = e ': r
  Underneath ('S n) (x ': r) e = x ': Underneath n r e

raiseUnderX :: SNat n -> Sem r a -> Sem (Underneath n r e) a

[isovector]

This comment suggests that this thing can never get stuck. Is that true? If so, how does it work?

[KingoftheHomeless]

The comment is just so newcomers won't get scared about "what do I need to have KnownRow be satisfied?"; the instances defined take care of it eventually.

It won't always work out so cleanly. Given a type variable s, in order for State s ': r to be KnownRow you need to specify that s is a Typeable.

[isovector]

Why the indirection?

[KingoftheHomeless]

Partly to get right order on type variables, but mainly so that we have Member as the constraint, rather than the internal Find.

[isovector]

I really like this. Left lots of comments because I don't 100% understand it yet, but the reification feels right.

[isovector]

I think I've lost the forest for the trees here. Can you give a paragraph summary of what this accomplishes (even if it's just making the Union module more elegant)

[KingoftheHomeless]

So the old proof had two components to it -- SNat n and IndexOf r n ~ e. More than simply making things ugly, the fact that part of the proof is a type equality constraint on IndexOf makes it hard to work with. Notably, pattern matching on the SNat n tells the type system nothing about r! You can't deduce r ~ x ': r' from n ~ 'Z or n ~ S n'. IIRC, I couldn't implement runCompose under the old proof mechanism because of this.

When it comes to reification, a recent thought I had makes the gains there less concrete. A Member constraint dictionary à-la Has in #281 has the flaws I detailed in #281 (comment). However, a proper reification is possible through the following:

data Membership r e where
  Membership :: (IndexOf r n ~ e) => SNat n -> Membership r e

This probably works; you should be able to base KnownRow, subsumeUsing, exposeUsing on it. Still, it's pretty ugly (and inefficient) that you need a wrapper, especially considering it's only needed because the proof is partly represented through a constraint when it doesn't need to be.

In short: this solution is prettier, as the entire proof is now represented by one datatype, and makes playing around with membership more cleaner. In addition, ElemOf provides extra information that makes certain stuff that was impossible before now possible, and it shouldn't affect performance.

[isovector]

I'm sold.

…

On Thu, Nov 28, 2019 at 4:27 AM KingoftheHomeless ***@***.***> wrote: So the old proof had two components to it -- SNat n and IndexOf r n ~ e. More than simply making things ugly, the fact that part of the proof is a type equality constraint on IndexOf makes it hard to work with. Notably, pattern matching on the SNat n tells the type system nothing about r! You can't deduce r ~ x ': r' from n ~ 'Z or n ~ S n'. IIRC, I couldn't implement runCompose under the old proof mechanism because of this. When it comes to reification, a recent thought I had makes the gains there less concrete. A Member constraint dictionary à-la Has in #281 <#281> has the flaws I detailed in #281 (comment) <#281 (comment)>. However, a proper reification *is* possible through the following: data Membership r e where Membership :: (IndexOf r n ~ e) => SNat n -> Membership r e This probably works; you should be able to base KnownRow, subsumeUsing, exposeUsing on it. Still, it's pretty ugly (and inefficient) that you need a wrapper, especially considering it's only needed because the proof is partly represented through a constraint when it doesn't need to be. In short: this solution is prettier, as the entire proof is now represented by one datatype, and makes playing around with membership more cleaner. In addition, ElemOf provides extra information that makes certain stuff that was impossible before now possible, and it *shouldn't* affect performance. — You are receiving this because your review was requested. Reply to this email directly, view it on GitHub <#282?email_source=notifications&email_token=AACLAFYYG2BNPW4DTSFIHEDQV3Q5PA5CNFSM4JQ7NXMKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEFKZJAA#issuecomment-559256704>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AACLAFZ237M77QHGCNG7TYDQV3Q5PANCNFSM4JQ7NXMA> .

-- I'm currently travelling the world, sleeping on people's couches and doing full-time collaboration on Haskell projects. If this seems interesting to you, please consider signing up as a host! https://isovector.github.io/erdos/