Разбор для выражений PHOAS

Ответ 1

Как говорит jozefg, вы можете легко конвертировать между операциями. Я покажу, как конвертировать между именем, де-Бройном и PHOAS-представлением лямбда-терминов. Сравнительно легко вставить это в синтаксический анализатор, если вы этого абсолютно хотите, но, вероятно, лучше сначала проанализировать именованное представление, а затем преобразовать.

Предположим, что

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

и следующие три представления лямбда-членов:

String основанные имена

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

type Name = String

индексы de-Bruijn

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)

Теперь переходы между LamP и другими (в обоих направлениях). Обратите внимание, что это частичные функции. Если вы применяете их к лямбда-терминам, которые содержат свободные переменные, вы несете ответственность за передачу подходящей среды.

Как перейти от LamN до LamP

Принимает имена сопоставления окружения для PHOAS. Окружение может быть пустым для закрытых условий.

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))

Как перейти от LamB в LamP

Принимает среду, в которой содержится список PHOAS. Может быть пустым списком для закрытых терминов.

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))

Как добраться от "LamP" до "LamN"

Требуется, чтобы потенциальные свободные переменные быть инстанцированными к их именам. Получает запас имен для генерации имена связующих. Должен быть создан в бесконечном списке взаимно разные имена.

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)

Как добраться из "LamP" в "LamB"

Требуется, чтобы потенциальные свободные переменные быть экземпляром чисел. Принимает смещение, которое указывает количество которые мы сейчас находимся. Должен быть создан для 0 для закрытого Термин.

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))

Пример

-- \ 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")))

Переход на де-Бройн через 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)))

Возврат к именам через 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")))

Ответ 2

jozefg имеет правильный ответ в своем комментарии. Всегда анализируйте простое абстрактное синтаксическое дерево, а не какое-то умное представление. Затем, после разбора, преобразуйте представления. В этом случае легко

data Named = NLam String Named | NVar String | NApp Named Named

convert :: (String -> a) -> Named -> Exp a a
convert f (NVar n) = var $ f n
convert f (NApp e1 e2) = app (convert f e1) (convert f e2)
convert f (NLam s e) = lam $ \a -> convert (nf a) e where
  nf a s' = if s' == s then a else f s'

вы могли бы использовать в качестве своей карты что-то отличное от функции String -> a. Data.Map, например, избавится от линейного поиска времени.

Одна хорошая вещь о PHOAS над другими схемами HOAS заключается в том, что вы можете легко "конвертировать назад"

addNames :: ExpF Int (State Int Named) -> State Int Named
addNames (App a b) = liftM2 NApp a b
addNames (Lam f)   = do
  i <- get
  put (i + 1)
  r <- f i
  return $ NLam ('x':show i) r

convert' :: Exp Int Int -> Named
convert' = fst 
  . flip runState 0
  . cata addNames 
  . liftM (return . NVar . ('x':) . show)

который даже работает как ожидалось

λ: convert' $ convert undefined $ NLam "x" $ NApp (NVar "x") (NLam "y" (NVar "y"))
> NLam "x0" (NApp (NVar "x0") (NLam "x1" (NVar "x1")))

Ответ 3

Я снова буду работать с темой других ответов здесь и предлагаю вам разобрать, как будто вы просто создаете наивное представление с именованными переменными. Если вы хотите избежать промежуточного представления, вы можете вставить его в парсер, не затрудняя понимание:

data Lam a = Var a | Lam a `App` Lam a | Lam (a -> Lam a)

type MkLam a = (String -> a) -> Lam a

var :: String -> MkLam a
var x = Var . ($ x)

app :: MkLam a -> MkLam a -> MkLam a
app = liftA2 App

lam :: String -> MkLam a -> MkLam a
lam v e env = Lam $ \x -> e $ \v' -> if v == v' then x else env v'

Идея состоит в том, что вместо использования конструкторов вашего промежуточного представления в вашем парсере вы используете эти функции напрямую. Они имеют те же типы, что и конструкторы, поэтому это действительно просто замена. Это также немного короче, так как теперь нам не нужно отдельно выписывать ADT и интерпретатор.