I want to develop a type safe lookup function for the following data type:
data Attr (xs :: [(Symbol,*)]) where Nil :: Attr ' (:*) :: KnownSymbol s => (Proxy s, t) -> Attr xs -> Attr ('(s , t) ': xs)
The obvious lookup function would be like:
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'
Lookup type family is defined in singletons library. This definition fails to type check on GHC 7.10.3 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 for the recursive call
lookupAttr s env' . This is reasonable, since we have that if
Lookup s ('(s',t') ': env) ~ 'Just t
s :~: s'
isn't provable, then
Lookup s env ~ 'Just t
must hold. My question is, how can I convince Haskell type checker that this is indeed true?
Lookup is defined in terms of
:== equality, which comes from here. Roughly,
Lookup is implemented this way:
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' doesn't give us any information about
Lookup s env , and doesn't let GHC reduce it. We need to know about
s :== s' , and for that we need to use the singleton version of
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'
Generally, you shouldn't use
sameSymbol , or any of the stuff in
GHC.TypeLits because they're too "low-level" and don't play along with
singletons by default.
Of course, you can write your own
Lookup and other functions, and don't need to use the
singletons imports; what matters is that you synchronize term level and type level, so that term level pattern matching produces relevant information for type level.