She*_*rsh 10 haskell coercion coerce newtype
我有以下 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
Run Code Online (Sandbox Code Playgroud)
但是,如果我将Flow类型的定义更改为以下内容:
data Flow i o = Flow (i -> Reader Int o) (o -> i)
Run Code Online (Sandbox Code Playgroud)
我开始看到一个奇怪的错误:
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
| ^^^^^^
Run Code Online (Sandbox Code Playgroud)
据我了解,我的数据类型不再是Coercible自动的。有没有办法告诉 GHC 我可以Flow自动强制类型值?我可以coerce手动每个字段,但我想coerce一次完成整个数据类型(这是DerivingVia工作所必需的)。
我尝试使用这样的RoleAnnotations扩展:
type role Flow representational representational
Run Code Online (Sandbox Code Playgroud)
但我看到一个错误:
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
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Run Code Online (Sandbox Code Playgroud)
我们来调查一下:
> :info Reader
type Reader r = ReaderT r Data.Functor.Identity.Identity :: * -> *
-- Defined in `Control.Monad.Trans.Reader'
Run Code Online (Sandbox Code Playgroud)
所以,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'
Run Code Online (Sandbox Code Playgroud)
...并且ReaderT是nominal在它的第三个参数,导致Reader要nominal在其第二个参数,使您的威逼失败。您不能使用您的Flow类型的角色注释来颠覆这一点,因为这将处理之前的ReaderT.
现在,您可能想知道为什么ReaderT有nominal第三个参数。要理解这一点,请考虑其定义:
newtype ReaderT r m a = ReaderT (r -> m a)
Run Code Online (Sandbox Code Playgroud)
a上面应该起什么作用?这要看情况。如果m :: * -> *是representational在它的论点上,那么ReaderT在 上就是这样a。这同样适用于nominal和phantom。在这里表达角色的“最佳”方式是使用角色多态性,如
type role forall r .
ReaderT representational (representational :: (* with role r) -> *) r
Run Code Online (Sandbox Code Playgroud)
其中第三个参数的作用取决于第二个更高级的参数。
唉,GHC 不支持像上面那样的角色多态性,所以我们只能使用最严格的角色:nominal.