haskell - 我如何获得 (sequence .) 的类型。 map ？

Question

我试图了解 Haskell 类型推断和类型系统是如何工作的。现在我正在研究(sequence .) . fmap的案例.我得到 (sequence .) 的类型和 (. fmap)就像haskell一样:

(.)      ::                             (b -> c) -> (a -> b) -> a -> c
fmap     :: Functor f                => (a -> b) -> f a -> f b
sequence :: (Traversable t, Monad m) => t (m a)  -> m (t a)

-- Type for . fmap:
a ~ (a -> b)
b ~ (f a -> f b)
. fmap              :: ((f a -> f b) -> c) -> ((a -> b) -> c)

-- Type for sequence:
b ~ t (m a1)
c ~ m (t a2)
sequence .          :: (a1 -> t (m a2)) -> (a1 -> m (t a2))

但是后来我无法获得 (sequence .) . fmap 的类型.我尝试了以下步骤，然后卡住了:

(sequence .) . fmap - ?

f a ~ a1
f b ~ t (m a2)
b ~ m a2
c ~ (a1 -> m (t a2))
(sequence .) . fmap :: (a -> m a2) -> (a1 -> m (t a2))

我得到的类型与 Haskell 给出的类型不同。

UPD 感谢@WillemVanOnsem，我取得了一些进展，但后来又卡住了……

(.)    ::              (b -> c) -> (a -> b) -> a -> c
(fmap) :: Functor f => (z -> u) -> f z -> f u
sequence .          :: (a1 -> t (m a2)) -> (a1 -> m (t a2))

b ~ (a1 -> t (m a2))
c ~ (a1 -> m (t a2))
a ~ (z -> u)
(sequence .) . fmap :: ((a1 -> t (m a2)) -> (a1 -> m (t a2))) ->
                       ((z -> u) -> (a1 -> t (m a2))) ->
                       ((z -> u) -> (a1 -> m (t a2))

Answer 1

让我们保持我们的类型变量都不同。

(.)      ::                             (b -> c) -> (a -> b) -> a -> c
fmap     :: Functor f                => (u -> v) -> f u -> f v
sequence :: (Traversable t, Monad m) => t (m x)  -> m (t x)

我们有两个函数 . 的用途.我会用 a1等第一个，和 a2和第二个类似。

在 (sequence .) , 我们有 (b1 -> c1) = (t (m x) -> m (t x)) , 所以 b1 = t (m x)和 c1 = m (t x) .使用替换， .专于 (t (m x) -> m (t x)) -> (a1 -> t (m x)) -> a1 -> m (t x) , 申请后 sequence ，我们有一个 (a1 -> t (m x)) -> a1 -> m (t x) 类型的术语.

现在我们可以看第二个 . , (sequence .) . fmap .在这里，我们有 (b2 -> c2) = (a1 -> t (m x)) -> a1 -> m (t x) , 和 (a2 -> b2) = (u -> v) -> f u -> f v .

这意味着:

b2 = a1 -> t (m x)
c2 = a1 -> m (t x)
a2 = (u -> v)
b2 = f u -> f v

请注意，我们有 b2在那里两次，这意味着 a1 = f u和 t (m x) = f v ，所以我们也可以推导出 f = t , v = m x .

现在我们知道了所有这些类型，我们知道第二个 .专门用于

((t u -> t (m x)) -> (t u -> m (t x)) 
  -> ((u -> m x) -> (t u -> t (m x))) 
  -> (u -> m x) 
  -> (t u -> m (t x))

但是我们已经应用了 .的参数，所以整个表达式的类型是 (u -> m x) -> (t u -> m (t x)) .

从那里开始，它只是变量重命名、约束和括号，远离 ghci 给我的东西。

> :t (sequence .) . fmap
(sequence .) . fmap
  :: (Monad m, Traversable t) => (a1 -> m a) -> t a1 -> m (t a)