在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是根据:==平等来定义的，它来自这里。大致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'，为此我们需要使用单例版本的:==.

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导入；重要的是同步术语级别和类型级别，以便术语级别模式匹配生成类型级别的相关信息。