2

函数 f 没有在以下代码中键入检查，它使用带有 Frames 和 Vinyl 的单例：

f :: forall rs1 rs2.  SList rs1 -> Frame (Record rs1) -> Int
f (OnlyRecord s1 t1) df1 = broadcast (*) (rhead <$> df1)

pattern OnlyRecord :: Sing s -> Sing t -> SList '[s :-> t]
pattern OnlyRecord sym typsing = SCons (SRecArrow sym typsing) SNil

rhead :: Record ((s :-> t) ': sstt) -> t
rhead (x :& xs) = getCol $ getIdentity x

data instance Sing (a :: Type) where
    SRecArrow :: Sing (s :: Symbol) -> Sing (t :: Type) -> Sing (s :-> t)

错误在于Couldn't match type ‘rs1’ with ‘'[s2 :-> t1]对 rhead 的调用——基本上，模式匹配似乎没有像我预期的那样绑定 rs1 的结构。但是如果我内联模式，它会输入检查：

f' :: forall rs1 rs2.  SList rs1 -> Frame (Record rs1) -> Int
f' (SCons (SRecArrow s1 t1) SNil) df1 = broadcast (*) (rhead <$> df1)

鉴于模式同义词应该是同义词，它不应该与内联模式相同吗？

4

1 回答 1

2

模式同义词的定义是正确的；这是错误的类型。正确的类型是

pattern OnlyRecord :: () => (rs ~ '[s :-> t]) => Sing s -> Sing t -> SList rs
pattern OnlyRecord ...

使用您的原始模式类型签名（相当于() => () => Sing s -> Sing t -> SList '[s :-> t]），您声称给定一个表达式x :: SList '[s :-> t]，您可以使用您的模式同义词匹配此表达式。但是， in f，您没有这样的表达式-您只有x :: SList rs1for some rs1，这严格来说是更一般的。使用正确的签名，您可以使用模式同义词来匹配这样的表达式，因为模式同义词被声明为适用于任何SList rs；然后提供的约束（即rs ~ '[s :-> t]）在模式匹配范围内可用。

有关模式签名的更多详细信息，请参阅GHC 用户指南。

于 2017-11-30T16:38:10.440 回答