模式同义词与正常模式不同

Question

函数f在以下代码中输入签名，该代码使用带有框架和乙烯基的单例：

：

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)

错误是调用rhead中的Couldn't match type ‘rs1’ with ‘'[s2 :-> t1] - 基本上，模式匹配似乎没有像我期望的那样绑定RS1的结构。但是，如果我插入模式，则类型检查：

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

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

Answer 1

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

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

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

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