haskell - 为什么我必须按字段强制此数据类型，而不是一次全部强制？

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 的角色在你的一般Iso类型。

考虑:

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

type (<->) = Iso T

你不能真的指望能够转换T () ()进入T () (Identity ())即使()和Identity ()是强制性的。

您需要类似(伪代码)的内容:

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

但我相信，这在当前的 Haskell 中无法完成。