为什么我必须按字段强制这种数据类型，而不是一次强制？

Question

我有两种类型 (<->) 和 (<-->) 代表类型之间的同构：

data Iso (m :: k -> k -> *) a b = Iso { to :: m a b, from :: m b a }
type (<->) = Iso (->)
infix 0 <->

data (<-->) a b = Iso' { to' :: a -> b, from' :: b -> a }
infix 0 <-->

两者之间的唯一区别是(<->) 是更通用类型的特化。

我可以很容易地coerce(<-->) 同构：

coerceIso' :: (Coercible a a', Coercible b b') => (a <--> b) -> (a' <--> b')
coerceIso' = coerce 

但是当我尝试使用 (<->) 同构时出现错误：

coerceIso :: (Coercible a a', Coercible b b') => (a <-> b) -> (a' <-> b')
coerceIso = coerce
{-
src/Data/Iso.hs:27:13: error:
    • Couldn't match type ‘a’ with ‘a'’ arising from a use of ‘coerce’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          coerceIso :: forall a a' b b'.
                       (Coercible a a', Coercible b b') =>
                       (a <-> b) -> a' <-> b'
        at src/Data/Iso.hs:25:1-73
      ‘a'’ is a rigid type variable bound by
        the type signature for:
          coerceIso :: forall a a' b b'.
                       (Coercible a a', Coercible b b') =>
                       (a <-> b) -> a' <-> b'
        at src/Data/Iso.hs:25:1-73

-}

我目前的解决方法是分别强制执行前进和后退功能：

coerceIso :: (Coercible a a', Coercible b b') => (a <-> b) -> (a' <-> b')
coerceIso (Iso f f') = Iso (coerce f) (coerce f')

但是为什么需要这样的解决方法呢？为什么不能直接强制(<->)？

Answer 1

不是一个直接的答案，但我想分享这个相关的技巧：每当m 是profunctor（我怀疑它通常是），你可以使用米田式的转换来制作一个具有代表性的等价类型论据。

newtype ProYo m a b = Yo2 (forall x y. (x -> a) -> (b -> y) -> m x y)

ProYo m 与 m 同构，除了它的参数角色是代表性的，通过以下同构：

toProYo :: (Profunctor m) => m a b -> ProYo m a b
toProYo m = ProYo (\f g -> dimap f g m)

fromProYo :: ProYo m a b -> m a b
fromProYo (ProYo p) = p id id

如果我们这样定义你的Iso

data Iso m a b = Iso { to :: ProYo m a b, from :: ProYo m b a }

coerceIso 未经修改通过。

Answer 2

问题在于参数m 在您的一般Iso 类型中的作用。

考虑：

data T a b where
  K1 :: Int    -> T () ()
  K2 :: String -> T () (Identity ())

type (<->) = Iso T

即使() 和Identity () 是强制的，你也不能指望能够将T () () 转换为T () (Identity ())。

你需要类似（伪代码）：

type role m representational representational =>
          (Iso m) representational representational

但我相信这在当前的 Haskell 中是做不到的。