不变函数的例子? [英] Example of Invariant Functor?
问题描述
我正在阅读关于monad图层包的文档我的大脑会沸腾起来。 在本文的 有没有 下面是一个标准地方,其中 我们很喜欢这种类型的结构,例如 这真的很悲惨,因为我们真正想要做的就是将这个 为了解决这个问题,你需要添加另一个类型参数,并将其称为参数HOAS 最后我们发现我们可以使用其中绑定是变量替换的 I'm reading documentation on monad layers package and my brain is going to boil up. In the Is there any example of an Here's a standard place where We'd love for this type to have structure like This is really tragic because what we would really like to do is to fold this To resolve this, you add another type parameter and call it Parametric HOAS And we end up finding that we can build a free monad atop this type using its 这篇关于不变函数的例子?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
mmtl
部分,作者会谈关于不变函子。它的方法 invmap
就像 Functor
的 fmap
,但它需要逆向态射也是(b - > a)
。我明白为什么作者说 hoist MFunctor
比 tmap $ c更强大$ c $> $ code>不变
,但是我没有看到逆向态射的点。
不变
的例子,它不能是 Functor
? Invariant
显示了更高阶的抽象语法(HOAS),用于嵌入lambda演算。在HOAS中,我们喜欢编写表达式类型,例如:
data ExpF a
= App a a
| Lam(a - > a)
- ((\ x。x)(\ x。x))有点像
ex :: ExpF(ExpF a)
ex = App(Lam id)(Lam id)
- 我们可以使用棘手的类型来使这个重复分层的ExpF更容易与
一起工作。 code> Functor
,但很遗憾因为 Lam
在正负两个位置都有 a
s,所以不能这样做。因此,我们定义
实例Invariant ExpF其中
invmap ab ba(App xy)= App(ab x)( ab a)
invmap ab ba(Lam aa)= Lam(ab。aa。ba)
ExpF
类型放入其中以形成一个递归表达式树。如果它是 Functor
,那很明显,但由于不是我们会得到一些非常难看且具有挑战性的结构。
data ExpF ba
= App aa
| Lam(b - > a)
派生函子
Functor
实例在此类型上创建一个免费monad。非常好!mmtl
section of this document the author talks about invariant functor. It's method invmap
is like fmap
of Functor
but it takes an inverse morphism (b -> a)
also. I understand why author says that hoist
of MFunctor
is more powerful than tmap
of Invariant
but i don't see what's the point of that inverse morphism.Invariant
which can't be an instance of Functor
?Invariant
shows up---higher order abstract syntax (HOAS) for embedding lambda calculus. In HOAS we like to write expression types likedata ExpF a
= App a a
| Lam (a -> a)
-- ((\x . x) (\x . x)) is sort of like
ex :: ExpF (ExpF a)
ex = App (Lam id) (Lam id)
-- we can use tricky types to make this repeat layering of `ExpF`s easier to work with
Functor
but sadly it cannot be since Lam
has a
s in both positive and negative position. So instead we define instance Invariant ExpF where
invmap ab ba (App x y) = App (ab x) (ab y)
invmap ab ba (Lam aa) = Lam (ab . aa . ba)
ExpF
type in on itself to form a recursive expression tree. If it were a Functor
that'd be obvious, but since it's not we get some very ugly, challenging constructions.data ExpF b a
= App a a
| Lam (b -> a)
deriving Functor
Functor
instance where binding is variable substitution. Very nice!