haskell 如何安全地将命名语法转换为PHOAS？

这个问题本质上与parsing for PHOAS expressions相同，但是我特别寻找一个使用Maybe类型安全处理范围外变量的答案（因此不使用Haskell的错误机制）。
具体来说，我有这些类型：

type Name = Int

data Lam = Var Name | Lam Name Lam | App Lam Lam 

data LamP p = VarP p | LamP (p -> LamP p) | AppP (LamP p) (LamP p)

为了简单起见，我使用整数作为名称。
从LamP到Lam的转换非常简单：

fromP :: (forall p. LamP p) -> Lam
fromP x0 = go 0 x0 where
  go _ (VarP n) = Var n
  go n (LamP f) = Lam n (go (n + 1) (f n))
  go n (AppP x y) = App (go n x) (go n y)

下面是我的另一个尝试：

type Env p = Int -> Maybe p

emptyEnv :: Env p
emptyEnv = const Nothing

lookupEnv :: Env p -> Int -> Maybe p
lookupEnv = id

insertEnv :: Env p -> Int -> p -> Env p
insertEnv f n x m
  | n == m = Just x
  | otherwise = f m

toP :: Lam -> Maybe (LamP p)
toP x0 = go x0 emptyEnv where
  go :: Lam -> Env p -> Maybe (LamP p)
  go (Var n)   env = VarP <$> lookupEnv env n
  go (Lam n x) env =
    go x (insertEnv env n _) >>= \x' -> pure (LamP (\p -> _) -- <<< problem!
  go (App x y) env = AppP <$> go x env <*> go y env

似乎不可能将p从LamP内部移动到其左侧的insertEnv。
然而，我坚信go计算的Just/Nothing结果不应该取决于我们在环境中插入了哪个p，所以我想放一个占位符，然后再填充它，但是我不知道该怎么做。
还是无法编写此函数？

这里有一个（部分不完整的）解决方案。
其思想是将GADT作为中间表示进行传递。
在FOAS中，我们使用De Bruijn指数和Peano自然数来表示变量。

data Nat = O | S Nat

data Lam = Var Nat | Lam Lam | App Lam Lam

现在我们用GADT来表示一个自由变量在[0,n)中的项，这些项有一个特殊的WeakC语法来进行显式弱化，这样我们就可以考虑一个自由变量在[0,n)中的项，就像在[0,n+1)中一样。

-- Lam with free vars in [0,n)
data LamC (n :: Nat) where
   -- weakening: [0,n) is included in [0,n+1)
   WeakC :: LamC n -> LamC ('S n)
   -- the "last-bound" variable
   VarC :: LamC ('S n)
   LamC :: LamC ('S n) -> LamC n
   AppC :: LamC n -> LamC n -> LamC n

-- Example: (\x -> x (\y -> y x))
test :: LamC 'O
test = LamC (AppC (VarC {- x -})
            (LamC (AppC (VarC {- y -}) (WeakC VarC {- x -}))))

注意VarC是如何“被最后一个lambda绑定的变量”的，即De Bruijn索引为零的变量。如果我们想访问其他变量，我们需要使用WeakC。
还要注意，应用程序如何方便地要求两边都有相同的n--这并没有失去推广性，因为我们有弱化，我们可以根据需要使这些索引为相同的n。
现在，将 closedLam项转换为LamC 'O看起来是可行的。我跳过了这一部分，将其作为练习。这可能需要使用一些Nat单例和存在体，因为这需要推广到... -> Maybe (exists n . (SNat n, LamC n))以使其归纳。看起来需要在应用程序中执行弱化操作。不过，您应该能够实际编写此代码。

-- Check if the term is closed, and in that case convert it
-- to LamC 'O. Return Nothing if the term is not closed.
lamToLamC :: Lam -> Maybe (LamC 'O)
lamToLamC _ = error "TODO"

最后，PHOAS术语：

data LamP p
   = VarP p
   | LamP (p -> LamP p)
   | AppP (LamP p) (LamP p)

环境现在是一个GADT，提供n变量的值。

data Env (n :: Nat) p where
   Enil  :: Env 'O p
   Econs :: p -> Env n p -> Env ('S n) p

现在我们可以把LamC项转换成LamP，只要我们有一个合适的环境，这样就可以很好地递归。

lamCToLamP :: Env n p -> LamC n -> LamP p
lamCToLamP (Econs _ rho ) (WeakC e)    =
   lamCToLamP rho e
lamCToLamP (Econs p _   ) VarC         =
   VarP p
lamCToLamP rho            (LamC e)     =
   LamP (\p -> lamCToLamP (Econs p rho) e)
lamCToLamP rho            (AppC e1 e2) =
   AppP (lamCToLamP rho e1) (lamCToLamP rho e2)

请注意，这里我们不必返回Maybe (LamP p))，这就避免了您在使用Nothing时发现的问题。这里，我们确信环境提供了p，而不是Maybe p，因此一切都是完整的（由于我们的GADT），我们不再需要担心。
最后，我们把碎片粘在一起。

lamToLamP :: Lam -> Maybe (LamP p)
lamToLamP l = lamCToLamP Enil <$> lamToLamC l

haskell 如何安全地将命名语法转换为PHOAS？

1条答案

相关问题

热门标签

最新问答