On Tue, 2009-10-13 at 13:28 +0100, Nils Anders Danielsson wrote:
On 2009-10-07 17:29, Robert Atkey wrote:
A deep embedding of a parsing DSL (really a context-sensitive grammar DSL) would look something like the following. I think I saw something like this in the Agda2 code somewhere, but I stumbled across it when I was trying to work out what "free" applicative functors were.
The Agda code you saw may have been due to Ulf Norell and me. There is a note about it on my web page:
http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinat...
Yes, it might have been that, OTOH I'm sure I saw it in some Haskell code. Maybe I was imagining it.
Note that these grammars are strictly less powerful than the ones that can be expressed using Parsec because we only have a fixed range of possibilities for each rule, rather than allowing previously parsed input to determine what the parser will accept in the future.
Previously parsed input /can/ determine what the parser will accept in the future (as pointed out by Peter Ljunglöf in his licentiate thesis). Consider the following grammar for the context-sensitive language {aⁿbⁿcⁿ| n ∈ ℕ}:
Yes, sorry, I was sloppy in what I said there. Do you know of a characterisation of what languages having a possibly infinite amount of nonterminals gives you. Is it all context-sensitive languages or a subset?
And a general definition for parsing single-digit numbers. This works for any set of non-terminals, so it is a reusable component that works for any grammar:
Things become more complicated if the reusable component is defined using non-terminals which take rules (defined using an arbitrary non-terminal type) as arguments. Exercise: Define a reusable variant of the Kleene star, without using grammars of infinite depth.
I see that you have an answer in the paper you linked to above. Another possible answer is to consider open sets of rules in a grammar:
data OpenRuleSet inp exp = forall hidden. OpenRuleSet (forall a. (exp :+: hidden) a -> Rule (exp :+: hidden :+: inp) a)
data (f :+: g) a = Left2 (f a) | Right2 (g a)
So OpenRuleSet inp exp, exports definitions of the nonterminals in 'exp', imports definitions of nonterminals in 'inp' (and has a collection of hidden nonterminals). It is then possible to combine them with a function of type:
combineG :: (inp1 :=> exp1 :+: inp) -> (inp2 :=> exp2 :+: inp) -> OpenRuleSet inp1 exp1 -> OpenRuleSet inp2 exp2 -> OpenRuleSet inp (exp1 :+: exp2)
One can then give a reusable Kleene star by stating it as an open rule set:
star :: forall a nt. Rule nt a -> OpenRuleSet nt (Equal [a])
where Equal is the usual equality GADT. Obviously, this would be a bit clunky to use in practice, but maybe more specialised versions combineG could be given. Bob -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.