haskell - 代表性功能的不动点

爱德华·克梅特(Edward Kmett)的实验性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)

我相信以下内容应该会起作用，除了遗漏的那一部分。我还担心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

点点滴滴roles

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不能随意匹配。

一个(可能有效吗？)概念，我只是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/