为什么较高级别的类型在Haskell中如此脆弱

Question

我正在搞乱这个runST功能.哪种类型(forall s. ST s a) -> a,似乎试图以任何方式使用它,没有任何间接直接应用,以非常讨厌的方式打破它.

runST :: (forall s. ST s a) -> a
const :: a -> b -> a

所以通过替换a在const为forall s. ST s a你应该得到的类型const runST

const runST :: b -> (forall s. ST s a) -> a

但是相反GHC说它无法a与之相匹配,(forall s. ST s a) -> a但由于a字面上的意思forall a. a是每种类型都满足,我不明白这是什么无效.

事实证明使用\_ -> runST实际上工作得很好,并提供正确的类型.

一旦我拥有constST了正确的类型,我想看看我是否uncurry可以,但不出所料,这也打破了.但它似乎真的不应该,尽管这种情况似乎不像前一个那么明显:

constST :: b -> (forall s. ST s a) -> a
uncurry :: (a -> b -> c) -> (a, b) -> c

所以,那肯定a在uncurry可以与被替换b的constST和b在uncurry可以与被替换(forall s. ST s a)的constST和a在uncurry可以与被替换c的constST.这给了我们:

uncurry constST :: (b, forall s. ST s a) -> a

现在不可否认,这种类型是不可预测的,我知道这是很有问题的.但在技术上,Just mempty当直接替代而不移动隐式forall量化时也是不可预测的.

Just :: a -> Maybe a
mempty :: forall a. Monoid a => a
Just mempty :: Maybe (forall a. Monoid a => a)

但是forall会自动浮出来给你:

Just mempty :: forall a. Monoid a => Maybe a

现在,如果我们做同样的事情,uncurry constST我们应该明智,并据我所知正确的类型:

uncurry constST :: (forall s. (b, ST s a)) -> a

哪个级别更高但不具有预测性.

有人可以向我解释为什么基本上没有上述内容实际上与GHC 8一起工作,是否有更基本的东西使得上述情况在一般情况下非常复杂？因为如果没有它似乎真的很好有上面的工作,如果只是为了摆脱$纯粹的烦人的特殊外壳runST.

另一方面,forall我们可以改为ImpredicativeTypes完全正常工作,而不是所有的浮动.它正确地推断类型Just mempty的Maybe (forall a. Monoid a => a),但它似乎像真正使用它并不那么容易.我听说过impredicative类型推断不是真的可行,但它会以某种方式限制对谓词类型的类型推断,除非你提供类型签名来指示其他方式.类似于MonoLocalBinds默认情况下为了类型推断而使局部绑定单态化.

Answer 1

您已回答了自己的问题:

...代a中const的forall s. ST s a...

这是定义impredictive多态性 -实例化一个类型的变量用的能力的多型体,其(松散地)具有一个类型forall在该类型的最左侧量词.

从关于这个主题的GHC trac页面:

GHC(尚未)支持不可预测的多态性

而且

我们已经做了各种尝试来支持不信任,所以有一面旗帜-XImpredicativeTypes.但它不起作用,绝对不受支持.如果你使用它,你就是独立的; 我对将要发生的事情没有任何承诺.

所以不要使用ImpredictiveTypes- 它无济于事.

现在有关血腥的细节 - 为什么所有具体的例子都像他们一样工作？

您已经注意到在表达式中Just mempty,Maybe (forall a. Monoid a => a)不推断出不可预测的类型; 相反,它forall是"浮出水面".您还注意到执行相同的过程uncurry constST会给出"更高等级但不具有不可预测性"的类型.该GHC用户指南有这样说的更高级别的类型:

通常,任意秩类型的类型推断是不可判定的....

对于lambda-bound或case-bound变量x,要么程序员为x提供显式多态类型,要么GHC的类型推断将假设x的类型中没有foralls.

所以你真的需要帮助它,并且通常排除了完全使用高阶函数(注意上面没有说明任意应用程序,只有绑定变量 - 并且uncurry constST没有绑定变量!).正确的类型Just mempty是等级1,因此没有问题推断它,有或没有其他类型签名.

例如,您可以这样编写(forall s. (b, ST s a)) -> a函数(至少在GHC 8.0.1上):

constST' :: forall a b . (forall s . (b, ST s a)) -> a
constST' z = runST z' 
  where z' :: forall s . ST s a
        z' = snd z

并且还要注意,您甚至无法对该对进行模式匹配,因为这会立即实例化绑定b类型var:

constST' :: forall a b . (forall s . (b, ST s a)) -> a
constST' (a,b) = _res 

使用打字的洞,你会得到:

* Found hole: _res :: a
  Where: `a' is a rigid type variable bound by
           the type signature for:
             constST' :: forall a b. (forall s. (b, ST s a)) -> a
* In the expression: _res
  In an equation for constST': constST' (a, b) = _res
* Relevant bindings include
    b :: ST s0 a 
    a :: b 

需要注意的类型b是ST s0 a一些清爽型的变量 s0,而不是必需forall s . ST s a的runST.没有办法让旧类型回来.

对于这类事情最简单的解决方案可能是定义一个newtype,如GHC trac页面所示:

newtype RunnableST a = RST (forall s . ST s a)

rrunST :: RunnableST a -> a 
rrunST (RST a) = runST a 

并存储ST准备在此容器中运行的操作:

doSomething :: RunnableST X
doSomething = RST $ do ...