使用名义角色进行类型推断

Using Nominal Roles for Type Inference

我有一个 newtype 的幻影类型,但我无法轻松使用它。

考虑以下示例:

import Data.Coerce

newtype F a b = F b

myzip :: (Num b) => F a b -> F a b
myzip = (coerce (+)) myf

myf :: F a b
myf = undefined

GHC 抱怨它 Couldn't match representation of type ‘a0’ with that of ‘Int’。基本上,coerce (+)的类型是F a0 -> F a -> F a,而不是我想要的类型,即F a -> F a -> F a.

考虑到 a 目前的角色 phantom,这是合理的。我想知道是否有一种简单的方法可以通过其他方法进行类型推断(我不想写出签名,这就是我首先使用 coerce 的原因!)。 特别是,我希望如果我将参数 a 的作用限制为名义上的,那么 GHC 将能够判断出签名的唯一可能选择是我想要的那个。没有这样的运气:GHC 给出了同样的错误。

如果重要的话,在我的真实代码中 a 的角色必须至少是代表性的,而 b 必须是名义上的。

让我们从几种类型开始:

coerce (+) :: (Num n, Coercible (n -> n -> n) b) => b
myf :: F c d

第一个问题是 GHC 没有希望确定 n 所以它可以选择 (+) 的实现。

让我们看看如果我们使用作用域类型变量来尝试一个简单的解决方案会发生什么:

myzip :: forall a b . Num b => F a b -> F a b
myzip = coerce ((+) :: b -> b -> b) myf

这不被接受。为什么?因为myf的类型有歧义!如果我们用另一个参数扩展 myzip,我们可以更清楚地看到这一点:

myzip x = coerce ((+) :: b -> b -> b) myf x

Coercible 与类型构造函数(在本例中为 ->)一起工作的方式来看,我们可以将所有内容排列起来并得出结论,myf 的类型必须可以用 b,其中 x :: F a b。但是在这种情况下 myf 的类型是不明确的。因此,GHC 无法 select bmyf 类型之间的适当 Coercible 实例。因为 coerce 实际上是引擎盖下的恒等函数,所以 选择哪个并不重要 ,但是 GHC 根本不会根据模棱两可的类型变量选择实例.要完成这项工作,您需要

myzip :: forall a b . Num b => F a b -> F a b
myzip = (coerce ((+) :: b -> b -> b)) (myf :: F a b)

输入角色

类型角色不能(至少目前)以任何方式指导实例解析。他们所能做的就是确定 Coercible 个实例是 生成的 。鉴于

class c => X d

GHC 将得出 X d 蕴含 c 的结论。但鉴于

instance c => X d

GHC 将不会得出X d蕴含c的结论。我不确定原因的细节,但情况一直如此。