我有這個記錄：
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作業？
uj5u.com熱心網友回復：
強制Coercible A B并不意味著Coercion (h A) (h B)對所有人的強制h。
考慮這個 GADT：
data T a where
K1 :: Int -> T A
K2 :: Bool -> T B
強制T A到T B等于強制Int到Bool，這顯然不應該發生。
只有當我們知道 的引數h具有正確的作用（例如representational或phantom，但不是nominal）時，我們才能執行該強制轉換。
現在，在您的特定情況下h是已知的 ( Identity)，并且肯定具有正確的role，因此它應該可以作業。我猜 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)
“注意：”部分就在現場。
我也試著堅持，強迫角色
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)。
轉載請註明出處，本文鏈接：https://www.uj5u.com/yidong/355864.html