Tipo di ricerca sicura su liste eterogenee in Haskell

Question

voglio sviluppare una funzione di tipo di ricerca sicuro per i seguenti tipi di dati:

data Attr (xs :: [(Symbol,*)]) where 
    Nil :: Attr '[] 
    (:*) :: KnownSymbol s => (Proxy s, t) -> Attr xs -> Attr ('(s , t) ': xs) 

La funzione di ricerca ovvia sarebbe come:

lookupAttr :: (KnownSymbol s, Lookup s env ~ 'Just t) => Proxy s -> Attr env -> t 
lookupAttr s ((s',t) :* env') 
     = case sameSymbol s s' of 
      Just Refl -> t 
      Nothing -> lookupAttr s env' 

dove Lookup la famiglia di tipi è definita nella libreria di singleton. Questa definizione non riesce a digitare controllo sulla GHC 7.10.3 con il seguente messaggio di errore:

Could not deduce (Lookup s xs ~ 'Just t) 
    from the context (KnownSymbol s, Lookup s env ~ 'Just t) 
     bound by the type signature for 
      lookupAttr :: (KnownSymbol s, Lookup s env ~ 'Just t) => 
          Proxy s -> Attr env -> t 

Questo messaggio viene generato per la chiamata ricorsiva lookupAttr s env'. Questo è ragionevole, dal momento che abbiamo che se

Lookup s ('(s',t') ': env) ~ 'Just t 

stive, e

s :~: s' 

non è dimostrabile, allora

Lookup s env ~ 'Just t 

deve tenere. La mia domanda è, come posso convincere il correttore di tipo Haskell che questo è vero?

Answer 1

Lookup è definito in termini di uguaglianza :==, che viene da here. Approssimativamente, Lookup è implementato in questo modo:

type family Lookup (x :: k) (xs :: [(k, v)]) :: Maybe v where 
    Lookup x '[] = Nothing 
    Lookup x ('(x' , v) ': xs) = If (x :== x') (Just v) (Lookup x xs) 

pattern matching on sameSymbol s s' non ci dà alcuna informazione su Lookup s env, e non lo lascia GHC ridurlo. Dobbiamo sapere su s :== s' e per questo dobbiamo usare lo singleton version di :==.

data Attr (xs :: [(Symbol,*)]) where 
    Nil :: Attr '[] 
    (:*) :: (Sing s, t) -> Attr xs -> Attr ('(s , t) ': xs) 

lookupAttr :: (Lookup s env ~ 'Just t) => Sing s -> Attr env -> t 
lookupAttr s ((s', t) :* env') = case s %:== s' of 
    STrue -> t 
    SFalse -> lookupAttr s env' 

In generale, non si dovrebbe usare KnownSymbol, sameSymbol, o una qualsiasi delle cose in GHC.TypeLits perché sono troppo "a basso livello" e non giocano con singletons per impostazione predefinita.

Naturalmente, è possibile scrivere il proprio Lookup e altre funzioni e non è necessario utilizzare le importazioni singletons; ciò che conta è che sincronizzi il livello di termine e il livello di testo, in modo che la corrispondenza del modello a livello di termine generi informazioni rilevanti per il livello di tipo.