这是如何构成Haskell刚性类型错误的？

Question

这有效:

data Wrapped a = Wrapped a

alpha :: IO s -> IO ()
alpha x = do
    rv <- wrapit x
    return ()
    where       
        wrapit :: IO s -> IO (Wrapped s)
        wrapit x' = do 
            a <- x'
            return (Wrapped a)

这不是:

data Wrapped a = Wrapped a

alpha :: IO s -> IO ()
alpha x = do
    rv <- wrapit
    return ()
    where       
        wrapit :: IO (Wrapped s)
        wrapit = do 
            a <- x
            return (Wrapped a)

为什么？

Answer 1

这是由于在标准Haskell中对类型变量进行作用域和量化的方式.您可以使第二个版本像这样工作:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

module RigidProblem where

data Wrapped a = Wrapped a

alpha :: forall s. IO s -> IO ()                                                
alpha x = do
    rv <- wrapit
    return ()
    where       
        wrapit :: IO (Wrapped s)
        wrapit = do 
            a <- x
            return (Wrapped a)

有两个更改:启用RankNTypes和ScopedTypeVariables语言扩展,并forall s在类型签名中添加explicit alpha.这两个扩展中的第一个允许我们引入显式,forall s从而将s范围带入体内alpha,而第二个使得它使得签名on wrapit不被类型推理引擎包含隐式forall s- 相反,该s签名用于命名一个类型变量,该变量应该在范围内并用它来标识.

如果我理解正确的话,Haskell中当前的默认情况是所有刚性类型变量(意味着类型变量出现在程序员明确提供的类型签名中)是隐式量化的,而不是词法范围,因此无法引用来自内部范围中提供的显式签名中的外部范围的刚性类型变量...(哦,麻烦,我确定有人可以比这更好地表达它.)无论如何,从类型检查器的角度来看,sin alpha's签名和wrapit签名中的签名是完全无关的,不能统一 - 因此是错误.

请参见本页面从GHC文档和本页面了解更多信息从哈斯克尔总理维基.

更新:我刚刚意识到我从未解释为什么第一个版本有效.为了完整起见:注意,与第一个版本,你可以使用t代替s在wrapit的签名,没有什么会改变.您甚至可以wrapit从where块中取出并使其成为单独的顶级功能.关键点在于它是一个多态函数,因此类型wrapit x由类型决定x.第一个版本wrapit的签名中使用的类型变量与签名中使用的类型变量的关系在alpha这里没有任何用处.随着第二个版本,这是当然是不同的,你必须诉诸上述挂羊头卖狗肉做wrapit的s是同样的事情alpha的s.

Answer 2

MichałMarczyk的上述答案是正确的,但值得注意的是,如果删除wrapit函数的类型签名,第二个版本确实有效:

data Wrapped a = Wrapped a

alpha :: IO s -> IO ()
alpha x = do
    rv <- wrapit
    return ()
    where
        -- No type signature here!
        wrapit = do
            a <- x
            return (Wrapped a)

也就是说,问题不在于代码本身; 这就是Haskell 98不允许你为wrapit函数写一个类型签名,因为它包含一个由它的上下文绑定的类型变量(外部alpha函数),而H98没有办法表达它.正如Michał所说,启用ScopedTypeVariables允许您这样做.