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

Question

以下函数使用递归方案库从列表中实现了良好的旧过滤器函数。

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 question 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]或者在catlist类型签名中alg :: forall b. ListF b [b] -> [b]添加一个forall 。没有编译！

问题：为什么我不能为alg指定类型签名？

score 10 · Accepted Answer

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

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，只适用于相同a的catafilter。

因此，解决方案如下。can的类型catafilter承诺与a它的调用者可能选择的任何一起工作：我们可以在forall a.那里添加。相反，alg必须保证只使用相同a的 of catafilter，所以我们重用类型变量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

this 编译，因为ScopedTypeVariables看到它a在范围内，并且不添加隐式forallin alg（因为它会在没有 th 扩展的情况下发生）。

概括：

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

score 5 · Accepted Answer

这有效

{-# 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

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

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

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]

score 1 · Accepted Answer

这有效，并且避免了所有反直觉forall的 s

{-# 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出现在一个模式上，编译器将它与a来自签名的catafilter.

您也可以/相反将类型注释放在alg Cons等式上。

我理解@Jogger 对为什么 ghc 对forall;的位置如此挑剔的困惑。以及 aforall或许表明的紧张情绪RankNTypes。

score 1 · Accepted Answer

问题在于它alg依赖于一个 external p，所以alg's 的类型不能简单地是多态的。

一种简单的解决方法是使其独立于任何外部实体，方法是将它们作为函数参数传入，以便函数可以按预期具有其简单的多态类型：

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

这不需要任何语言扩展。

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

4 回答 4

Related

Reference