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

问题描述

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

  data Attr（xs :: [（ Symbol，*）]）其中
 Nil :: Attr'[] 
（：*）:: KnownSymbol s => （Proxy s，t） - > Attr xs  - > Attr（'（s，t）'：xs）
  

显而易见的查找函数如下所示：

  lookupAttr ::（KnownSymbol s，Lookup s env〜'Just t）=>代理s  - > Attr env  - > t 
 lookupAttr s（（s'，t）：* env'）
 = case $ s 
只是Refl  - > t 
 Nothing  - > lookupAttr s env'
  

其中查找类型系列在singletons库中定义。此定义无法在GHC 7.10.3上输入检查并显示以下错误消息：

$ p $ 无法推断（Lookup s xs〜'从上下文（KnownSymbol s，Lookup s env〜'Just t）
绑定

lookupAttr ::（KnownSymbol s，Lookup s env〜'Just t ）=>
代理服务器 - > Attr env - > t


这个消息是为递归调用 lookupAttr s env' code>。这是合理的，因为我们有如果



 查找s（'（s'，t'）'：env）〜'只要t 
  

成立，并且

<$ p $不可证明，那么 s：〜：s'


/ p>



  Lookup s env〜'Just t 
  

必须成立。我的问题是，我如何说服Haskell类型检查器确实是真的？

/hackage.haskell.org/package/singletons-2.1/docs/src/Data-Singletons-Prelude-List.htmlrel =nofollow> Lookup 是根据：== 相等来定义的，它来自。粗略地说， Lookup 以这种方式实现：

  type family Lookup（x :: x）（xs :: [（k，v）]）可能v其中
查找x'[] =无
查找x（'（x'，v）'：xs） = If（x：== x'）（Just v）（Lookup x xs）
  

模式匹配on sameSymbol s'不会提供任何有关 Lookup s env 的信息，并且不会让GHC减少它。我们需要知道 s：== s'，为此我们需要使用 singleton version of of ：= = 。

 数据Attr（xs :: [（Symbol，*）]）其中
 Nil :: Attr'[] 
（：*）::（Sing s，t） - > Attr xs  - > Attr（'（s，t）'：xs）
 
 lookupAttr ::（Lookup s env〜'Just t）=>唱歌 - > 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 imports;重要的是你同步术语级别和类型级别，以便术语级别模式匹配产生类型级别的相关信息。

I want to develop a type safe lookup function for the following data type:

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

The obvious lookup function would be like:

 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'

where Lookup type family is defined in singletons library. This definition fails to type check on GHC 7.10.3 with the following error message:

 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

This message is generated for the recursive call lookupAttr s env'. This is reasonable, since we have that if

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

holds, and

s :~: s'

isn't provable, then

Lookup s env ~ 'Just t

must hold. My question is, how can I convince Haskell type checker that this is indeed true?

解决方案

Lookup is defined in terms of :== equality, which comes from here. Roughly, Lookup is implemented this way:

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)

Pattern matching on sameSymbol s s' doesn't give us any information about Lookup s env, and doesn't let GHC reduce it. We need to know about s :== s', and for that we need to use the singleton version of :==.

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'

Generally, you shouldn't use KnownSymbol, sameSymbol, or any of the stuff in GHC.TypeLits because they're too "low-level" and don't play along with singletons by default.

Of course, you can write your own Lookup and other functions, and don't need to use the singletons imports; what matters is that you synchronize term level and type level, so that term level pattern matching produces relevant information for type level.

这篇关于在Haskell的异类列表中键入安全查找的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！