在Haskell的异类列表中键入安全查找

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

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'生成lookupAttr s env' 。 这是合理的，因为我们有如果

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

持有和

s :~: s'

那么不可证明

Lookup s env ~ 'Just t

必须持有。 我的问题是，我怎么能说服Haskell类型检查器这确实是真的？

---

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

链接地址: http://www.djcxy.com/p/91803.html

上一篇: Type safe lookup on heterogeneous lists in Haskell

下一篇: Why does my AdaptiveTrigger fire when I change the theme settings?