TypeLit à partir de l'expression générique Integer

Question

La seule manière que je connaisse pour construire un Nat consiste à utiliser -XDataKinds avec des entiers promus, c'est-à-dire type MyInt = 10 :: Nat.

Au lieu de cela, je voudrais avoir une fonction

foo :: Integer -> Integer 

que je peux avec un indice réfléchi Nat, puis réifier le résultat. Pour démontrer ce que je veux dire, supposons une certaine fonction mkNat :: Integer -> Q Type. Je veux écrire

type Z = $(mkNat $ foo $ natVal (Proxy::Proxy 10)) 

(Dans mon exemple, foo est assez rapide qu'il peut être calculé au moment de la compilation sans frais généraux prohibitifs.) Avoir cette capacité me permet d'économiser le processus en plusieurs étapes de l'exécution foo dans un GHCi séparé session, puis en copiant la représentation décimale du résultat dans un fichier source, puis en compilant le code que je voulais vraiment.

Bien sûr, le seul composant manquant est mkNat. Si j'écris mon propre type de données personnalisé, l'équivalent de mkNat est facile à écrire. Mais j'aimerais vraiment utiliser les TypeLits intégrés. Y a-t-il des TemplateHaskell (ou des singletons, ou d'autres éléments magiques) qui me permettraient de réifier une expression Integer arbitraire en Nat?

Answer 1

Oui!

{-# LANGUAGE DataKinds  #-} 
{-# LANGUAGE TemplateHaskell #-} 

module Main where 

import Data.Proxy 
import GHC.TypeLits 
import Splices 

type Z = $(mkNat $ natVal (Proxy :: Proxy 10)) 

Et puis:

module Splices where 

import Language.Haskell.TH 

mkNat :: Integer -> Q Type 
mkNat = return . LitT . NumTyLit