Haskell 中有态射吗？

Question

我有一些 GADT，它代表 lambda 演算中的一个术语。

data Term a = 
      Var a
    | Lambda a (Term a)
    | Apply (Term a) (Term a)

我想做的是有一个用于该类型转换的通用接口。它应该具有与此类似的类型签名：

(Term a -> Term a) -> Term a -> Term a

编写这个函数很容易：

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f (Var v) = f (Var v)
fmap' f (Lambda v t) = Lambda v (fmap' f t)
fmap' f (Apply t1 t2) = Apply (fmap' f t1) (fmap' f t2)

所以，我的问题是 haskell （或 haskell 库）中有某种通用结构来进行这种转换（类似于 Functor >，它可能应该称为态射）？

Answer 1

作为参考，这里是术语...

data Term a = 
      Var a
    | Lambda a (Term a)
    | Apply (Term a) (Term a)

（我注意到变量的表示是抽象的，这通常是一个很好的计划。）

...这是建议的函数。

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f (Var v) = f (Var v)
fmap' f (Lambda v t) = Lambda v (fmap' f t)
fmap' f (Apply t1 t2) = Apply (fmap' f t1) (fmap' f t2)

这个定义让我困扰的是 f 只适用于 (Var v) 形式的术语，所以你不妨实现替换 。

subst :: (a → Term a) → Term a → Term a 
subst f (Var v) = f v
subst f (Lambda v t) = Lambda v (subst f t)
subst f (Apply t1 t2) = Apply (subst f t1) (subst f t2)

如果您稍微注意区分绑定变量和自由变量，您就可以将 Term 设为 Monad，并通过替换实现 (>>=)。一般来说，术语可以具有用于重命名的Functor结构和用于替换的Monad结构。 Bird 和 Paterson 有一篇可爱的论文那个，但我离题了。

同时，如果您确实想要执行除 at 变量之外的操作，一种通用方法是使用通用遍历工具包，如 uniplate，如 augustss 建议的那样。另一种可能，也许稍微更有纪律，是根据您的类型使用“折叠”。

tmFold :: (x -> y) -> (x -> y -> y) -> (y -> y -> y) -> Term x -> y
tmFold v l a (Var x)       = v x
tmFold v l a (Lambda x t)  = l x (tmFold v l a t)
tmFold v l a (Apply t t')  = a (tmFold v l a t) (tmFold v l a t')

在这里，v、l 和 a 为您的Term定义了一个替代代数 -形成操作，仅作用于y，而不是Term x，解释如何处理变量、lambda 和应用程序。对于某些合适的单子m（例如，为变量线程化环境），您可以选择y为m（Term x），而不是只是Term x本身。每个子项都经过处理以给出 y，然后选择适当的函数来生成整个项的 y。折叠捕获标准递归模式。

普通的一阶数据类型（以及一些表现良好的高阶数据类型）都可以配备折叠运算符。以牺牲可读性为代价，您甚至可以一劳永逸地编写折叠运算符。

data Fix f = In (f (Fix f))

fixFold :: Functor f => (f y -> y) -> Fix f -> y
fixFold g (In xf) = g (fmap (fixFold g) xf)

data TermF a t
  = VarF a
  | LambdaF a t
  | ApplyF t t

type Term a = Fix (TermF a)

与递归 Term a 不同，此 TermF a t 解释了如何使用 t 元素创建术语的一层在地下的地方。我们通过使用递归 Fix 类型取回递归 Term 结构。我们在外观上损失了一点，因为每一层都有一个额外的 In 来包裹它。我们可以定义

var x      = In (VarF x)
lambda x t = In (LambdaF x t)
apply t t' = In (Apply x t t')

，但不能在模式匹配中使用这些定义。不过，回报是我们可以使用通用的 fixFold 而无需额外费用。要根据项计算 y，我们只需要给出一个类型为的函数

TermF a y -> y

（就像 v、l 和 a上面的）解释了如何处理其子项已被处理为 y 类型值的任何项。通过明确一层的类型，我们可以利用逐层工作的一般模式。

Answer 2

查看uniplate 包。它可以进行您正在讨论的那种转换，但适用于任意数据结构。

Answer 3

使用问题中引用的 fmap' ，转换函数 f 只能将 Var 值转换为不同的 lambda 表达式。它无法将 Lambda 或 Apply 转换为其他内容，因为它是在 fmap' 函数中硬编码的，这些构造函数保持不变。

例如，您的 fmap' 可以将 Var 1 转换为 Lambda 1 (Var 1)，但反之则不然。
这真的是你的意图吗？

如果 fmap' 允许任意转换，您最终会得到以下结果：

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f t = f t

这与 $ 相同。

（另一方面，如果只允许 fmap' 更改表达式中的值，而根本不更改其结构，那么您将回到通常的 fmap.)

Answer 4

首先，我没有你的实际问题的答案，尽管我确实有一些可能对你有用的想法，但不确定。

在我看来，这并不那么普遍，我希望您使用类似的东西：

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f (Var v) = f $ Var v
fmap' f (Lambda v t) = f $ Lambda v (fmap' f t)
fmap' f (Apply t1 t2) = f $ Apply (fmap' f t1) (fmap' f t2)

它仍然允许您使用相同的功能，您只需在 f 本身内进行模式匹配。我认为这个函数可以用于诸如计算 lambda 演算之类的事情（不过，您需要随身携带一些状态）。

将来对您可能更有用的东西可能是：

fmapM :: Monad m => (Term a -> m (Term a)) -> Term a -> m (Term a)
fmapM f (Var v)         = f (Var v)
fmapM f (Lambda v t)    = do
    t' <-fmapM f t
    f (Lambda v t')
fmapM f (Apply t1 t2)   = do
    t1' <- fmapM f t1
    t2' <- fmapM f t2
    f (Apply t1' t2')

您可以稍后将其与 State monad 一起使用来跟踪 lambda 的绑定。此外，当您使用 Identity monad 时，此函数与上面的函数相同，您可以编写一个简单的函数，采用 f :: (Term a -> Term a) 并使用 fmap' f = fmapM (f.(return :: ->身份a))。

让我知道这是否有帮助:)

Answer 5

您可能会发现 unbound 包很有用，尤其是 substs 函数。