在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问题type-signature-in-a-where-clause 的答案建议使用ScopedTypeVariables扩展.最后答案为什么是如此不常见的类型签名在where-clauses中的评论 建议使用forall量化.

所以我补充说:

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

在我的模块的顶部和尝试不同类型的签名ALG像: alg :: forall a. ListF a [a] -> [a]或 alg :: forall b. ListF b [b] -> [b]或添加FORALL在凯利板型签名.没有编译!

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

Answer 1

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

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.

所以,解决方案如下.catafilter可以承诺a与其调用者可能选择的任何类型:我们可以在forall a.那里添加.相反,alg必须承诺只使用相同a的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

这个编译自ScopedTypeVariables认为这a是在范围,并且不添加隐含forall的alg(因为它没有将第扩展发生).

摘要:

• 没有ScopedTypeVariables,每个类型注释都有自己隐含forall ...的顶部,量化所有变量.没有注释可以引用其他注释的变量(您可以重用相同的名称,但它不被视为相同的变量).
• 使用时ScopedTypeVariables,定义foo :: forall t. T t u ; foo = def处理如下:
  • 类型变量t是普遍量化的,并在类型检查时引入范围def:类型注释def可以参考t
  • u如果当前在范围内,则类型变量引用外部定义的变量u
  • 类型变量u(如果不在范围内)是普遍量化的,但在类型检查时没有带入范围def(为了兼容性,这里我们遵循相同的行为,没有扩展名)

Answer 2

这有效

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