Boxed combinators?
clayrat opened this issue · 8 comments
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?
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.appApparently 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.
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..
Wait. Does that mean that if we had a BoxedParser : Nat -> Type -> Type we would
be able to define an instance for BoxedParser n?
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...
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.
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!
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.
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.