Тип безопасный поиск гетерогенных списков в Haskell

Question

Я хочу разработать функцию типа безопасного подстановка для следующего типа данных:

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

Очевидная функция поиска будет, как:

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 тип семейства определяется в библиотеке одиночек. Это определение не удается ввести проверку на GHC 7.10.3 со следующим сообщением об ошибке:

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 

Это сообщение генерируется для рекурсивного вызова lookupAttr s env'. Это разумно, так как мы имеем, что если

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

держит, и

s :~: s' 

не доказуемо, то

Lookup s env ~ 'Just t 

должен держать. Мой вопрос: как я могу убедить проверку типа Haskell, что это действительно так?

Answer 1

Lookup определено в терминах :== равенство, которое исходит от here. Грубо говоря, Lookup реализуется следующим образом:

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) 

соответствие шаблона на sameSymbol s s' не дает нам никакой информации о Lookup s env, и не позволяет GHC уменьшить его. Нам нужно знать о s :== s', и для этого нам необходимо использовать 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' 

Как правило, вы не должны использовать KnownSymbol, sameSymbol, или любой материал, в GHC.TypeLits, потому что они слишком «низкий уровень» и не играть вместе с singletons по умолчанию.

Конечно, вы можете написать свой собственный Lookup и другие функции, и не нужно использовать импорт singletons; важно то, что вы синхронизируете уровень термина и тип уровня, так что соответствие шаблону уровня уровня создает релевантную информацию для уровня типа.