在 recursion-schemes
包定义了以下类型:
newtype Fix f = Fix (f (Fix f))
newtype Mu f = Mu (forall a. (f a -> a) -> a)
它们是同构的吗?如果是,你如何证明?
最佳答案
Are they isomorphic?
是的,它们在 Haskell 中是同构的。见 What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package一些补充说明。
If so, how do you prove it?
让我们从定义执行转换的函数开始:
muToFix :: Mu f -> Fix f
muToFix (Mu s) = s Fix
fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)
为了证明这些函数见证了同构,我们必须证明:
muToFix . fixToMu = id
fixToMu . muToFix = id
来自
Fix
然后回来同构的一个方向比另一个更直接:
muToFix (fixToMu t) = t
muToFix (fixToMu t) -- LHS
muToFix (Mu (\f -> cata f t))
(\f -> cata f t) Fix
cata Fix t -- See below.
t -- LHS = RHS
上面的最后一段,
cata Fix t = t
,可以通过cata
的定义来验证:cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix
cata Fix t
,那么,是 Fix (fmap (cata Fix) (unfix t))
.我们可以用归纳法证明它一定是t
,至少对于有限 t
(无限结构会变得更加微妙 - 请参阅本答案末尾的附录)。有两种可能需要考虑:unfix t :: f (Fix f)
是空的,没有可挖掘的递归位置。在这种情况下,它必须等于 fmap absurd z
一些 z :: f Void
, 因此:cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (fmap (cata Fix) (fmap absurd z))
Fix (fmap (cata Fix . absurd) z)
-- fmap doesn't do anything on an empty structure.
Fix (fmap absurd z)
Fix (unfix t)
t
unfix t
不是空的。那样的话,我们至少知道fmap (cata Fix)
除了申请之外什么也做不了cata Fix
在递归位置上。这里的归纳假设是,这样做将使这些位置保持不变。然后我们有:cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (unfix t) -- Induction hypothesis.
t
(最终,
cata Fix = id
是 Fix :: f (Fix f) -> Fix x
是初始 F 代数的推论。直接诉诸这个事实在这个证明的上下文中,可能是太多的捷径。)
来自
Mu
然后回来给定
muToFix . fixToMu = id
,证明fixToMu . muToFix = id
足以证明:muToFix
是单射的,或 fixToMu
是满射的。 让我们采用第二个选项,并查看相关定义:
newtype Mu f = Mu (forall a. (f a -> a) -> a)
fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)
fixToMu
那么,作为满射,意味着,给定任何特定的 Functor
f
, 类型 forall a. (f a -> a) -> a
的所有函数可以定义为 \alg -> cata alg t
,对于某些特定的 t :: Fix f
.然后,任务变成对 forall a. (f a -> a) -> a
进行编目。函数,看看是否所有的函数都可以用那种形式表达。我们如何定义
forall a. (f a -> a) -> a
功能不依赖 fixToMu
?无论如何,它必须涉及使用f a -> a
代数作为参数提供以获得 a
结果。直接的途径是将它应用到一些 f a
值(value)。一个主要的警告是,因为 a
是多态的,我们必须能够变出说f a
任何选择的值(value) a
.只要f
,这是一个可行的策略- 值恰好存在。在这种情况下,我们可以这样做:fromEmpty :: Functor f => f Void -> forall a. (f a -> a) -> a
fromEmpty z = \alg -> alg (fmap absurd z)
为了使符号更清晰,让我们为可以用来定义
forall a. (f a -> a) -> a
的事物定义一个类型。职能:data Moo f = Empty (f Void)
fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Empty z) = \alg -> alg (fmap absurd z)
除了直接路线,还有另一种可能性。鉴于
f
是 Functor
,如果我们有一个 f (Moo f)
我们可以两次应用代数,第一次应用在外 f
下层,通过 fmap
和 fromMoo
:fromLayered :: Functor f => f (Moo f) -> forall a. (f a -> a) -> a
fromLayered u = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
考虑到我们也可以制作
forall a. (f a -> a) -> a
出f (Moo f)
值,将它们添加为 Moo
的情况是有意义的。 :data Moo f = Empty (f Void) | Layered (f (Moo f))
因此,
fromLayered
可以合并到 fromMoo
:fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo = \case
Empty z -> \alg -> alg (fmap absurd z)
Layered u -> \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
请注意,通过这样做,我们偷偷地从应用
alg
转移了。下一个f
递归应用层 alg
下任意数量f
层。接下来,我们可以注意到
f Void
值可以注入(inject)Layered
构造函数:emptyLayered :: Functor f => f Void -> Moo f
emptyLayered z = Layered (fmap absurd z)
这意味着我们实际上并不需要
Empty
构造函数:newtype Moo f = Moo (f (Moo f))
unMoo :: Moo f -> f (Moo f)
unMoo (Moo u) = u
Empty
呢?案例在 fromMoo
?两种情况的唯一区别在于,在Empty
案例,我们有 absurd
而不是 \moo -> fromMoo moo alg
.自所有 Void -> a
功能是 absurd
,我们不需要单独的 Empty
如果有:fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Moo u) = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)
一个可能的外观调整是翻转
fromMoo
参数,因此我们不需要将参数写入 fmap
作为一个 lambda:foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg (Moo u) = alg (fmap (foldMoo alg) u)
或者,更无意义:
foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg = alg . fmap (foldMoo alg) . unMoo
在这一点上,再看一下我们的定义表明一些重命名是有序的:
newtype Fix f = Fix (f (Fix f))
unfix :: Fix f -> f (Fix f)
unfix (Fix u) = u
cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix
fromFix :: Functor f => Fix f -> forall a. (f a -> a) -> a
fromFix t = \alg -> cata alg t
它是:所有
forall a. (f a -> a) -> a
函数的形式为 \alg -> cata alg t
一些 t :: Fix f
.因此,fixToMu
是满射的,我们有所需的同构。附录
在评论中,对
cata Fix t = t
中归纳论证的适用性提出了一个密切相关的问题。推导。至少,仿函数定律和参数性确保 fmap (cata Fix)
不会产生额外的工作(例如,它不会扩大结构,或引入额外的递归位置来挖掘),这证明了为什么在推导的归纳步骤中进入递归位置是最重要的。既然如此,如果 t
是一个有限结构,空f (Fix t)
的基本情况最终会到达,一切都清楚了。如果我们允许 t
然而,要成为无限,我们可以继续无休止地下降,fmap
之后 fmap
之后 fmap
,从未达到基本情况。然而,无限结构的情况并不像最初看起来那么糟糕。惰性首先使无限结构可行,它允许我们懒惰地消耗无限结构:
GHCi> :info ListF
data ListF a b = Nil | Cons a b
-- etc.
GHCi> ones = Fix (Cons 1 ones)
GHCi> (\(Fix (Cons a _)) -> a) (cata Fix ones)
1
GHCi> (\(Fix (Cons _ (Fix (Cons a _)))) -> a) (cata Fix ones)
1
虽然递归位置的连续性无限延伸,但我们可以在任何点停止并从周围的
ListF
中获得有用的结果。功能上下文。需要重申的是,此类上下文不受 fmap
的影响。 ,因此我们可能消耗的结构的任何有限段都不会受到 cata Fix
的影响。 .这种懒惰的缓刑反射(reflect)了,正如在本讨论的其他地方提到的,懒惰如何破坏不动点之间的区别
Mu
, Fix
和 Nu
.不偷懒,Fix
不足以编码高效的核心递归,因此我们必须切换到 Nu
,最大不动点。这是差异的一个小示范:GHCi> :set -XBangPatterns
GHCi> -- Like ListF, but strict in the recursive position.
GHCi> data SListF a b = SNil | SCons a !b deriving Functor
GHCi> ones = Nu (\() -> SCons 1 ()) ()
GHCi> (\(Nu c a) -> (\(SCons a _) -> a) (c a)) ones
1
GHCi> ones' = Fix (SCons 1 ones')
GHCi> (\(Fix (SCons a _)) -> a) ones'
^CInterrupted.
关于haskell - Fix 和 Mu 同构,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/61083423/