Typ sichere Lookup auf heterogene Listen in Haskell

Question

Ich möchte eine Art sichere Lookup-Funktion für die folgenden Datentypen entwickeln:

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' 

wo Lookup:

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

Die offensichtliche Lookup-Funktion sein würde, Typ Familie ist in Singletons-Bibliothek definiert. Diese Definition versagt Überprüfung GHC 7.10.3 mit der folgenden Fehlermeldung eingeben:

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 

Diese Nachricht ist für den rekursiven Aufruf lookupAttr s env' erzeugt wird. Dies ist sinnvoll, da wir, dass, wenn

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

hält, und

s :~: s' 

ist nicht beweisbar, dann

Lookup s env ~ 'Just t 

muss halten. Meine Frage ist, wie kann ich Haskell Typ Checker überzeugen, dass dies tatsächlich wahr ist?

Answer 1

Lookup ist in Bezug auf :== Gleichheit definiert, die von here kommt. Grob gesagt, ist Lookup auf diese Weise umgesetzt:

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 auf sameSymbol s s' uns nicht geben keine Informationen über Lookup s env, und lassen Sie nicht GHC es reduzieren. Wir müssen über s :== s' wissen, und dafür müssen wir die singleton version von :== verwenden.

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' 

Im Allgemeinen sollten Sie nicht KnownSymbol verwenden, sameSymbol oder irgendwelche von dem Zeug in GHC.TypeLits, weil sie zu „low-level“ sind und spielen nicht mit singletons standardmäßig zusammen.

Natürlich können Sie Ihre eigenen Lookup und andere Funktionen schreiben, und müssen nicht die singletons Importe verwenden; Entscheidend ist, dass Sie die Termebene und die Typebene synchronisieren, sodass die Mustererkennung auf Termebene relevante Informationen für die Typstufe liefert.