Boxed combinators?

[clayrat]

Using combinators on rec appears to be fairly common, and it seems to always require defining helpers to make types align, e.g.:

andbox : All (Box (Parser' s) :-> Box (Parser' t) :-> Box (Parser' (s, t)))
andbox {s} {t} p q = map2 {a=Parser' s} {b=Parser' t} (\p, q => and p q) p q

nelistbox : All (Box (Parser' s) :-> Box (Parser' (NEList s)))
nelistbox {s} p = map {a=Parser' s} nelist p

Should we maybe provide a separate module for these out of the box :), or there's a more elegant solution?

[gallais]

The fact that Induction.Nat.map nelist p doesn't work out of the box looks like a bug in Idris' elaborator to me: the error mentions an explicit index (j1 : Nat) but the All-defined types only ever work with implicit indices...

So I figured we could use Idiom brackets instead: the problem is just begging for us to throw Applicative at it (we already have map and app and Box (Parser ...) has a pure!).

However I can't seem to declare

Applicative (\ a => Box (Parser' a) n) where

  pure  = box
  (<*>) = Induction.Nat.app

Apparently an implementation cannot mention a universally quantified variable standing for a value. All the arguments have to be either types or constructors...

So I guess there is no other way than to define a TParsec.Combinators.Box with definitions with exactly the same name that can be used qualified. It's a shame.

[clayrat]

Apparently an implementation cannot mention a universally quantified variable standing for a value. All the arguments have to be either types or constructors...

Yeah, that's a known limitation in current Idris. You can do it for named implementations:

[appbox] Applicative (\ a => Box (Parser' a) n) where
  ...

but that will require wrapping every usage of it in using implementation appbox or passing it via the @{..} syntax, which is not so elegant.

There is, however, a light at the end of the tunnel..

[gallais]

Wait. Does that mean that if we had a BoxedParser : Nat -> Type -> Type we would be able to define an instance for BoxedParser n?

[gallais]

Ah. No. Nevermind. Plus it wouldn't fit in the interface anyway because Box's argument is a Nat-indexed Type family, not a mere Type...

[clayrat]

I don't think so, BoxedParser would evaluate to a lambda and cause the exact same error :(

I've just discovered though, that you can in fact inline the helper - writing map {a=Parser' _} nelist rec and map2 {a=Parser' _} {b=Parser' _} (\p,q => and p q) inside a larger expression both seem to work fine.

[gallais]

What if you write map {a=Parser _ _} nelist rec instead? Because if that's enough then we can consider writing a module with specialised versions of map and app!

[clayrat]

Yeah, writing map {a=Parser _ _ _ _} nelist rec works! I'm using 4 params here since the project using this is still based on the master branch.

[gallais]

In the #36 PR I have added a bunch of combinators called some variants of lift that take a function on parsers and make it a function on boxed parsers provided that the return type is a boxed parser.

Once I had this my life was a lot easier as I could propagate the Box wherever I wanted without having to deal with the implicits Idris cannot infer when using map2.