haskell - shampoo - análisis de expresiones PHOAS

haskell shampoo

Question

Creo que entiendo PHOAS (sintaxis abstracta paramétrica de orden superior), y veo cómo podemos imprimir una expresión (cf. http://www.reddit.com/r/haskell/comments/1mo59h/phoas_for_free_by_edward_kmett/ccbxzoo ) .

Pero, no veo cómo crear un analizador para tales expresiones, por ejemplo, esto toma "(lambda (a) a)" y genera (el valor de Haskell correspondiente a) lam $ / x -> x . (Y debe usar Text.Parsec o similar.)

Puedo crear un analizador que genere términos lambda con la indexación de-Bruijn, pero ¿qué ayudaría?

Answer 1

Como dice jozefg, puedes convertir fácilmente entre operaciones. Mostraré cómo convertir entre un nombre, un de-Bruijn y una representación de PHOAS de los términos lambda. Es relativamente fácil fusionar eso en el analizador si es absolutamente necesario, pero probablemente es mejor analizar primero una representación nombrada y luego convertirla.

Asumamos

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

y las siguientes tres representaciones de términos lambda:

Nombres basados ​​en String

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

type Name = String

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

Ahora las conversiones entre LamP y los demás (en ambas direcciones). Tenga en cuenta que estas son funciones parciales. Si los está aplicando a los términos lambda que contienen variables libres, es responsable de pasar un entorno adecuado.

Cómo ir de LamN a LamP

Toma un entorno asignando nombres a las variables de PHOAS. El entorno puede estar vacío para términos cerrados.

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

Cómo ir de LamB a LamP

Toma un entorno que es una lista de variables de PHOAS. Puede ser la lista vacía para términos cerrados.

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

Cómo llegar de ''LamP'' a ''LamN''

Requiere que las variables libres potenciales sean instanciadas a sus nombres. Toma un suministro de nombres para generar nombres de carpetas. Debe ser instanciado a una lista infinita de nombres mutuamente diferentes.

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)

Cómo llegar de ''LamP'' a ''LamB''

Requiere que las variables libres potenciales sean instanciadas a números. Toma un desplazamiento que indica el número de carpetas en las que estamos actualmente. Se debe crear una instancia a 0 para un término cerrado.

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

Un ejemplo

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

Ir a de-Bruijn a través de 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)))

Volviendo a los nombres a través de 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")))

Answer 2

Volveré a ejecutar el tema de las otras respuestas aquí y sugeriré que analice como si solo estuviera creando la representación ingenua con variables nombradas. Si desea evitar la representación intermedia, puede integrarla en el analizador sin que sea más difícil de entender:

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

La idea es que en lugar de usar los constructores de su representación intermedia en su analizador, use estas funciones directamente. Tienen los mismos tipos que tendrían los constructores, por lo que en realidad es solo un reemplazo directo. También es un poco más corto, ya que ahora no tenemos que escribir por separado el ADT y el intérprete.

Answer 3

jozefg tiene la respuesta correcta en su comentario. Siempre analice un simple árbol de sintaxis abstracta, no una representación inteligente. Luego, después de analizar, convertir representaciones. En este caso, es fácil.

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

por supuesto, podría usar otra función que no sea una función String -> a como su mapa. Data.Map por ejemplo, eliminaría las búsquedas de tiempo lineales.

Una cosa interesante acerca de PHOAS sobre otros esquemas HOAS es que puede "volver a convertir" fácilmente.

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)

que incluso funciona como se espera

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