parsing for PHOAS expressions

Question

I think I understand PHOAS (parametric higher-order abstract syntax), and I see how we can pretty-print an expression (cf. http://www.reddit.com/r/haskell/comments/1mo59h/phoas_for_free_by_edward_kmett/ccbxzoo).

But - I don't see how to build a parser for such expressions, e.g., that takes "(lambda (a) a)" and builds (the Haskell value corresponding to) lam $ \ x -> x. (And it should use Text.Parsec or similar.)

I can build a parser that produces lambda terms with de-Bruijn indexing but what would it help?

Answer 1

As jozefg says, you can easily convert between operations. I'll show how to convert between a named, a de-Bruijn, and a PHOAS representation of lambda terms. It's relatively easy to fuse that into the parser if you absolutely want to, but it's probably better to parse a named representation first and then convert.

Let's assume

import Data.Map (Map)
import qualified Data.Map as M

and the following three representations of lambda terms:

String-based names

data LamN = VarN Name | AppN LamN LamN | AbsN Name LamN
  deriving (Eq, Show)

type Name = String

de-Bruijn indices

data LamB = VarB Int | AppB LamB LamB | AbsB LamB
  deriving (Eq, Show)

PHOAS

data LamP a = VarP a | AppP (LamP a) (LamP a) | AbsP (a -> LamP a)

Now the conversions between LamP and the others (in both directions). Note that these are partial functions. If you're applying them to lambda terms that contain free variables, you're responsible for passing a suitable environment.

How to go from LamN to LamP

Takes an environment mapping names to PHOAS variables. The environment can be empty for closed terms.

lamNtoP :: LamN -> Map Name a -> LamP a
lamNtoP (VarN n)     env = VarP (env M.! n)
lamNtoP (AppN e1 e2) env = AppP (lamNtoP e1 env) (lamNtoP e2 env)
lamNtoP (AbsN n e)   env = AbsP (\ x -> lamNtoP e (M.insert n x env))

How to go from LamB to LamP

Takes an environment that's a list of PHOAS variables. Can be the empty list for closed terms.

lamBtoP :: LamB -> [a] -> LamP a
lamBtoP (VarB n)     env = VarP (env !! n)
lamBtoP (AppB e1 e2) env = AppP (lamBtoP e1 env) (lamBtoP e2 env)
lamBtoP (AbsB e)     env = AbsP (\ x -> lamBtoP e (x : env))

How to get from 'LamP' to 'LamN'

Requires potential free variables to be instantiated to their names. Takes a supply of names for generating names of binders. Should be instantiated to an infinite list of mutually different names.

lamPtoN :: LamP Name -> [Name] -> LamN
lamPtoN (VarP n)         _sup  = VarN n
lamPtoN (AppP e1 e2)      sup  = AppN (lamPtoN e1 sup) (lamPtoN e2 sup)
lamPtoN (AbsP f)     (n : sup) = AbsN n (lamPtoN (f n) sup)

How to get from 'LamP' to 'LamB'

Requires potential free variables to be instantiated to numbers. Takes an offset that indicates the number of binders we're currently under. Should be instantiated to 0 for a closed term.

lamPtoB :: LamP Int -> Int -> LamB
lamPtoB (VarP n)     off = VarB (off - n)
lamPtoB (AppP e1 e2) off = AppB (lamPtoB e1 off) (lamPtoB e2 off)
lamPtoB (AbsP f)     off = AbsB (lamPtoB (f (off + 1)) (off + 1))

An example

-- \ x y -> x (\ z -> z x y) y

sample :: LamN
sample = AbsN "x" (AbsN "y"
  (VarN "x" `AppN` (AbsN "z" (VarN "z" `AppN` VarN "x" `AppN` VarN "y"))
            `AppN` (VarN "y")))

Going to de-Bruijn via PHOAS:

ghci> lamPtoB (lamNtoP sample M.empty) 0
AbsB (AbsB (AppB (AppB (VarB 1) (AbsB (AppB (AppB (VarB 0) (VarB 2)) (VarB 1)))) (VarB 0)))

Going back to names via PHOAS:

ghci> lamPtoN (lamNtoP sample M.empty) [ "x" ++ show n | n <- [1..] ]
AbsN "x1" (AbsN "x2" (AppN (AppN (VarN "x1") (AbsN "x3" (AppN (AppN (VarN "x3") (VarN "x1")) (VarN "x2")))) (VarN "x2")))