习惯用法布尔平等用法（单身人士） [英] Idiomatic boolean equality usage (singletons)

问题描述

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

  data Store e（ss :: [Symbol]）其中
 Nil :: Store e'[] 
缺点： - >存储e ss  - >存储e（s'：ss）
 
数据HasElem（a :: k）（as :: [k]）其中
 AtHead :: HasElem a（a'：as）
 InTail :: HasElem a as  - > HasElem a（b'：as）
 $ b $ class HasElemC（a :: k）（as :: [k]）其中hasElem :: HasElem a为
实例HasElemC {OVERLAPPING} a a'：as）where hasElem = AtHead 
 instance HasElemC a as => HasElemC a（b'：as）其中hasElem = InTail hasElem 
 
来自:: HasElemC s ss =>存储e ss  - > e s 
 from = from'hasElem 
 
 from':: HasElem s ss  - >存储e ss  - > 's 
  - 从'_无'=未定义
从'h（缺点元素商店）=案例h 
 AtHead  - >元素
 InTail h' - >从'h'存储
  

有点作品，如果你忽略了编译器警告我不提供 from'_Nil 定义（顺便说一句，为什么它有办法让它停下来？）但是我最开始想做的事情是使用单例图书馆的地道风格，而不是写我自己的类型级代码。例如：

$ p $ import Data.Singletons.Prelude.List

data Store e（ss： ：[Symbol]）其中
Nil :: Store e'[]
Cons :: Sing s - > e s - >存储e ss - >将e（s'：ss）

从:: Elem s ss〜True =>存储e ss - >来自（Cons证据元素嵌套）的e s
= ???


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

ghc@7.10.3，singletons@2.1

解决方案

不要使用布尔值！我似乎继续 重复 我自己关于这一点：布尔对于依赖类型编程的有用性极其有限，你越早学习这种习惯就越好。
$ b $ Elem s ss〜True context允诺你 s 位于 ss 某处，但并不表示 。当你需要从 ss 列表中产生一个 s -value时，这会让你陷入困境。有一点是没有足够的信息为您的目的。

比较这与您的原始 HasElem 类型的计算有用性，它的结构像一个给出列表中元素索引的自然数。 （比较 There（There Here）和 S（SZ）的值的形状。）从 ss 列表中添加一个 s ，您只需要取消索引。

也就是说，您仍应该能够恢复您丢弃的信息，并从中提取 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 
恢复_ =？_ x []（）
恢复_ =？_ x（y :: ys）prf with x =？ y 
恢复_ =？_ x（.x :: ys）prf | yes refl = here 
 recover _ =？_ x（y :: ys）prf |没有p =那里（恢复_ =？_ x ys prf）
  

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

---

顺便说一句，您应该能够阻止GHC通过在左侧执行 Elem 匹配而不是在情况下 -expression：

  from':: HasElem s ss  - >存储e ss  - >来自'（InTail i）（Cons元素店）='我店
  ' $ p> 
 
 
当你在定义的右边时，模式匹配为了改进左边其他项的可能构造函数已经太晚了。 / p> 
I want to create a data structure to store items tagged on type level using Symbol. This:
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
kinda works, if you neglect the fact that compiler warns me for not supplying from' _ Nil definition (why does it, by the way? is there a way to make it stop?) But what I really wanted to do in the beginning was to use singletons library in idiomatic fashion, instead of writing my own type-level code. Something like this:
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) = ???
Sadly I could not figure out how to convert the context to a propositional equality. How can you use building blocks from singletons library to do what I'm trying to do?

ghc@7.10.3, singletons@2.1
解决方案
Don't use Booleans! I seem to keep repeating myself on this point: Booleans are of extremely limited usefulness in dependently-typed programming and the sooner you un-learn the habit the better.

An Elem s ss ~ True context promises to you that s is in ss somewhere, but it doesn't say where. This leaves you in the lurch when you need to produce an s-value from your list of ss. One bit is not enough information for your purposes.

Compare this with the computational usefulness of your original HasElem type, which is structured like a natural number giving the index of the element in the list. (Compare the shape of a value like There (There Here) with that of S (S Z).) To produce an s from a list of ss you just need to dereference the index.

That said, you should still be able to recover the information you threw away and extract a HasElem x xs value from a context of Elem x xs ~ True. It's tedious, though - you have to search the list for the item (which you already did in order to evaluate Elem x xs!) and eliminate the impossible cases. Working in Agda (definitions omitted):
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)
All this work is unnecessary, though. Just use the information-rich proof-term to start with.



By the way, you should be able to stop GHC warning you about incomplete patterns by doing your Elem matching on the left hand side, rather than in a case-expression:
from' :: HasElem s ss -> Store e ss -> e s
from' AtHead (Cons element store) = element
from' (InTail i) (Cons element store) = from' i store
By the time you're on the right-hand side of a definition, it's too late for pattern-matching to refine the possible constructors for other terms on the left.

                        
这篇关于习惯用法布尔平等用法（单身人士）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！