慣用論理型等価使用法（シングルトン）

Question

シンボルを使用して型レベルでタグ付けされたアイテムを格納するデータ構造を作成したいとします。この：あなたはコンパイラがfrom' _ Nil定義（？？なぜそれが、やり方によって、それは止めるようにする方法があるん）しかし、私が本当に欲しかっを供給していないために私を警告しているという事実を無視した場合

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 

はちょっと、作品初めに自分の型レベルコードを書くのではなく、シングルトンライブラリを慣用的な方法で使用することでした。このような何か：

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！私はこの時点でkeeprepeatingmyselfのように思えます。ブーリアンは、依存型プログラミングでは非常に限られた有用性を持ち、より早く習慣を学ぶほど早くなります。

Elem s ss ~ Trueコンテキストはsがどこかssであることをあなたに約束したが、それは言いません。 ssのリストからs値を生成する必要があるとき、これは不安にあなたを残します。 1ビットはあなたの目的に十分な情報ではありません。

元の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) 

これらの作業はすべて必要ありません。情報豊富な校正用語を使い始めるだけです。

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

で：

ところで

---

、あなたはむしろcase - 式に比べて、左側にあなたのElemマッチングを行うことによって、不完全なパターンに関する警告GHCを停止することができるはずです定義の右側にいるときは、パターンマッチングでは、左側の他の用語に使用できるコンストラクタを絞り込むのが遅すぎます。