8

我有以下类型，它基于论文Cooutining 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 cand Coerrcible (Hyper c a) (Hyper b a)，而后者需要Coercible (Hyper a b) (Hyper a c)，但它进入了一个无限循环。

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

4

1 回答 1

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

我不认为这是一个错误。相反，这是用于推断类型安全强制的算法的限制。在描述该算法的论文中，承认类型检查递归新类型可能会发散，并且“按设计”的行为是减少计数器将检测循环并报告错误。（例如，参见第 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 示例中一样，这是因为新类型的展开行为。如果您将 newtype 切换为 a data，它可以正常工作，因为 GHC 不会尝试解包，而是可以Coercible (Hyper a b) (Hyper a c)直接从的第二个参数Coercible b c的代表角色派生。Hyper

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

于 2020-06-06T20:14:37.697 回答