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 回答