不变函数的例子？ [英] Example of Invariant Functor?

问题描述

我正在阅读关于monad图层包的文档我的大脑会沸腾起来。

在本文的 mmtl 部分，作者会谈关于不变函子。它的方法 invmap 就像 Functor 的 fmap ，但它需要逆向态射也是（b - > a）。我明白为什么作者说 hoist MFunctor 比 tmap $ 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 ，那很明显，但由于不是我们会得到一些非常难看且具有挑战性的结构。

为了解决这个问题，你需要添加另一个类型参数，并将其称为参数HOAS

  data ExpF ba 
 = App aa 
 | Lam（b  - > a）
派生函子
  

最后我们发现我们可以使用其中绑定是变量替换的 Functor 实例在此类型上创建一个免费monad。非常好！

I'm reading documentation on monad layers package and my brain is going to boil up.

In the 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.

Is there any example of an Invariant which can't be an instance of Functor?

解决方案

Here's a standard place where Invariant shows up---higher order abstract syntax (HOAS) for embedding lambda calculus. In HOAS we like to write expression types like

data 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

We'd love for this type to have structure like Functor but sadly it cannot be since Lam has as 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)

This is really tragic because what we would really like to do is to fold this 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.

To resolve this, you add another type parameter and call it Parametric HOAS

data ExpF b a
  = App a a
  | Lam (b -> a)
  deriving Functor

And we end up finding that we can build a free monad atop this type using its Functor instance where binding is variable substitution. Very nice!

这篇关于不变函数的例子？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！