爱德华·克梅特的实验 roles package提供了各种用于解除强制的实用程序,其中一些我已粘贴在本问题的末尾。包中的关键类是
class Representational (t :: k1 -> k2) where
-- | An argument is representational if you can lift a coercion of the argument into one of the whole
rep :: Coercion a b -> Coercion (t a) (t b)
给定类型
newtype Fix p a = In {out :: p (Fix p a) a}
我希望写出类似的东西
instance Representational p => Representational (Fix p)
我相信除了缺少一 block 之外,以下内容应该有效。我还有点担心 bar
可能过于严格,导致所有内容都陷入无限循环。
-- With {-# LANGUAGE PolyKinds, ScopedTypeVariables, etc.)
import Data.Type.Coercion
import Data.Coerce
import Data.Roles
instance Representational p => Representational (Fix p) where
rep :: forall a b . Coercion a b -> Coercion (Fix p a) (Fix p b)
rep x = sym blah . quux . baz . blah
where
bar :: Coercion (p (Fix p a)) (p (Fix p b))
bar = rep (rep x)
baz :: Coercion (p (Fix p a) a) (p (Fix p b) a)
baz = eta bar
quux :: Coercion (p (Fix p b) a) (p (Fix p b) b)
quux = undefined -- ?????????
blah :: forall x . Coercion (Fix p x) (p (Fix p x) x)
blah = Coercion
角色的点点滴滴
eta :: forall (f :: x -> y) (g :: x -> y) (a :: x).
Coercion f g -> Coercion (f a) (g a)
instance Representational Coercion
instance Representational f => Representational (Compose f)
最佳答案
如上所述,这个问题无法解决,因为 p
是Representational
(甚至是Phantom
)这一事实并不意味着p (Fix p a)
是代表性的。这是一个反例:
data NF a b where
NF :: NF a ()
instance Representational NF where
rep _ = Coercion
显然,NF a
从来都不是代表性的;我们不可能实现
rep :: Coercion x y -> Coercion (NF a x) (NF a y)
(无论选择a
),因为NF a x
仅在x ~ ()
时才存在。
因此,我们需要一个更精确的表征双仿函数概念来使这个想法变得合理。在任何情况下,unsafeCoerce
几乎肯定是实现它所必需的,因为挖掘无限的 Coercion
链将花费无限的时间,而 Coercion
code>无法延迟匹配。
一个(可能有效?)概念,我只是 suggested on GitHub :
class Birepresentational t where
birep :: Coercion p q -> Coercion a b -> Coercion (t p a) (t q b)
instance Birepresentational f => Representational (Fix f) where
rep (x :: Coercion a b) = (birep :: forall p q x y . Coercion p q -> Coercion x y -> Coercion (f p x) (f q y))
(unsafeCoerce x :: Coercion (Fix f a) (Fix f b))
x `seq` unsafeCoerce x
强制应用birep
的目的是(希望)确保它确实终止,因此它的类型是可信的。
关于haskell - 代表性双仿函数的不动点,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34080644/