2016-07-10 1 views
9

Desidero creare una struttura dati per archiviare gli elementi contrassegnati a livello di testo utilizzando Symbol. Questo:Utilizzo dell'uguaglianza booleana idiopatica (singleton)

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 

funziona un pò, se si trascura il fatto che compilatore mi avvisa di non fornendo from' _ Nil definizione (? Il motivo per cui lo fa, tra l'altro c'è un modo per farlo smettere?) Ma quello che ho veramente voluto all'inizio dovevo usare la libreria di singletons in modo idiomatico, invece di scrivere il mio codice a livello di codice. Qualcosa di simile a questo:

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

Purtroppo non riuscivo a capire come convertire il contesto per un'uguaglianza proposizionale. Come si possono usare i mattoncini della libreria di singletons per fare ciò che sto cercando di fare?

[email protected]10.3, [email protected]

+1

È possibile rimuovere l'avviso in 'from'' aggiungendo funzioni' storeHead :: Store e (s ': ss) -> es' e 'storeTail :: Store e (s': ss) -> Store e ss 'e li usa sullo store dopo aver abbinato' AtHead' o 'InTail'. – cchalmers

+1

Le due istanze di 'HasElemC' si sovrappongono.GHC troverà impossibile scaricare un vincolo 'HasElemC' perché non controlla le precondizioni quando esegue la ricerca di prove. Fortunatamente c'è [un trucco ben noto che utilizza famiglie di tipi e 'UndecidableInstances'] (https://wiki.haskell.org/GHC/AdvancedOverlap). (In effetti questo è uno dei pochi buoni usi delle famiglie di tipo booleano.) –

+0

Grazie, cchalmers, ha funzionato. Grazie, Benjamin. Le sovrapposizioni vanno bene nel mio caso: non ho bisogno di funzioni polimorfiche in ss. Anche se potrei averne bisogno in futuro. – NioBium

risposta

8

Don't use Booleans! Mi sembra di keeprepeatingmyself su questo punto: le booleane hanno un'utilità estremamente limitata nella programmazione tipizzata in modo dipendente e prima si disimpara l'abitudine e meglio è.

Un Elem s ss ~ True contesto promette a voi che s è in ss da qualche parte, ma non dice dove . Questo ti lascia in balia quando hai bisogno di produrre un valore s dal tuo elenco di ss. Un bit non è abbastanza informazioni per i tuoi scopi.

Confrontate questo con l'utilità computazionale del vostro tipo originale HasElem, che è strutturato come un numero naturale che fornisce l'indice dell'elemento nell'elenco. (Confrontare la forma di un valore come There (There Here) con quello di S (S Z).) Per produrre un s da un elenco di ss è sufficiente effettuare la dereferenziazione dell'indice.

Detto questo, si dovrebbe comunque essere in grado di recuperare le informazioni che hai buttato via e estrarre un valore HasElem x xs da un contesto di Elem x xs ~ True. È noioso, però - devi cercare nella lista l'oggetto (che hai già fatto per valutare Elem x xs!) Ed eliminare i casi impossibili. Lavorando in Agda (definizioni omesse):

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) 

Tuttavia, tutto questo lavoro non è necessario. Basta usare il termine di prova ricco di informazioni per iniziare.


A proposito, si dovrebbe essere in grado di fermare GHC che avvisa sui modelli incompleti facendo la vostra Elem corrispondente sul lato sinistro, piuttosto che in un 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 Nel momento in cui sei sul lato destro di una definizione, è troppo tardi per la corrispondenza del modello per perfezionare i possibili costruttori per gli altri termini sulla sinistra.

+0

Grazie. Stavo solo cercando di non inventare la ruota. Sperando ancora che qualcuno possa fornire una soluzione nei singleton di Haskell, se ne esiste uno. Qual è il punto nel sollevare tutte queste funzioni a livello di testo, se non è possibile utilizzarle nelle dimostrazioni? – NioBium

+0

Bene, i singleton sono (e 'singletons' è) una particolare modalità di utilizzo di GADT e tipi di dati. Termini di prova come "Elem" sono un altro. Non si inseriscono naturalmente nella struttura singleton perché non sono singleton! –