惯用布尔等式用法(单例)

Question

我想创建一个数据结构来存储使用Symbol标记在类型级别的项目.这个:

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,singleletons@2.1

Answer 1

不要使用布尔人!我似乎在这一点上不断 重复 自己:布道在依赖类型编程中的用处非常有限,越早你越不习惯这种习惯.

一个Elem s ss ~ True上下文承诺s在ss某个地方,但它没有说明在哪里.当你需要s从你的列表中产生一个值时,这会让你陷入困境ss.一点不足以满足您的目的.

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

也就是说,您仍然可以恢复您丢弃的信息并HasElem x xs从上下文中提取值Elem x xs ~ True.但这很乏味 - 您必须在列表中搜索该项目(您已经为了评估而做了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在左侧进行匹配而不是在表达式中停止GHC警告你有关不完整模式case的信息:

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

当你在定义的右侧时,模式匹配为了改进左边其他术语的可能构造函数为时已晚.