Considerations for bidirectional parsing

[endgame]

Following on from the reddit discussion at: https://www.reddit.com/r/haskell/comments/icm66e/abstracting_over_applicative_alternative/

A couple of thoughts about how product-profunctors could better support this use case. Suppose we have a printer/parser profunctor pair: data PPPP a b = PPPP (Printer a) (Parser b) with ProductProfunctor and SumProfunctor instances (likely derived from the Product (Clown Printer) (Joker Parser) construction). Then it should be possible (in a separate library, which I might try to build at some point) to build a series of combainators that work on Sum/ProductProfunctors and provide an Applicative/Alternative-esque experience:

(-*-) :: ProductProfunctor p => p a a -> p b b -> p (a, b) (a, b)
(-|-) :: SumProfunctor p => p a a -> p b b -> p (Either a b) (Either a b)

1. generics-eot is very useful for pulling apart/putting together nearly-arbitrary structures in this way. Having (***!) and empty would keep code symmetric with (+++!) and potentially zero (see below) inside the library; please reconsider its potential deprecation.
2. generics-eot unconditionally ends the alternation between constructors with a Void, which means that we'd want a SumProfunctor p => p Void Void to finish handling chains of alternatives. I see a comment in the SumProfunctor class about zero being omitted because it didn't appear useful; are you open to adding it?

[tomjaguarpaw]

I'm not sure what you mean about the Applicative/Alternative-esque experience. Are you suggesting adding synonyms (-*-) for p2 and (-|-) for (+++!)? I don't see the connection to an Applicative/Alternative-esque experience. Those combinators are actually quite far away from how we use Applicatives and Alternatives in practice!

We use (<$>), (<*>) and pure for Applicatives, which correspond to (***$), (****) and purePP and the latter have been much more convenient for me when using product profunctors than p2/(***!).

The situation for SumProfunctor (and Decidable) is much less promising because of the The Mysterious Incomposability of Decidable. If you have a satisfactory way of composing SumProfunctors I would love to hear about it! The closest thing to a satisfactory solution that I have found is to use a free arrow and use arrow notation to compose SumProfunctors (and Decidables). It has the drawback that it requires a special notation and is not type safe.

1. I don't plan to remove the functionality ProductProfunctor p => p a a -> p b b -> p (a, b) (a, b). It's in the library under the name p2. However I don't see that it is particularly useful as a type class method. Do you have an argument to the contrary?

2. Sure, seems reasonable, although I would probably use the type zero :: p Void a which is strictly more general. On the other hand, Divisible has lose :: (a -> Void) -> f a so perhaps I should understand their rationale in case losePP :: (a -> Void) -> p a b would be better.

[endgame]

This is what I have in a scratch space. I'm not sure if I want to restrict myself to a single type variable (as below), or expose both type variables from the profunctors. The idea is to glue a Contravariant and a Functor together (presumably one is the encoder, and the other a decoder for a given type):

newtype PPPP f g a = PPPP { runPPPP :: Product (Clown f) (Joker g) a a }

infixr 3 -$-
infixr 4 -|-
infixr 4 -|
infixr 4 |-
infixr 5 -*-
infixr 5 -*
infixr 5 *-

(-$-)
  :: (Contravariant f, Functor g)
  => (a -> b, b -> a) -> PPPP f g a -> PPPP f g b
(-$-) (f, g) = PPPP . dimap g f . runPPPP

(-*-)
  :: (Divisible f, Applicative g)
  => PPPP f g a -> PPPP f g b -> PPPP f g (a, b)
PPPP fga -*- PPPP fgb = PPPP $ fga ***! fgb

(-*)
  :: (Divisible f, Applicative g)
  => PPPP f g a -> PPPP f g () -> PPPP f g a
PPPP fga -* PPPP fgu = (fst, (,())) -$- PPPP (fga ***! fgu)

(*-)
  :: (Divisible f, Applicative g)
  => PPPP f g () -> PPPP f g a -> PPPP f g a
PPPP fgu *- PPPP fga = (snd, ((),)) -$- PPPP (fgu ***! fga)

(-|-)
  :: (Decidable f, Alternative g)
  => PPPP f g a -> PPPP f g b -> PPPP f g (Either a b)
PPPP fga -|- PPPP fgb = PPPP $ fga +++! fgb

(-|)
  :: (Decidable f, Alternative g)
  => PPPP f g a -> PPPP f g Void -> PPPP f g a
PPPP fga -| PPPP fgv = (either id absurd, Left) -$- PPPP (fga +++! fgv)

(|-)
  :: (Decidable f, Alternative g)
  => PPPP f g Void -> PPPP f g a -> PPPP f g a
PPPP fgv |- PPPP fga = (either absurd id, Right) -$- PPPP (fgv +++! fga)

Here's an example use:

eot :: HasEot a => (Eot a -> a, a -> Eot a)
eot = (fromEot, toEot)

char :: Char -> PPPP Printer Parser ()
char = undefined

string :: String -> PPPP Printer Parser ()
string = undefined

make :: PPPP Printer Parser String
make = undefined

model :: PPPP Printer Parser String
model = undefined

int :: PPPP Printer Parser Int
int = undefined

rocket :: PPPP Printer Parser ()
rocket = undefined

data Car = Car
  { _make :: String
  , _model :: String
  , _engine :: Engine
  } deriving Generic

data Engine = Pistons Int | Rocket deriving Generic

ppCar :: PPPP Printer Parser Car
ppCar = eot
  -$- (string "make: " *- make -* char '\n')
  -*- (string "model: " *- model -* char '\n')
  -*- (eot -$- int -*- PPPP P.empty -|- rocket -|- void)
  -*- PPPP P.empty
  -|- void
  where void = PPPP $ Pair (Clown D.lost) (Joker empty)

ppCar looks a lot like a normal Applicative construction, but you get bidirectional printing/parsing if you unpack the PPPP. I'm still not sure exactly what I want (-*-) etc to operate over, but it feels like there could be something neat here.

[tomjaguarpaw]

Can you show your definition of HasEot? That seems rather important!

[endgame]

Comes from generics-eot: HasEot.

Still not certain whether I want to define (-*-) etc over:

• (-*-) :: PPPP f g a -> f g b -> f g (a, b)
• (-*-) :: PPPP' f g a c -> PPPP' f g b d -> PPPP' f g (a, b) (c, d) (splitting type variables)
• (-*-) :: ProductProfunctor p => p a c -> p b d -> p (a, b) (c, d) (working on ProductProfunctor directly)

Or some other variant.

[tomjaguarpaw]

Ah, interesting, so this is very similar to what I came up with in The Mysterious Incomposability of Decidable except what you call -|- I called -*- (and I didn't have the Alternative part). Yes, this is the best way I know of of composing SumProfunctors (short of abusing arrow notation).

[endgame]

Yep, I think we're on the same page. Going back to your earlier comments:

• So long as p2 is kept, the only objection I have to its departure from the ProductProfunctor typeclass is a handwavy symmetry argument with SumProfunctor.
• Generalised void :: SumProfunctor p => p Void a seems ok, but could it be void :: SumProfunctor p => p a b? The reason we can have a generalised empty :: ProductProfunctor p => p a () is because we have (implied for now) class (Profunctor p, forall a. Applicative (p a)) => ProductProfunctor p. Similarly we should be able to have class (Profunctor p, forall a . Alternative (f a)) => SumProfunctor p, so should we be able to use Control.Applicative.empty to get that?
• Perhaps this means that empty :: ProductProfunctor p => p a () should be removed to avoid name clashes?

• Divisible has (a -> Void) for this reason: if you look at my blog post or Ed's Discrimination is Wrong video at 25:27, we see this table:

  pureish    :: Applicative f => (()   ->    a) -> f a
  emptyish   :: Alternative f => (Void ->    a) -> f a
  conquerish :: Divisible   f => (a    ->   ()) -> f a
  lose       :: Decidable   f => (a    -> Void) -> f a

  • The arguments are the arrows to/from the unit of the monoidal category that we're coming from with our monoidal functor.
  • pureish becomes pure by recognising that in a lazy language, () -> a is equivalent to a. (Not true in strict languages.)
  • emptyish becomes empty by recognising that there is exactly one arrow Void -> a (absurd), so no point providing it.
  • conquerish becomes conquer for the same reason (const ())
  • lose can't be simplified.

  Maybe that helps?

But I think that if the connection between Alternative and SumProfunctor is sound (and I suspect it is but I just woke up), then we can just use Control.Applicative.Empty without having to glom additional functions into the SumProfunctor class.

[tomjaguarpaw]

Generalised void :: SumProfunctor p => p Void a seems ok, but could it be void :: SumProfunctor p => p a b?

Not as far as I can tell.

The reason we can have a generalised empty :: ProductProfunctor p => p a () is because we have (implied for now) class (Profunctor p, forall a. Applicative (p a)) => ProductProfunctor p.

Hmm, it's true that we implicitly have that superclass constraint (in fact it is equivalent to ProductProfunctor) but I think that might be a mirage in this case. As I see it the reason that we have p a () is because we have p () () and we can lmap (const ()) (similar to conquerish, as you explain below). We can't start from p Void Void and get p a Void (though we can get p Void a).

Similarly we should be able to have class (Profunctor p, forall a . Alternative (f a)) => SumProfunctor p, so should we be able to use Control.Applicative.empty to get that?

I don't see why this correspondence should necessarily hold.

Divisible has (a -> Void) for this reason

I'm not sure what you're saying here. a -> Void isn't inhabited unless a isn't inhabited so it doesn't allow us to get f a in general.

[endgame]

[...] the reason that we have p a () is because we have p () () and we can lmap (const ()) (similar to conquerish, as you explain below). We can't start from p Void Void and get p a Void (though we can get p Void a).

Right, so we must have p () () as the unit, which we can lmap (const ()) to get p a () which unifies with p () () so we may as well provide it as the typeclass method. For SumProfunctor, p Void Void is the unit, so from rmap absurd we get p Void a, which unifies, so it may as well be the unit.

Similarly we should be able to have class (Profunctor p, forall a . Alternative (f a)) => SumProfunctor p

I don't see why this correspondence should necessarily hold.

I think you're right. I tried to build newtype Alt p a b = Alt (p a b) and write an instance (SumProfunctor p, Applicative (Alt p a)) => Alternative (Alt p a) and failed. It's a bit surprising to me that it doesn't, given that it does for ProductProfunctor. The Applicative-style (****) relies on being able to lmap (\a -> (a, a)). The corresponding operation for SumProfunctor requires you to construct an a -> Either a a which has two candidates and no way to choose the right one.

Divisible has (a -> Void) for this reason

I'm not sure what you're saying here. a -> Void isn't inhabited unless a isn't inhabited so it doesn't allow us to get f a in general.

That was what I was trying to get at. For Decidable you need to prove that a is impossible (provide a -> Void) to consider it handled (get your f a). And there's no way to simplify this obligation (hence, mysterious incomposability).

---

Summary: to get the pool of operators I want, I think the only real change I need is for SumProfunctor to require a unit. I can get the ProductProfunctor unit from pure, and p2 will remain in the library, so they're fine. The best candidate we've found for a SumProfunctor unit is probably void :: SumProfunctor p => p Void a.

[sjoerdvisscher]

Maybe SumProfunctor p is equivalent to (Profunctor p, forall b. Decidable (Flip p b))?

[tomjaguarpaw]

Maybe SumProfunctor p is equivalent to (Profunctor p, forall b. Decidable (Flip p b))?

Aha, this seems plausible.

[endgame]

By the way, are there any plans to introduce quantified superclasses?

[tomjaguarpaw]

By the way, are there any plans to introduce quantified superclasses?

I haven't really considered it. What would be the benefit?

[tomjaguarpaw]

to get the pool of operators I want, I think the only real change I need is for SumProfunctor to require a unit

Yes, seems like a good thing for this library to provide.

[endgame]

By the way, are there any plans to introduce quantified superclasses?

I haven't really considered it. What would be the benefit?

It's "more right", I guess? Like how there are eventual plans to have a quantified functor superclass for Bifunctor.

[endgame]

Now that #64 is up for consideration (again), I don't think there's anything to do on this issue. When we get symmetric and unital sum/product profunctor classes, I'll have a play with my codec projects and see which operators are useful and generic enough to offer up to this package.