在 where 子句中指定函数类型签名

Question

以下函数从列表中实现了很好的旧 filter 函数通过使用 recursion-schemes 库。

import Data.Functor.Foldable 

catafilter :: (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    -- alg :: ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

编译成功，像catafilter odd [1,2,3,4]这样的简短测试成功。但是，如果我取消注释 alg 的类型签名，我会收到以下错误：

src/cata.hs:8:30: error:
    • Couldn't match expected type ‘a’ with actual type ‘a1’
      ‘a1’ is a rigid type variable bound by
        the type signature for:
          alg :: forall a1. ListF a1 [a1] -> [a1]
        at src/cata.hs:6:5-29
      ‘a’ is a rigid type variable bound by
        the type signature for:
          catafilter :: forall a. (a -> Bool) -> [a] -> [a]
        at src/cata.hs:3:1-39
    • In the first argument of ‘p’, namely ‘x’
      In the expression: (p x)
      In the expression: if (p x) then x : xs else xs
    • Relevant bindings include
        xs :: [a1] (bound at src/cata.hs:8:18)
        x :: a1 (bound at src/cata.hs:8:16)
        alg :: ListF a1 [a1] -> [a1] (bound at src/cata.hs:7:5)
        p :: a -> Bool (bound at src/cata.hs:4:12)
        catafilter :: (a -> Bool) -> [a] -> [a] (bound at src/cata.hs:4:1)
  |
8 |     alg  (Cons x xs) = if (p x) then x : xs else xs
  |                              ^

SO 问题的答案type-signature-in-a-where-clause 建议使用 ScopedTypeVariables 扩展。 why-is-it-so-uncommon-to-use-type-signatures-in-where-clauses 的最后一个答案中的评论建议使用 forall 量化。

所以我补充说：

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

在我模块的顶部，并尝试了 alg 的不同类型签名，例如： alg :: forall a. ListF a [a] -> [a] 或 alg :: forall b. ListF b [b] -> [b] 或将 forall 添加到 catalist 类型签名。没有编译！

问题：为什么我无法为 alg 指定类型签名？

Answer 1

这个有效

{-# Language ScopedTypeVariables #-}

import Data.Functor.Foldable 

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg
  where
    alg :: ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

如果省略 forall，它们是完全不同的 a（尽管在句法上它们是相同的）。

由于隐式量化，您未注释的版本被视为

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg
  where
    alg :: forall a1. ListF a1 [a1] -> [a1]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

这解释了您的错误消息：

Couldn't match expected type ‘a’ with actual type ‘a1’

谓词 (p :: a -> Bool) 需要类型为 a 的参数，但它是 x :: a1 来自 Cons x xs :: ListF a1 [a1] 的参数！

根据错误消息中的绑定，查看显式量化版本是否有意义：

xs         :: [a1] 
x          :: a1
alg        :: ListF a1 [a1] -> [a1] 
p          :: a -> Bool 
catafilter :: (a -> Bool) -> [a] -> [a]

Answer 2

没有扩展，原始未注释的代码

catafilter :: (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

等同于启用ScopedTypeVariables后，显式量化所有类型变量，如下：

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: forall a. ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

这又等同于（通过 alpha 转换量化变量）

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: forall b. ListF b [b] -> [b]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

这会触发类型错误，因为 p 想要一个 a 参数，但是 p x 传递了一个 b 参数。

重点是，启用扩展后，以 forall b. ... 开头的函数有望与 b 的任何选项一起使用。这个承诺对 alg 来说太强了，它只对 catafilter 的 a 有效。

因此，解决方案如下。 catafilter 的类型可以承诺与它的调用者可能选择的任何 a 一起工作：我们可以在那里添加 forall a.。相反，alg 必须承诺只使用 catafilter 的相同 a，因此我们重用类型变量 a 而无需添加另一个 forall.

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

这个编译是因为 ScopedTypeVariables 看到 a 在范围内，并且不会在 alg 中添加隐式 forall （因为它会在没有扩展名的情况下发生） .

总结：

没有ScopedTypeVariables，每个类型注释都有自己隐含的forall ...，量化所有变量。没有注解可以引用其他注解的变量（可以重用同名，但不认为是同一个变量）
与ScopedTypeVariables，定义foo :: forall t. T t u ; foo = def的处理如下：
- 类型变量t在类型检查时被普遍量化并引入作用域def：def中的类型注解可以参考t
- 类型变量u，如果当前在范围内，指的是外部定义的u
- 类型变量u，如果不在范围内，则在类型检查时被普遍量化但不进入范围def（为了兼容性，这里我们遵循相同的行为而没有扩展名）

Answer 3

这行得通，并且避免了与 foralls

的所有违反直觉的混淆

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Functor.Foldable 

catafilter :: (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    -- alg :: ListF a [a] -> [a]
    alg  (Nil :: ListF aa [aa])  =  [] :: [aa]
    alg  (Cons x xs) = if (p x) then x : xs else xs

在 alg Nil 等式上我实际上可以使用 tyvar a：我使用 aa 只是为了表明它们是不同的绑定。因为 aa 出现在模式上，所以编译器将它与 catafilter.

的签名中的 a 统一起来

您可以 also/instead 将类型注释放在 alg Cons 等式上。

我理解@Jogger 的困惑，为什么 ghc 对 forall 的位置如此挑剔；以及 forall 可能表示 RankNTypes.

的紧张情绪

Answer 4

问题是 alg 依赖于外部 p，所以 alg 的类型不能简单地是多态的。

一个简单的解决方法是通过将它们作为函数参数传入，使其独立于任何外部实体，这样函数就可以像预期的那样具有其简单的多态类型：

catafilter :: (a -> Bool) -> [a] -> [a]
catafilter = cata . alg
  where
    alg :: (b -> Bool) -> ListF b [b] -> [b]
    alg p Nil  =  []
    alg p (Cons x xs)  =  if (p x) then x : xs else xs

这不需要任何语言扩展。

在 where 子句中指定函数类型签名

Specifying a function type signature in a where clause

haskell

ghc

catamorphism

recursion-schemes