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

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中完成。