5

我有这个记录：

import Data.Functor.Identity
import Control.Monad.Trans.Identity
import Data.Coerce

data Env m = Env {
        logger :: String -> m ()
    }

env :: Env IO
env = undefined

和这个强制函数

decorate 
    :: Coercible (r_ m) (r_ (IdentityT m))   
    => r_ m -> r_ (IdentityT m)        
decorate = coerce

这适用于没有问题的记录值：

decoratedEnv :: Env (IdentityT IO)
decoratedEnv = decorate env

但是，如果我定义唯一稍微复杂的记录

data Env' h m = Env' {
        logger' :: h (String -> m ())
    }

env' :: Env' Identity IO
env' = undefined

并尝试IdentityT像以前一样插入包装器

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = decorate env'

我得到错误：

* Couldn't match type `IO' with `IdentityT IO'
    arising from a use of `decorate'

在我看来，额外的Identity参数Env'不应该停止coerce工作。为什么coerce在这种情况下会失败？有没有办法让coerce工作？

4

1 回答 1

5

强制Coercible A B并不意味着Coercion (h A) (h B)对所有人都强制h。

考虑这个 GADT：

data T a where
  K1 :: Int  -> T A
  K2 :: Bool -> T B

强制T AtoT B等于强制Intto Bool，这显然不应该发生。

只有当我们知道参数h具有正确的角色（例如representationalor phantom，但不是nominal）时，我们才能执行该强制。

现在，在您的具体情况下h是已知的（Identity），并且肯定具有正确的角色，所以它应该可以工作。我猜 GHC 强制系统在处理这种“行为良好”h的同时拒绝行为不端的强制系统并没有那么强大，所以它保守地拒绝一切。

添加一个类型孔似乎证实了这一点。我试过

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = _ decorate' @(Env' Identity)

并得到了错误

* Couldn't match representation of type: r_0 m0
                           with that of: r_0 (IdentityT m0)
    arising from a use of decorate'
  NB: We cannot know what roles the parameters to `r_0' have;
    we must assume that the role is nominal
* In the first argument of `_', namely decorate'
  In the expression: _ decorate' @(Env' Identity)
  In an equation for decoratedEnv':
      decoratedEnv' = _ decorate' @(Env' Identity)

“NB：”部分就在现场。

我也尝试过坚持，并且强迫角色

type role Env' representational representational
data Env' h m = Env' {
        logger' :: h (String -> m ())
    }

无济于事：

* Role mismatch on variable m:
    Annotation says representational but role nominal is required
* while checking a role annotation for Env'

我能找到的最好的解决方法是打开/重新包装，并利用QuantifiedConstraints本质上要求h具有非nominal角色：

decorate' 
    :: (forall a b. Coercible a b => Coercible (h a) (h' b))
    => Coercible m m'
    => Env' h m -> Env' h' m'
decorate' (Env' x) = Env' (coerce x)

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = decorate' env'

这不是一个理想的解决方案，因为它违背了Coercible. 在这种情况下，重新包装只有 O(1) 成本，但如果我们有一个Env' Identity IO要转换的列表，我们将支付 O(N)。

于 2021-11-09T15:55:03.357 回答