Comment capturer une variable de type dans une citation TemplateHaskell

Question

J'essaie d'écrire une instance Lift qui soulève non seulement le constructeur, mais également ses variables de type. Par exemple, prenez Proxy a. J'ai besoin d'une Liftinstance telle que, lorsqu'elle lift (Proxy @Int)est épissée, GHC infère correctement que l'expression générée est un Proxy Int.

-- GHC should infer that x :: Proxy Int
x = $(TH.lift (Proxy @Int))

J'ai essayé ceci:

instance Lift (Proxy a) where
  lift _ = [|Proxy @a|]

x = $(TH.lift (Proxy @Int))

Il semble TH capturé aet pas Intcomme prévu. Je ne sais pas quoi essayer d'autre

/.../TH/Test.hs:15:7: error:
    • The exact Name ‘a’ is not in scope
        Probable cause: you used a unique Template Haskell name (NameU), 
        perhaps via newName, but did not bind it
        If that's it, then -ddump-splices might be useful

Answer 1

template-haskell ne semble rien fournir de tel. Mais il existe peut-être une solution que vous pouvez mettre en œuvre à partir de zéro. L'idée est de définir une classe pour porter une citation représentant chaque type:

class TLift a where
  tlift :: Q Type

Par exemple:

instance TLift Int where
  tlift = [t|Int|]

-- and so on

Puis pour définir un devis avec une application de type:

proxyQ :: forall a. TLift a => Q Exp
proxyQ = [|Proxy @( $(tlift @a) )|]

Une limitation ici est que les TLiftinstances ne peuvent produire des guillemets que pour des types complètement concrets, pas de variables de type. Peut-être que la réflexion peut contourner cela.

Answer 2

Je suis presque sûr que cela ne peut pas être fait avec une référence directe au type afin d'utiliser des applications de type. Au moment où le code épissé fait référence à a, la portée dans laquelle il a été défini n'existe plus.

Mais je pense que c'est l'un des problèmes connus qui a conduit à la création du modèle typé Haskell. Et cela peut être utilisé pour résoudre ce problème. Notez que GHC 8.10 a introduit une entrée supplémentaire dans la classe liftTyped, qui peut résoudre ce problème directement. Mais il fournit également l'indication nécessaire pour l'utiliser sur les versions antérieures de GHC, c'est-à-dire lift x === unTypeQ (liftTyped x).

À partir de là, j'ai pu voir comment écrire une instance de Liftfor Proxy apour les versions de GHC antérieures à 8.10.

instance Lift (Proxy a) where
    lift x = unTypeQ (helper x)
      where
        helper :: Proxy b -> Q (TExp (Proxy b))
        helper _ = [|| Proxy ||]

Pour GHC 8.10, ce serait juste

instance Lift (Proxy a) where
    liftTyped _ = [|| Proxy ||]

Honnêtement, il y a un tas d' Liftexemples apparemment manquants. Ce n'est que l'un des plus indirects à écrire, du moins avant GHC 8.10.