缺少绑定时，haskell中缺少多态推理

html5 • • 问答

类型是否通用取决于绑定的存在与否。这可能会导致意外故障。

这是正常行为吗，有什么原因吗？

{-# LANGUAGE RankNTypes #-}


data IFix0 f a   = IFix0 ( f (IFix0 f) a   ) | In0 a 


msfcata0_OK :: (forall r. (a -> r a) -> (r a -> a) -> f r a -> a) -> (forall z. IFix0 f z) -> a 
msfcata0_OK f = go where go (IFix0 x) = f In0 go x
                         go (In0 v)   = v


msfcata0_KO :: (forall r. (a -> r a) -> (r a -> a) -> f r a -> a) -> (forall z. IFix0 f z) -> a 
msfcata0_KO f  (IFix0 x) = f In0 (msfcata0_KO f) x  -- Couldn't match type ‘IFix0 f a’ with ‘forall z. IFix0 f z’
msfcata0_KO f   (In0 v)  = v

回答

这是一个非常小的重写，以更好地显示正在发生的事情。

{-# Language ScopedTypeVariables, RankNTypes #-}

data IFix0 f a = IFix0 (f (IFix0 f) a) | In0 a


msfcata0_OK
    :: forall f a.
       (forall r. (a -> r a) -> (r a -> a) -> f r a -> a)
    -> (forall z. IFix0 f z) -> a
msfcata0_OK f = go
  where
    go :: IFix0 f a -> a
    go (IFix0 x) = f In0 go x
    go (In0 v)   = v


msfcata0_KO
    :: forall f a.
       (forall r. (a -> r a) -> (r a -> a) -> f r a -> a)
    -> (forall z. IFix0 f z) -> a
msfcata0_KO f (IFix0 x) = f In0 (msfcata0_KO f) x -- line 21
msfcata0_KO f (In0 v)   = v

然后是错误：

    • Couldn't match type ‘IFix0 f a’ with ‘forall z. IFix0 f z’
      Expected type: IFix0 f a -> a
        Actual type: (forall z. IFix0 f z) -> a
    • In the second argument of ‘f’, namely ‘(msfcata0_KO f)’
      In the expression: f In0 (msfcata0_KO f) x
      In an equation for ‘msfcata0_KO’:
          msfcata0_KO f (IFix0 x) = f In0 (msfcata0_KO f) x
    • Relevant bindings include
        x :: f (IFix0 f) a (bound at free.hs:21:22)
        f :: forall (r :: * -> *). (a -> r a) -> (r a -> a) -> f r a -> a
          (bound at free.hs:21:13)
        msfcata0_KO :: (forall (r :: * -> *).
                        (a -> r a) -> (r a -> a) -> f r a -> a)
                       -> (forall z. IFix0 f z) -> a
          (bound at free.hs:21:1)
   |
21 | msfcata0_KO f (IFix0 x) = f In0 (msfcata0_KO f) x -- line 21
   |                                  ^^^^^^^^^^^^^

因此，让我们从查看错误消息开始。它说(msfcata0_KO f)has the type(forall z. IFix0 f z) -> a但第二个参数f需要是IFix0 f a -> a。后一种类型是 with 的特化r ~ IFix0 f，它是In0作为第一个参数传递给 的f。

很明显，这些类型并不匹配。f不能像使用 type 参数(forall z. IFix0 f z) -> a一样使用 type 参数IFix0 f a -> a。要对前者做任何事情，它需要传递一个多态值。要使用后者，它可以利用a在 的上下文中固定的事实f并传入与特定选择一起使用的值a。

那么有什么不同msfcata0_OK呢？好吧，当您创建本地绑定而不提供类型时，类型是本地推断的。我曾经ScopedTypeVariables在重写该函数时指定推断类型。（请注意，此装置f和a类型有在顶级类型签名结合的那些。）这种类型是与类型兼容f，所以它不是通过错误go来f。

不过，这提出了一个明显的问题：如果 GHC 不能(forall z. IFix0 f z) -> a与IFix0 f a -> ain统一msfcata0_KO，为什么它可以在 中统一msfcata0_OK？不同之处在于子类型化方向。在 中msfcata0_OK， type 的表达式IFix0 f a -> a被生成为 type 的值(forall z. IFix0 f z) -> a，这很好。在 中msfcata0_KO， type 表达式(forall z. IFix0 f z) -> a被需要 type 值的东西消耗IFix0 f a -> a，而这不起作用。多态值的子类型化方向取决于类型是处于正位置还是负位置。

在肯定的位置，具体类型是多态类型的子类型。您可以使用类型的值(forall a. a)，如果它是类型的值Int或者Bool，所以(forall a. a)是的超类型Int，Bool以及任何其它具体类型。但在消极的情况下，情况正好相反。一个类型的函数Int -> Bool可以接受一个类型的参数(forall a. a)，但是一个类型的函数(forall a. a) -> Bool不能接受一个类型的参数Int，所以负数(forall a. a)是 的子类型Int。

因此，回到高层次的原始问题 - 通过允许 GHC 从头开始​​为 推断类型go，您改变了它对更多多态和更少多态类型进行统一的地方。这导致子类型关系朝着正确的方向工作，因此类型检查成功。

以上是缺少绑定时，haskell中缺少多态推理的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>