Rodzaj bezpieczne wyszukiwanie na heterogenicznych list w Haskell

Question

Chcę rozwijać funkcję typu bezpieczny odnośników dla następującego typu danych:

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

Funkcja Lookup oczywiste byłoby jak:

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' 

gdzie Lookup rodzina typów jest zdefiniowana w bibliotece singletons. Definicja ta nie typ kontroli na GHC 7.10.3 z następującym komunikatem o błędzie:

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 

Ten komunikat jest generowany dla rekurencyjnego wywołania lookupAttr s env'. Jest to uzasadnione, ponieważ mamy, że jeśli

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

trzyma i

s :~: s' 

nie jest do udowodnienia, a następnie

Lookup s env ~ 'Just t 

musi posiadać. Moje pytanie brzmi: jak mogę przekonać sprawdzacz typu Haskella, że ​​to prawda?

Answer 1

Lookup jest zdefiniowany w kategoriach równości :==, która pochodzi z here. Z grubsza, Lookup jest realizowany w ten sposób:

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) 

dopasowanie Wzór na sameSymbol s s' nie daje nam żadnych informacji o Lookup s env i nie pozwól GHC je zmniejszyć. Musimy wiedzieć o s :== s', a do tego musimy użyć singleton version z :==.

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' 

Generalnie nie powinno się używać KnownSymbol, sameSymbol lub którykolwiek z tych rzeczy w GHC.TypeLits ponieważ są one zbyt „low-level”, a nie grać razem z singletons domyślnie.

Oczywiście można pisać własne Lookup i inne funkcje, i nie trzeba korzystać z importu singletons; ważne jest, aby zsynchronizować poziom terminów i poziom typu, aby dopasowywanie wzorców na poziomie terminów generowało odpowiednie informacje na poziomie typu.