iso-parsing example

[hanshoglund]

This is an application/extension of iso-deriving to parsing/pretty-printing.

The idea is simple:

• Describe a BNF-style grammar as type-level expression
• Define a type constructor Parse :: Grammar -> Type, giving us a canonical AST for any such grammar

Here is an example. The grammar L accepts expressions such as {}, {1,2,3}, etc.

type L =
  Then
    ( Keyword "{"
    )
    ( Then
        (SepBy1 PrimNat (Keyword ","))
        (Keyword "}")
    )

Now Parse L defines an AST for this grammar, with the expected instances for Show and Read. The requirement that read . show = id = show . read is automatically satisfied.

We may want a more idiomatic AST for this type. We define such a type and iso-derive Read and Show.

newtype Foo = Foo [Int] -- Our "AST"
  deriving (Read, Show) via (Parse L `As` Foo)

The isomorphism is straightforward.

instance Inject (Parse L) Foo where
  inj (PT PK (PT (PS a) PK)) = Foo $ fmap (\(PN x) -> x) a

instance Project (Parse L) Foo where
  prj (Foo xs) = PT PK $ PT (PS $ fmap PN xs) PK

What does PK, PN etc. mean? They are the type constructors of Parse. We can read them as "parse of keyword", "parse of a natural etc" etc.

data Parse :: Syntax -> Type where
  PK :: KnownSymbol s => Parse (Keyword s)
  PM :: [Parse a] -> Parse (Many1 a)
  PS :: [Parse a] -> Parse (SepBy1 a sep)
  PN :: Int -> Parse PrimNat
  PT :: Parse a -> Parse b -> Parse (Then a b)