哈斯克尔有没有态射？

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有一篇可爱的论文,但我离题了.

同时,如果你确实想要在变量之外采取其他行动,那么一种通用方法是使用通用遍历工具包,例如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)对一些合适的单子m(例如,线程的变量的环境中),而不仅仅是Term x本身.处理每个子项以给出a 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.通过明确关于一个层包含的类型,我们可以逐层挖掘工作的一般模式.

Answer 2

看看uniplate包.它可以做你正在谈论的那种转换,但是对于任意数据结构.