惯用的布尔相等用法（单例）

Question

我想创建一个数据结构来存储使用符号在类型级别标记的项目。这个：

data Store e (ss :: [Symbol]) where
  Nil :: Store e '[]
  Cons :: e s -> Store e ss -> Store e (s ': ss)

data HasElem (a :: k) (as :: [k]) where
  AtHead :: HasElem a (a ': as)
  InTail :: HasElem a as -> HasElem a (b ': as)

class HasElemC (a :: k) (as :: [k]) where hasElem :: HasElem a as
instance HasElemC {OVERLAPPING} a (a ': as) where hasElem = AtHead
instance HasElemC a as => HasElemC a (b ': as) where hasElem = InTail hasElem

from :: HasElemC s ss => Store e ss -> e s
from = from' hasElem

from' :: HasElem s ss -> Store e ss -> e s
-- from' _ Nil = undefined
from' h (Cons element store) = case h of
  AtHead -> element
  InTail h' -> from' h' store

有点工作，如果你忽略编译器警告我没有提供 from' _ Nil 定义的事实（为什么它，顺便说一句？有没有办法让它停止？）但我真正想做的是开始是以惯用的方式使用单例库，而不是编写我自己的类型级代码。像这样的：

import Data.Singletons.Prelude.List

data Store e (ss :: [Symbol]) where
  Nil :: Store e '[]
  Cons :: Sing s -> e s -> Store e ss -> Store e (s ': ss)

from :: Elem s ss ~ True => Store e ss -> e s
from (Cons evidence element nested) = ???

遗憾的是，我无法弄清楚如何将上下文转换为命题相等。你如何使用单例库中的构建块来做我想做的事情？

ghc@7.10.3, singletons@2.1

Answer 1

Don't use Booleans!在这一点上，我似乎 keep repeating myself：布尔值在依赖类型编程中的用处极其有限，越早摆脱这种习惯越好。

Elem s ss ~ True 上下文向您保证s 位于ss 某处，但它没有说明在哪里。当您需要从ss 列表中生成s-值时，这会让您陷入困境。一点信息不足以满足您的目的。

将此与原始 HasElem 类型的计算有用性进行比较，该类型的结构类似于一个自然数，给出了列表中元素的索引。 （比较There (There Here) 与S (S Z) 之类的值的形状。）要从ss 列表中生成s，您只需取消引用索引。

也就是说，您应该仍然能够恢复您丢弃的信息并从Elem x xs ~ True 的上下文中提取HasElem x xs 值。不过，这很乏味 - 您必须在列表中搜索该项目（您已经这样做了以评估Elem x xs！）并消除不可能的情况。在 Agda 中工作（省略定义）：

recover : {A : Set}
          (_=?_ : (x : A) -> (y : A) -> Dec (x == y))
          (x : A) (xs : List A) ->
          (elem {{_=?_}} x xs == true) ->
          Elem x xs
recover _=?_ x [] ()
recover _=?_ x (y :: ys) prf with x =? y
recover _=?_ x (.x :: ys) prf | yes refl = here
recover _=?_ x (y :: ys) prf | no p = there (recover _=?_ x ys prf)

不过，所有这些工作都是不必要的。只需使用信息丰富的证明术语即可。

---

顺便说一句，您应该能够通过在左侧进行Elem 匹配而不是在case-表达式中进行匹配，从而停止 GHC 警告您有关不完整模式的警告：

from' :: HasElem s ss -> Store e ss -> e s
from' AtHead (Cons element store) = element
from' (InTail i) (Cons element store) = from' i store

当您位于定义的右侧时，模式匹配为左侧的其他术语细化可能的构造函数为时已晚。