haskell - 在 Haskell 中对异构列表进行类型安全查找

Question

我想为以下数据类型开发一个类型安全的查找函数:

data Attr (xs :: [(Symbol,*)]) where
   Nil  :: Attr '[]
   (:*) :: KnownSymbol s => (Proxy s, t) -> Attr xs -> Attr ('(s , t) ': xs)

显而易见的查找功能如下:

 lookupAttr :: (KnownSymbol s, Lookup s env ~ 'Just t) => Proxy s -> Attr env -> t
 lookupAttr s ((s',t) :* env')
       = case sameSymbol s s' of
            Just Refl -> t
            Nothing   -> lookupAttr s env'

在哪里 Lookup类型族在单例库中定义。此定义无法在 GHC 7.10.3 上进行类型检查，并显示以下错误消息:

 Could not deduce (Lookup s xs ~ 'Just t)
   from the context (KnownSymbol s, Lookup s env ~ 'Just t)
      bound by the type signature for
             lookupAttr :: (KnownSymbol s, Lookup s env ~ 'Just t) =>
                           Proxy s -> Attr env -> t

此消息是为递归调用 lookupAttr s env' 生成的.这是合理的，因为我们有如果

Lookup s ('(s',t') ': env) ~ 'Just t

持有，并且

s :~: s'

无法证明，那么

Lookup s env ~ 'Just t

必须持有。我的问题是，我怎样才能让 Haskell 类型检查器相信这确实是真的？

Answer 1

Lookup 定义为 :==平等，来自here .粗略地说，Lookup以这种方式实现:

type family Lookup (x :: k) (xs :: [(k, v)]) :: Maybe v where
  Lookup x '[] = Nothing
  Lookup x ('(x' , v) ': xs) = If (x :== x') (Just v) (Lookup x xs)

sameSymbol s s' 上的模式匹配没有给我们任何关于 Lookup s env 的信息，并且不会让 GHC 减少它。我们需要了解 s :== s' ，为此我们需要使用 singleton version的 :== .

data Attr (xs :: [(Symbol,*)]) where
   Nil  :: Attr '[]
   (:*) :: (Sing s, t) -> Attr xs -> Attr ('(s , t) ': xs)

lookupAttr :: (Lookup s env ~ 'Just t) => Sing s -> Attr env -> t
lookupAttr s ((s', t) :* env') = case s %:== s' of
  STrue  -> t
  SFalse -> lookupAttr s env'

一般来说，你不应该使用 KnownSymbol , sameSymbol , 或 GHC.TypeLits 中的任何内容因为他们太“低级”了，不配合 singletons默认。

当然你也可以自己写 Lookup等功能，无需使用 singletons进口；重要的是您同步术语级别和类型级别，以便术语级别模式匹配产生类型级别的相关信息。