时间戳

首页 > 解决方案 > 为什么我必须按字段而不是一次强制这种数据类型？

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

问题描述

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

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')

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

标签： haskellcoercion

解决方案

问题在于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 中是做不到的。

推荐阅读