haskell - 将函数引入范围会使代码无法编译

Question

考虑以下片段

-- This compiles
import Control.Monad

v :: Monad m => m b
v = undefined

w :: Monad m => m c
w = undefined

h :: Monad m => a -> m c
h = v' >=> w'
 where v' :: Monad m1 => a -> m1 b
       v' = const v
       w' :: Monad m2 => b -> m2 c
       w' = const w

它编译得很好并且能够解决 m ~ m1 ~ m2，但是如果我们将 v 和 w 带入 h 作用域，那么它将不再编译:Couldn't match type `m1' with `m'

-- This doesn't compiles but looks equivalent to h

h' :: Monad m => m b -> m c -> a -> m c
h' v w = v' >=> w'
  where v' :: Monad m1 => a -> m1 b
        v' = const v
        w' :: Monad m2 => b -> m2 c
        w' = const w

我认为 h 和 h' 在类型解析起作用时是等价的，因为 h 和 都不是h' 对 m 的假设。但事实证明，h'需要借助ScopedTypeVariables来指定m ~ m1 ~ m2

GHC 没有在 h 中提示，而是在 h' 中提示，我觉得很奇怪。为什么编译h'需要ScopedTypeVariables，编译h却不需要？

备案

以防万一你想知道这是编译的 h' 版本。但请注意问题是为什么ScopedTypeVariables 不需要编译h？ 而不是为什么ScopedTypeVariables 是需要编译 h'?

{-# LANGUAGE ScopedTypeVariables #-}
h' :: forall m a b c. Monad m => m b -> m c -> a -> m c
h' v w = v' >=> w'
  where v' :: Monad m => a -> m b
        v' = const v
        w' :: Monad m => b -> m c
        w' = const w

Answer 1

{-# LANGUAGE ScopedTypeVariables, TypeFamilies, RankNTypes, UnicodeSyntax #-}

请记住，带有类型变量(不是来自封闭范围)的签名是隐式普遍量化的。 IE。你的第一个例子是

v :: ∀ m b . Monad m => m b
v = undefined

w :: ∀ m c . Monad m => m c
w = undefined

h :: ∀ m a c . Monad m => a -> m c
h = v' >=> w'
 where v' :: ∀ m₁ b . Monad m₁ => a -> m₁ b
       v' = const v
       w' :: ∀ m₂ b c . Monad m₂ => b -> m₂ c
       w' = const w

让我们在这里做一些 α 重命名，使它们全部匹配，您可以随时使用通用量化绑定(bind)来完成:(编译器在上面的示例中在后台执行此操作)

v :: ∀ m₁ b . Monad m₁ => m₁ b
v = undefined

w :: ∀ m₂ c . Monad m₂ => m₂ c
w = undefined

h :: ∀ m a ζ . Monad m => a -> m ζ
h = v' >=> w'
 where v' :: ∀ m₁ b . Monad m₁ => a -> m₁ b
       v' = const v
       w' :: ∀ m₂ b c . Monad m₂ => b -> m₂ c
       w' = const w

但是，在您的第二个示例中，v 和 w 的类型未被普遍量化。相反，他们从 h' 的签名中得到了严格的 m。因此，您不能在 普遍量化的局部定义中使用它们。您必须将其限制为等于外部 m，但这首先会破坏量化点。

h' :: ∀ m a b c . Monad m => m b -> m c -> a -> m c
h' v w = v' >=> w'
  where v' :: ∀ m₁ . (Monad m₁, m₁~m) => a -> m₁ b
        v' = const v
        w' :: ∀ m₂ . (Monad m₂, m₂~m) => b -> m₂ c
        w' = const w

(这里，Monad m₁/Monad m₂ 约束是多余的，因为我们已经知道那个地方的 Monad m。)

你想要的是 v 和 w 被普遍量化，就像它们在第一个例子中一样。这使得 h' 的类型成为 rank-2 类型:

h' :: ∀ m a b c . Monad m
       => (∀ m₁ . Monad m₁ => m₁ b) -> (∀ m₂ . Monad m₂ => m₂ c) -> a -> m c
h' v w = v' >=> w'
  where v' :: ∀ m₁ . Monad m₁ => a -> m₁ b
        v' = const v
        w' :: ∀ m₂ . Monad m₂ => b -> m₂ c
        w' = const w