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

Posted 2023-02-18

【中文标题】为啥我必须按字段强制这种数据类型，而不是一次强制？

【英文标题】：Why do I have to coerce this data type by fields, rather than all at once?为什么我必须按字段强制这种数据类型，而不是一次强制？

【发布时间】：2019-11-09 15:15:48

【问题描述】：

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

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

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

【问题讨论】：

好的，我想我明白了。有一个隐含的type role Iso representational nominal nominal，因为编译器无法预测m 的参数是名义上的还是代表性的，所以它很安全。现在我只希望有一种方法可以要求type role m representational representational

在这个 GHC 提案实施后可以指定这样的类型角色：github.com/ghc-proposals/ghc-proposals/pull/233我昨天遇到了类似的问题。

【参考方案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 未经修改通过。

【讨论】：

不错！在我目前的情况下不起作用 m is a natural transformation 但绝对是放入我的工具箱的有用技巧。

【参考方案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 中是做不到的。

【讨论】：

是的，我期待某种依赖类型的角色，其中type role Iso m = type role m

@rampion 确实如此。我试图将type role 附加到同义词，但这也是不允许的。