haskell - Haskell中有态射吗？

Question

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

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

我想要做的是对该类型进行转换的通用接口(interface)。它应该具有类似于以下的类型签名:

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

如果您稍微注意区分绑定(bind)变量和自由变量，您将能够制作 Term一个 Monad实现替换 (>>=) .通常，术语可以有 Functor重命名结构和 Monad替代结构。 Bird and Paterson 有一篇可爱的论文关于那个，但我离题了。

同时，如果您确实想在变量以外的地方采取行动，一种通用的方法是使用通用遍历工具包，如 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 和应用程序。您可以选择y成为 m (Term x)对于一些合适的单子(monad)m (例如，为变量线程化环境)，而不仅仅是 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 解释如何制作一层术语子项中的元素。我们得到递归 Term使用递归 Fix 的结构类型。我们在外观上有所损失，因为每一层都有一个额外的 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 类型值的任何术语.通过明确说明一层由什么组成的类型，我们可以利用逐层工作的一般模式。