Idiomatische Boolesche Gleichheitsverwendung (Singletons)

Question

Ich möchte eine Datenstruktur erstellen, um Elemente zu speichern, die auf Typebene mit Symbol gekennzeichnet sind. Dies:

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 

irgendwie funktioniert, wenn man die Tatsache vernachlässigen, dass Compiler warnt mich nicht liefern from' _ Nil Definition (? Warum tut es, nebenbei bemerkt ist es eine Möglichkeit, es stoppen zu machen?) Aber was ich wirklich wollte Am Anfang war es, Singletons-Bibliothek in idiomatischer Weise zu verwenden, anstatt meinen eigenen Code auf Typenebene zu schreiben. So etwas wie das:

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) = ??? 

Leider konnte ich nicht herausfinden, wie man den Kontext in eine propositionale Gleichheit umwandeln kann. Wie können Sie Bausteine ​​aus der Singletons-Bibliothek verwenden, um das zu tun, was ich versuche?

ghc@7.10.3, singletons@2.1

Answer 1

Don't use Booleans! Ich scheine keeprepeatingmyself zu diesem Punkt: Booleans sind von extrem begrenzter Nützlichkeit in abhängiger Programmierung und je früher Sie die Gewohnheit lernen, desto besser.

Ein Elem s ss ~ True Kontext verspricht Ihnen, dass s in ss irgendwo, aber es sagt nicht wo. Dies lässt Sie im Stich, wenn Sie einen s-Wert aus Ihrer Liste ss produzieren müssen. Ein Bit ist nicht genug Informationen für Ihre Zwecke.

Vergleichen Sie dies mit der Rechenleistung Ihres ursprünglichen HasElem Typs, der wie eine natürliche Zahl strukturiert ist und den Index des Elements in der Liste angibt. (Vergleichen Sie die Form eines Werts wie There (There Here) mit der von S (S Z).) Um einen s aus einer Liste von ss zu erzeugen, müssen Sie nur den Index dereferenzieren.

Das heißt, Sie noch in der Lage sein sollte, die Sie entfernt einen HasElem x xs Wert aus einem Kontext von Elem x xs ~ True warf Informationen wiederherzustellen und extrahieren. Es ist langweilig, obwohl - Sie müssen die Liste für den Artikel (, die Sie bereits getan haben, um Elem x xs zu bewerten!) Und die unmöglichen Fälle zu beseitigen suchen. Arbeiten in Agda (Definitionen weggelassen):

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 diese Arbeit ist jedoch unnötig. Verwenden Sie einfach den informationsreichen Proof-Term für den Anfang.

---

By the way, sollten Sie in der Lage sein GHC zu stoppen Ihnen unvollständiges Muster Warnung von Ihrem Elem Matching auf der linken Seite zu tun, anstatt in einem case -Ausdrucks:

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

von Wenn Sie sich auf der rechten Seite einer Definition befinden, ist es für die Mustererkennung zu spät, um die möglichen Konstruktoren für andere Begriffe auf der linken Seite zu verfeinern.