Enter Safe Search for Heterogeneous Lists in Haskell

Question

I want to develop a safe type search function for the following data type:

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

An obvious search function would look like this:

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

where the Lookup type family is defined in the single library. This definition cannot enter the GHC 7.10.3 check with the following error message:

  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 

This message is generated to call lookupAttr s env' recursively. This is reasonable since we have that if

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

and

 s :~: s' 

not provable then

 Lookup s env ~ 'Just t 

. My question is: how can I convince a Haskell type check that this is really so?

Answer 1

Lookup defined in terms of equality :== , which comes from. Roughly, Lookup is implemented as follows:

 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) 

Comparing the templates on sameSymbol s s' does not give us any information about Lookup s env and does not allow GHC to reduce it. We need to know about s :== s' , and for this we need to use singleton version :== .

 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' 

As a rule, you should not use KnownSymbol , sameSymbol or any material in GHC.TypeLits , because they are too "low level" and do not play along with singletons by default.

Of course, you can write your own Lookup and other functions, and you don't need to use singletons import; what matters is that you synchronize the term level and level type so that matching the level level pattern creates relevant information for the type level.