haskell - 声明适用于具有特定字段的 Vinyl 记录的约束

Question

我使用vinyl声明许多不同的记录类型，其中一些记录类型具有名为 Content 且具有特定类型 LanguageContent 的字段。对于依赖于记录中存在的字段的函数，我想要一个如下类型:

getContent :: HasContent a => a -> LanguageContent
getContent a = a ^. rlens SContent . unAttr

(给出的函数仅供说明之用；有许多函数采用 HasContent 的内容并用它做不同的事情。)

现在我只需要将 HasContent 声明为约束。我可以使用 Data.Vinyl.Notation 得到的最接近的是:

getContent :: (Content ∈ fs) => Rec Attr fs -> LanguageContent

可以声明类型族，但函数不会进行类型检查:

type family HasContent c :: Constraint
type instance HasContent (Rec Attr rs) = Content ∈ rs

getContent :: HasContent a => a -> LanguageContent
getContent a = a ^. rlens SContent . unAttr

Could not deduce (a ~ Rec Attr rs0)
from the context (HasContent a)

我可以使用两个参数进行约束，这两个参数可以工作，但并不理想(rs 是我必须在各处重复的参数):

type HasContent c rs = (c ~ Rec Attr rs, Content ∈ rs)

如果没有额外的参数(请参阅@ChristianConkle的回答)，我只会得到:

type HasContent c = (c ~ Rec Attr rs, Content ∈ rs)

Not in scope: type variable ‘rs’

如何声明一个仅适用于 Rec Attr fs 且 Content ∈ fs 的约束？

Answer 1

编辑:@Koterpillar's test file似乎表明这种类型的同义词并不按我预期的方式工作；看来该约束在定义内不可用。值得进行调查或提出后续问题来确定原因。我的理解是 (C x => T x) -> Y 相当于 C x => T x -> Y，但事实上该示例不起作用似乎证明了这一点。 /编辑

我想你想写这个:

type RecWithContent rs = Content ∈ rs => Rec Attrs rs

getContent' :: RecWithContent rs -> LanguageContent

这实际上只是将约束包装在类型同义词中。您需要 RankNTypes 以及可能还有一堆其他扩展。

您现有的尝试解决问题并在 => 右侧仅留下 a 可以归结为以下类型同义词:

type HasContent c = (Content ∈ fs, c ~ Rec Attr fs)

换句话说，您希望 HasContent 见证两个不同的事情:Content 位于 fs 中，以及类型参数 c 等于Rec Attr fs。

我认为您无法以您方便的方式执行此操作。对于类型同义词，表面层问题是 rs 不在右侧的范围内。更深层次的问题是你要求编译器弥补fs;你想写类似 exists fs. (Content ∈ fs, c ~ Rec Attr fs)，在当前的 Haskell 中无法直接表达。

您的类型系列解决方案不会有帮助，但原因不同。在 getContent 的定义中，编译器需要证明 a 确实是 Rec Attr rs0 才能使用 rlens (或者可能是 unAttr)，但它无法从类型系列中推断出这一点。 (您知道只有一种类型实例，但编译器不使用该逻辑。)