Type safe lookup on heterogeneous lists in Haskell

Question

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'

where 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

holds, and

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?

Where is sameSymbol defined? Is that from the singletons library as well? — Kwarrtz
When using strings to represent bound variables, you pay a significant price in the complexity of your language implementation. Capture-avoiding substitution and alpha-equivalence are both notoriously tricky to get right, not to mention the cost of battling with Symbol's rather janky implementation in GHC. If you're building a type-safe embedded DSL I think you should seriously consider HOAS as a simpler alternative. — Benjamin Hodgson

András Kovács András Kovács · Accepted Answer · 2016-05-21T10:23:18

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 KnownSymbol, 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.

Type safe lookup on heterogeneous lists in Haskell

1 Answers