haskell - 为什么不能在 GHC 中强制超功能？

Question

我有以下类型，它基于论文 Coroutining folds with hyperfunctions :

newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }

它的第一个参数是逆变的，第二个参数是协变的，所以它是一个 profunctor:

instance Profunctor Hyper where
  lmap f = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> h $ Hyper $ f . k . go

  rmap g = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> g $ h $ Hyper $ k . go

  dimap f g = go where
    go (Hyper h) = Hyper $ \(Hyper k) -> g $ h $ Hyper $ f . k . go

我还想实现(可能不安全的)强制运算符:

  -- (#.) :: Coercible c b => q b c -> Hyper a b -> Hyper a c
  (#.) _ = coerce

  -- (.#) :: Coercible b a => Hyper b c -> q a b -> Hyper a c
  (.#) = const . coerce

但是，当我这样做时，我收到以下错误消息:

   • Reduction stack overflow; size = 201
     When simplifying the following type:
       Coercible (Hyper a b) (Hyper a c)
     Use -freduction-depth=0 to disable this check
     (any upper bound you could choose might fail unpredictably with
      minor updates to GHC, so disabling the check is recommended if
      you're sure that type checking should terminate)
   • In the expression: coerce
     In an equation for ‘#.’: (#.) _ = coerce

我猜它正在尝试验证 Coercible (Hyper a b) (Hyper a c) , 这需要 Coercible b c和 Coerrcible (Hyper c a) (Hyper b a) , 后者需要 Coercible (Hyper a b) (Hyper a c) ，但它进入一个无限循环。

知道我会用什么注释来解决这个问题，如果有的话？还是我应该硬着头皮使用 unsafeCoerce ?

Answer 1

我认为很明显 Profunctor实例在这里不起作用，因此以下独立程序给出了相同的错误:

import Data.Coerce
newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }
(#.) :: (Coercible c b) => q b c -> Hyper a b -> Hyper a c
(#.) _ = coerce

我不认为这是一个错误。相反，这是用于推断类型安全强制的算法的限制。在 the paper描述算法，它承认类型检查递归新类型可能会发散，并且“按设计”的行为是减少计数器将检测循环并报告错误。 (例如，请参见第 27 页。)在第 30 页上进一步指出，“事实上，我们知道它对递归新类型的处理......算法是不完整的”(即，存在无法由实现的算法)。您可能还想浏览问题 #15928 中的讨论。关于类似的循环。

这里发生的是 GHC 试图解决 Coercible (Hyper a b) (Hyper a c)首先打开新类型以产生新目标:

Coercible (Hyper b a -> b) (Hyper c a -> c)

这需要 Coercible (Hyper b a) (Hyper c a) GHC 试图通过首先解开新类型以产生新目标来解决这个问题:

Coercible (Hyper a b -> a) (Hyper a c -> a)

这需要 Coercible (Hyper a b) (Hyper a c) ，我们陷入了一个循环。

与问题 #15928 示例中一样，这是因为新类型的展开行为。如果将新类型切换为 data ，它工作正常，因为 GHC 不会尝试解包，而是可以导出 Coercible (Hyper a b) (Hyper a c)直接来自 Coercible b c以及 Hyper 的代表角色的第二个参数。

不幸的是，整个算法是语法导向的，所以 newtypes 总是会以这种方式展开，并且没有办法让 GHC “推迟”展开并尝试替代证明。

除了有......新类型只有在构造函数在范围内时才会被解包，所以你可以将它分成两个模块:

-- HyperFunction.hs
module HyperFunction where
newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }

-- HyperCoerce.hs
module HyperCoerce where
import HyperFunction (Hyper)  -- don't import constructor!
import Data.Coerce
(#.) :: (Coercible c b) => q b c -> Hyper a b -> Hyper a c
(#.) _ = coerce

它的类型检查很好。

如果这太难看或导致一些其他问题，那么我猜 unsafeCoerce是要走的路。