在Haskell中,双序列和双逆之间的关系是如何工作的?

fcg9iug3  于 2023-04-30  发布在  其他
关注(0)|答案(1)|浏览(116)

我在Haskell中“精神类型检查”bisequencebitraverse之间的关系时遇到了一些麻烦。以下是他们的签名,根据文件:

bisequence :: (Bitraversable t, Applicative f) => t (f a) (f b) -> f (t a b)
bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> t a b -> f (t c d)

同样根据文档,以下关系成立:

bisequence ≡ bitraverse id id

但这种关系对我来说没有意义:

  • id的签名是a -> a,那么它如何被接受为bitraverse的第一个或第二个参数,而bitraverse需要e。例如a -> f c
  • 即使我们克服了第一点,bitraverse id id的类型应该是Bitraversable t => t a b -> f (t c d),对吗?但这与bisequence的类型不同;它在输入中的ab上丢失了一个应用程序。

我错过了什么?我确信这两个误解是相关的,因为它们都是关于类型中缺少应用层。

aij0ehis

aij0ehis1#

让我们分解所有的变量。

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> t a b -> f (t c d)

现在我们有了id :: x -> x(我在这里使用了不同的变量名,这样我们就不会混淆使用相同的名称来表示两个不同的东西)。然后当我们写bitraverse id时,我们有id必须与bitraverse的第一个参数统一,所以

a -> f c ~ x -> x

~是统一关系)
因此,a ~ xf c ~ x。把它代入

bitraverse id :: Applicative f => (b -> f d) -> t (f c) b -> f (t c d)

冲洗并重复第二个id,我们称其具有类型签名id :: y -> y。我们要统一

b -> f d ~ y -> y

所以b ~ yf d ~ y,通过相同的逻辑。因此,

bitraverse id id :: Applicative f => t (f c) (f d) -> f (t c d)

也就是

bisequence :: Applicative f => t (f a) (f b) -> f (t a b)

换个名字
值得注意的是,当我们说bitraverse的参数是a -> f c时,我们从未说过a * 不 * 等于f ca实际上可以是任何值,在本例中,我们将其选择为等于f c(由id类型的统一强制要求)。

相关问题