Comment créer une liste de niveaux de type avec des symboles pour tester une famille de types

Question

J'essaie d'en savoir plus sur la programmation au niveau type Haskell. J'ai écrit une petite fonction pour rechercher une clé, un symbole, dans une liste de niveau du type:

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 

import GHC.TypeLits 

type family Lookup (x :: k) (l :: [(k,v)]) :: k where 
    Lookup k ('(k,a) ': ls) = a 
    Lookup k ('(x,a) ': ls) = Lookup k ls 
    Lookup k '[]    = TypeError (Text "Key not found: ") 

GHC (8.0.1) compile cette fonction sans erreurs et maintenant je dois tester la fonction GHCi. Dans GHCi je définir les options:

:set -XDataKinds 
:set -XTypeOperators 

et essayez d'exécuter un premier test exemple:

:kind! Lookup "bar" '[("foo", Int), ("bar", String)] 

Les cordes "bar" et "foo" devrait être des chaînes de niveau Type aka Symbols.

GHC rejette mon petit cas de test avec:

<interactive>:1:14: error: 
    • Expected kind ‘[(Symbol, v0)]’, 
     but ‘'[("foo", Int), ("bar", String)]’ has kind ‘[*]’ 
    • In the second argument of ‘Lookup’, namely 
     ‘'[("foo", Int), ("bar", String)]’ 
     In the type ‘Lookup "bar" '[("foo", Int), ("bar", String)]’ 

La question est de savoir comment changer l'exemple de test, donc GHC acceptera.

Remarque: Ma fonction de niveau de type Lookup est dans sa première version, il se peut que ce soit faux, peut-être que je devrais utiliser CmpSymbol ou faire d'autres changements. Cependant, ceci est et non le sujet de cette question SO.

Answer 1

(k1, k2) est le type de paires d'éléments de type/genre k1 et k2 et '(a, b) est une paire plage-niveau de type (voir l'').

'(a, b) :: (k1, k2) with a :: k1 and b :: k2 

Fix:

Lookup "bar" '[ '("foo", Int), '("bar", String)]