为啥不能在 GHC 中强制超功能？

Posted 2023-02-18

【中文标题】为啥不能在 GHC 中强制超功能？

【英文标题】：Why can't hyperfunctions be coerced in GHC?为什么不能在 GHC 中强制超功能？

【发布时间】：2020-09-23 17:38:40

【问题描述】：

我有以下类型，基于论文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？

【问题讨论】：

哇，这听起来确实像 GHC 错误！请举报！

嗯...实际上，这很棘手。不，可能没有解决方法。

我猜你不想要(#.) _ = rmap coerce，对吧？

@chi，这根本没用，因为它不是免费的。

@chi，我应该更具体一些。编写该定义根本没有用，因为这是默认定义所做的。

【参考方案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 页上进一步指出，“事实上，我们知道它对递归新类型的处理......算法是不完整的”（即，存在无法推断的类型安全强制实现的算法）。您可能还想浏览 issue #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 b c 和Hyper 的第二个参数的代表角色派生Coercible (Hyper a b) (Hyper a c)。

不幸的是，整个算法都是语法导向的，所以新类型总是会以这种方式展开，并且没有办法让 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 是要走的路。

【讨论】：

喂。我想我最初的猜测比我后来的猜测要好。多么可怕的事情：将构造函数带入范围会阻止模块进行类型检查。坦率地说，这似乎是一个不可接受的情况！

有人对此有解释吗？听起来好像 newtype-unwrapping 只是作为一种针对非常具体的东西的 hack 而引入的。

仅供参考，我刚刚打开了GHC ticket 来看看这个。

@leftaroundabout, newtype wrapping/unwrapping 是强制公理的基本类型之一。而且它相当有用：coerce :: [a] -> [Sum a] 等。