1

我有

{-# LANGUAGE RankNTypes, TypeInType #-}

import Data.Coerce
import Data.Kind

newtype IFix f i = IFix { unIFix :: f (IFix f) i }

class IFunctor (f :: (i -> Type) -> i -> Type) where
  imap :: (forall i'. a i' -> b i') -> (forall i'. f a i' -> f b i')

f :: IFunctor f => forall i. IFix f i -> IFix f i
f = undefined

g :: IFunctor f => forall i. IFix f i -> IFix f i
g = IFix . imap f . unIFix

h :: IFunctor f => forall i. IFix f i -> IFix f i
h = coerce . imap f . coerce

i :: IFunctor f => forall i. IFix f i -> IFix f i
i = coerce (imap f)

其中IFix是索引类型构造函数的类型级固定点，i是索引（幻像参数），IFunctor是实际上是函子的此类索引类型构造函数的类，f只是一个随机函数，g, h，i尝试f在IFix包装下传播。附注：这是一个简化的示例，实际上我经常在其他设置中遇到类似的问题，手动重新包装变得有点乏味（对于一个我想避免将 unwrap-rewrap 函数映射到列表或其他结构）。

input:18:5: error:
    • Couldn't match representation of type ‘f (IFix f) i’
                               with that of ‘f0 (IFix f1) i0’
        arising from a use of ‘coerce’
   |
18 | h = coerce . imap f . coerce
   |     ^^^^^^

input:21:5: error:
    • Couldn't match representation of type ‘f (IFix f) i’
                               with that of ‘f2 (IFix f3) i1’
        arising from a use of ‘coerce’
   |
21 | i = coerce (imap f)
   |     ^^^^^^^^^^^^^^^

老实说，我并不感到惊讶，但是由于我看不到强制的底层，我想知道，有没有办法修改我的定义，以便coerce可以应用？我试过RoleAnnotations但是

  1. type role IFix nominal phantom是无效的
  2. 我不知道如何为类型类要求类型角色（我担心没有办法，因为文档提到类型类假定参数是名义上的）

所以我的问题是，有没有办法让强制在这种情况下工作，如果没有，是否有任何深层原因为什么不这样做，或者这只是当前角色推理实现的限制。我的幼稚观点使我相信类型类可以对参数的角色施加约束，而实例必须满足约束。是否有一些有用的强制技巧的好来源？

4

1 回答 1

1

实际上，g不要h进行类型检查，因为类型imap f不明确。

imap :: IFunctor f => (a ~> b) -> (f a ~> f b)

例如， in h,imap f被推断为以下类型，带有自由统一变量?f0, ?f1, ?i0：

h = coerce . (imap f :: ?f0 (IFix ?f1) ?i0 -> ?f0 (IFix ?f1) ?i0) . coerce

通常上下文允许我们实例化这些变量，但这里的上下文是：

coerce . _ . coerce

注意 的类型coerce :: Coercible a b => a -> b，就类型推断而言，它完全解耦了输入和输出类型。

我们可以使用扩展ScopedTypeVariables来注解imap f：

h :: forall f i. IFunctor f => IFix f i -> IFix f i
h = coerce . (imap f :: f (IFix f) i -> f (IFix f) i) . coerce

或专门coerce限制其形状：

type E a = a -> a

i :: IFunctor f => IFix f i -> IFix f i
i = (coerce :: E (f (IFix f) i) -> E (IFix f i)) (imap f)

coerce本身就太笼统了，所以必须添加这样的注释是很常见的。拥有一个常见专业库可能是值得的。

于 2018-10-02T14:42:32.747 回答