供参考,以下是相关术语...
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,您可以在这里查看:
Bird and Paterson,但我偏离主题了。
同时,如果你确实想要对变量以外的东西进行操作,一种常见的方法是使用像uniplate这样的通用遍历工具包,就像augustss建议的那样。另一个可能,也许稍微更加纪律严明的方法,是使用您类型的‘fold’。
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)
),而不仅仅是
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解释了如何制作一个术语的一层,其中子术语位置有个元素。我们通过使用递归
Fix类型来获得递归
Term结构。在美学上我们会失去一点,因为每一层都有一个额外的包装它。我们可以定义:
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
类型值的术语。通过在类型上明确表达每一层包含什么,我们可以利用逐层工作的通用模式。
class Morphism m where fmap' :: (m a → m a) → m a → m a
这样的类型类(但可能有不同的名称)? - stakx - no longer contributingfmap'
的目的是什么... 给定签名的最简单实现不就是id
吗? - Matthias Benkardid
只接受一个参数,而fmap'
是一个二元操作。重要的一点似乎是fmap'
仅对一个类型的值进行操作并返回;这就是它与例如($)
的区别所在。 - stakx - no longer contributingfmap'
和其他Haskell函数一样是一元的。(m a → m a) → m a → m a
与(m a → m a) → (m a → m a)
相同,后者是id
类型的一个实例。 - Matthias Benkardid
并不是该签名下唯一合理的函数。 - stakx - no longer contributing