不能以“读者”作为字段“强制”数据类型

Posted 2023-02-18

【中文标题】不能以“读者”作为字段“强制”数据类型

【英文标题】：Cannot 'coerce' data type with 'Reader' as a field

【发布时间】：2020-09-02 12:26:06

【问题描述】：

我有以下 Haskell 代码，可以完美编译：

import Control.Monad.Reader (Reader (..))
import Data.Coerce (Coercible, coerce)

data Flow i o = Flow (i -> o) (o -> i)

coerceFlow
    :: (Coercible i i', Coercible o o')
    => Flow i o
    -> Flow i' o'
coerceFlow = coerce

但是，如果我将 Flow 类型的定义更改为以下内容：

data Flow i o = Flow (i -> Reader Int o) (o -> i)

我开始看到一个奇怪的错误：

Coerce.hs:10:14: error:
    • Couldn't match type ‘o’ with ‘o'’ arising from a use of ‘coerce’
      ‘o’ is a rigid type variable bound by
        the type signature for:
          coerceFlow :: forall i i' o o'.
                        (Coercible i i', Coercible o o') =>
                        Flow i o -> Flow i' o'
        at Coerce.hs:(6,1)-(9,17)
      ‘o'’ is a rigid type variable bound by
        the type signature for:
          coerceFlow :: forall i i' o o'.
                        (Coercible i i', Coercible o o') =>
                        Flow i o -> Flow i' o'
        at Coerce.hs:(6,1)-(9,17)
    • In the expression: coerce
      In an equation for ‘coerceFlow’: coerceFlow = coerce
    • Relevant bindings include
        coerceFlow :: Flow i o -> Flow i' o' (bound at Coerce.hs:10:1)
   |
10 | coerceFlow = coerce
   |              ^^^^^^

据我了解，我的数据类型不再自动为Coercible。有没有办法告诉 GHC 我可以自动强制 Flow 类型的值？我可以手动coerce 每个字段，但我想一次coerce 整个数据类型（这是DerivingVia 工作所必需的）。

我尝试像这样使用RoleAnnotations 扩展：

type role Flow representational representational

但我看到一个错误：

Coerce.hs:6:1: error:
    • Role mismatch on variable o:
        Annotation says representational but role nominal is required
    • while checking a role annotation for ‘Flow’
  |
6 | type role Flow representational representational
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

【参考方案1】：

让我们调查一下：

> :info Reader
type Reader r = ReaderT r Data.Functor.Identity.Identity :: * -> *
        -- Defined in `Control.Monad.Trans.Reader'

所以，Reader 是根据 ReaderT 定义的。

> :info ReaderT
type role ReaderT representational representational nominal
newtype ReaderT r (m :: k -> *) (a :: k)
  = ReaderT runReaderT :: r -> m a
        -- Defined in `Control.Monad.Trans.Reader'

... 并且 ReaderT 在其第三个参数中是 nominal，导致 Reader 在其第二个参数中是 nominal，并使您的强制失败。您不能使用 Flow 类型的角色注释来颠覆这一点，因为这将处理 ReaderT 的先前角色注释。

现在，您可能想知道为什么 ReaderT 有一个 nominal 第三个参数。要理解这一点，请考虑它的定义：

newtype ReaderT r m a = ReaderT (r -> m a)

上面a的作用应该是什么？这得看情况。如果m :: * -> * 在它的参数上是representational，那么ReaderT 在a 上就是这样。 nominal 和 phantom 也是如此。在这里表达角色的“最佳”方式是使用角色多态性，如

type role forall r .
     ReaderT representational (representational :: (* with role r) -> *) r

第三个参数的作用取决于第二个更高种类的参数。

唉，GHC 不支持像上面那样的角色多态性，所以我们只能使用最严格的角色：nominal。

【讨论】：

哦，这其实很有趣。请注意，如果您导入ReaderT（newtype 构造函数是重要部分），您确实会得到coerce :: (Coercible i i', Coercible o o') => Reader i o -> Reader i' o'。但是，即使导入了，OP 的代码也不起作用。看来强制求解器忽略newtypes 上的角色的能力并没有扩展到data。我不确定这是故意的还是疏忽还是什么。

@HTNW 这……很奇怪。我没想到coerce 会打字。看起来 GHC 正在展开第一个 data 定义，但不是 OP 案例中的第二个。

我认为 this proposal 实际上会让 OP 的代码通过允许 GHC 窥视 data 和 newtype 来工作（同样，只要所有相关的构造函数都是可见的）。不过不确定。

【参考方案2】：

@chi 解释的问题不再是问题，如果您避免使用 ReaderT 并使用教科书(->) r monad：

-# LANGUAGE FlexibleContexts #-
module Foo where
import Data.Coerce (Coercible, coerce)

newtype RT r o = RT  runR :: r -> o 
data Flow i o = Flow (i -> RT Int o) (o -> i)

coerceFlow
    :: (Coercible i i', Coercible o o')
    => Flow i o
    -> Flow i' o'
coerceFlow = coerce