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]
È 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
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.) –
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