2

我使用乙烯基来声明许多不同的记录类型，其中一些有一个名为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？

4

1 回答 1

2

编辑：@Koterpillar 的测试文件似乎表明这种类型的同义词不能按我预期的方式工作；看来约束在定义中不可用。值得调查或跟进问题以确定原因。我的理解(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见证两件不同的事情：即Contentin fs，并且类型参数c等于Rec Attr fs。

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

您的类型族解决方案无济于事，但出于不同的原因。在 的定义中getContent，编译器需要证明a确实是Rec Attr rs0为了使用rlens（或可能unAttr），但它不能从类型族中推断出这一点。（您知道只有一种类型实例，但编译器不使用该逻辑。）

于 2015-03-05T00:37:30.413 回答