每种类型都有独特的变形吗? [英] Does each type have a unique catamorphism?
问题描述
最近，我终于开始觉得自己能理解变态.我在最近的答案中写了一些关于它们的内容，但我会简要地说一遍，在递归过程中对类型的抽象化遍历该类型的值，并对该类型具有的每个构造函数将该类型上的模式匹配化为一个函数.虽然我欢迎上面链接的我的回答中的这一点或更长版本的任何更正，但我认为我或多或少都对此有所保留，这不是这个问题的主题，只是一些背景.
Recently I've finally started to feel like I understand catamorphisms. I wrote some about them in a recent answer, but briefly I would say a catamorphism for a type abstracts over the process of recursively traversing a value of that type, with the pattern matches on that type reified into one function for each constructor the type has. While I would welcome any corrections on this point or on the longer version in the answer of mine linked above, I think I have this more or less down and that is not the subject of this question, just some background.
一旦我意识到传递给目录转换的函数完全对应于该类型的构造函数，并且这些函数的参数同样对应于那些构造函数的字段的类型，那一切突然变得很机械，我看不到在哪里有备用实现的余地.
Once I realized that the functions you pass to a catamorphism correspond exactly to the type's constructors, and the arguments of those functions likewise correspond to the types of those constructors' fields, it all suddenly feels quite mechanical and I don't see where there is any wiggle room for alternate implementations.
例如，我只是构成了这种愚蠢的类型，对其结构的含义"没有真正的概念，并为其衍生了一个同构词.我看不到其他任何可以定义这种类型的通用折叠的方法:
For example, I just made up this silly type, with no real concept of what its structure "means", and derived a catamorphism for it. I don't see any other way I could define a general-purpose fold over this type:
data X a b f = A Int b
| B
| C (f a) (X a b f)
| D a
xCata :: (Int -> b -> r)
-> r
-> (f a -> r -> r)
-> (a -> r)
-> X a b f
-> r
xCata a b c d v = case v of
A i x -> a i x
B -> b
C f x -> c f (xCata a b c d x)
D x -> d x
我的问题是，每种类型都具有独特的变形吗(取决于参数重新排序)?还是有反例:无法定义其同形异义的类型，或者存在两种截然不同但同等合理的同构异形的类型?如果没有反例(例如，一种类型的字形是唯一的并且微不足道可推导的)，那么是否有可能让GHC为我派生某种类型的类，从而自动完成这项工作?
My question is, does every type have a unique catamorphism (up to argument reordering)? Or are there counterexamples: types for which no catamorphism can be defined, or types for which two distinct but equally reasonable catamorphisms exist? If there are no counterexamples (i.e., the catamorphism for a type is unique and trivially derivable), is it possible to get GHC to derive some sort of typeclass for me that does this drudgework automatically?
推荐答案
与递归类型相关的分解过程可以通过机械方式得出.
The catamorphism associated to a recursive type can be derived mechanically.
假设您有一个递归定义的类型，有多个构造函数，每个构造函数都有自己的arity.我将借用OP的示例.
Suppose you have a recursively defined type, having multiple constructors, each one with its own arity. I'll borrow OP's example.
data X a b f = A Int b
| B
| C (f a) (X a b f)
| D a
然后，我们可以通过强制每个Arity为1来重写相同的类型，而不消耗所有内容.如果添加单位类型()，则Arity零(
Then, we can rewrite the same type by forcing each arity to be one, uncurrying everything. Arity zero (B) becomes one if we add a unit type ().
data X a b f = A (Int, b)
| B ()
| C (f a, X a b f)
| D a
然后，我们可以利用Either而不是多个构造函数，将构造函数的数量减少到一个.下面，为简便起见，我们只写中缀+而不是Either.
Then, we can reduce the number of constructors to one, exploiting Either instead of multiple constructors. Below, we just write infix + instead of Either for brevity.
data X a b f = X ((Int, b) + () + (f a, X a b f) + a)
在术语级别，我们知道我们可以重写任何递归定义
以x = f x where f w = ...的形式编写一个明确的不动点方程x = f x.在类型级别，我们可以使用相同的方法
反映递归类型.
At the term-level, we know we can rewrite any recursive definition
as the form x = f x where f w = ..., writing an explicit fixed point equation x = f x. At the type-level, we can use the same method
to refector recursive types.
data X a b f = X (F (X a b f)) -- fixed point equation
data F a b f w = F ((Int, b) + () + (f a, w) + a)
现在，我们注意到我们可以自导函子实例.
Now, we note that we can autoderive a functor instance.
deriving instance Functor (F a b f)
之所以可行，是因为在原始类型中，每个递归引用仅在 positive 位置出现.如果这不成立，使F a b f不能用作函子，那么我们就不可能具有变态.
This is possible because in the original type each recursive reference only occurred in positive position. If this does not hold, making F a b f not a functor, then we can't have a catamorphism.
最后，我们可以编写cata的类型，如下所示:
Finally, we can write the type of cata as follows:
cata :: (F a b f w -> w) -> X a b f -> w
这是OP的xCata类型吗?它是.我们只需要应用一些类型同构.我们使用以下代数定律:
Is this the OP's xCata type? It is. We only have to apply a few type isomorphisms. We use the following algebraic laws:
1) (a,b) -> c ~= a -> b -> c (currying)
2) (a+b) -> c ~= (a -> c, b -> c)
3) () -> c ~= c
顺便说一句，如果我们将(a,b)写为乘积a*b，将单元()写为1，而将a->b写为幂b^a，则很容易记住这些同构.实际上，它们变成了1) c^(a*b) = (c^a)^b , 2) c^(a+b) = c^a*c^b, 3) c^1 = c.
By the way, it's easy to remember these isomorphisms if we write (a,b) as a product a*b, unit () as1, and a->b as a power b^a. Indeed they become 1) c^(a*b) = (c^a)^b , 2) c^(a+b) = c^a*c^b, 3) c^1 = c.
无论如何，让我们开始仅重写F a b f w -> w部分
Anyway, let's start to rewrite the F a b f w -> w part, only
F a b f w -> w
=~ (def F)
((Int, b) + () + (f a, w) + a) -> w
=~ (2)
((Int, b) -> w, () -> w, (f a, w) -> w, a -> w)
=~ (3)
((Int, b) -> w, w, (f a, w) -> w, a -> w)
=~ (1)
(Int -> b -> w, w, f a -> w -> w, a -> w)
让我们现在考虑完整类型:
Let's consider the full type now:
cata :: (F a b f w -> w) -> X a b f -> w
~= (above)
(Int -> b -> w, w, f a -> w -> w, a -> w) -> X a b f -> w
~= (1)
(Int -> b -> w)
-> w
-> (f a -> w -> w)
-> (a -> w)
-> X a b f
-> w
确实是(重新命名w=r)通缉类型
Which is indeed (renaming w=r) the wanted type
xCata :: (Int -> b -> r)
-> r
-> (f a -> r -> r)
-> (a -> r)
-> X a b f
-> r
cata的标准"实现是
cata g = wrap . fmap (cata g) . unwrap
where unwrap (X y) = y
wrap y = X y
由于其通用性，需要花一些力气才能理解，但这确实是预期的.
It takes some effort to understand due to its generality, but this is indeed the intended one.
关于自动化:是的，这可以自动化，至少部分自动化.
hackage上有recursion-schemes软件包，它允许
一个写类似的东西
About automation: yes, this can be automatized, at least in part.
There is the package recursion-schemes on hackage which allows
one to write something like
type X a b f = Fix (F a f b)
data F a b f w = ... -- you can use the actual constructors here
deriving Functor
-- use cata here
示例:
import Data.Functor.Foldable hiding (Nil, Cons)
data ListF a k = NilF | ConsF a k deriving Functor
type List a = Fix (ListF a)
-- helper patterns, so that we can avoid to match the Fix
-- newtype constructor explicitly
pattern Nil = Fix NilF
pattern Cons a as = Fix (ConsF a as)
-- normal recursion
sumList1 :: Num a => List a -> a
sumList1 Nil = 0
sumList1 (Cons a as) = a + sumList1 as
-- with cata
sumList2 :: forall a. Num a => List a -> a
sumList2 = cata h
where
h :: ListF a a -> a
h NilF = 0
h (ConsF a s) = a + s
-- with LambdaCase
sumList3 :: Num a => List a -> a
sumList3 = cata $ \case
NilF -> 0
ConsF a s -> a + s
这篇关于每种类型都有独特的变形吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
