Obtenir une liste régulière à partir d'une liste des types

Question

J'ai trouvé un moyen de convertir un Nat en un Integer en utilisant Proxy et natVal comme vous pouvez le voir dans le code ci-dessous:

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 

module Main where 

import Data.Proxy (Proxy) 
import Data.Monoid ((<>)) 
import GHC.TypeLits 

main :: IO() 
main = do 
    fromNat (undefined :: Proxy 5) 

fromNat :: KnownNat n => Proxy n -> IO() 
fromNat proxy = do 
    let (num :: Integer) = natVal proxy -- converting a Nat to an Integer 
    putStrLn $ "Some num: " <> show num 

Mais je ne suis pas en mesure de penser d'une manière simple de convertir une liste de type dans une liste régulière, le code ci-dessous ne tapez même pas vérifier:

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 

module Main where 

import Data.Proxy (Proxy) 
import Data.Monoid ((<>)) 
import GHC.TypeLits 

main :: IO() 
main = do 
    fromNat  (undefined :: Proxy 5) 
    fromListNat (undefined :: Proxy '[2,3,10]) 

fromNat :: KnownNat n => Proxy n -> IO() 
fromNat proxy = do 
    let (num :: Integer) = natVal proxy -- converting a Nat to an Integer 
    putStrLn $ "Some num: " <> show num 

fromListNat :: Proxy [Nat] -> IO() 
fromListNat = undefined 

Comment puis-je convertir une liste de type dans une liste régulière?

Answer 1

La réponse est de faire quelque chose comme KnownNat mais pour les listes de niveau de type de Nat. Nous procédons par induction sur la liste de niveau de type, en utilisant une classe de type. Ce type de classe, à travers ses contraintes de superclasse, vérifiera que tous les éléments de votre liste satisfont KnownNat et ensuite il utilisera ce fait pour reconstruire une liste de niveau terme.

{-# LANGUAGE TypeOperators, KindSignatures #-} 

-- Similar to `KnownNat (n :: Nat)` 
class KnownNatList (ns :: [Nat]) where 
    natListVal :: proxy ns -> [Integer] 

-- Base case 
instance KnownNatList '[] where 
    natListVal _ = [] 

-- Inductive step 
instance (KnownNat n, KnownNatList ns) => KnownNatList (n ': ns) where 
    natListVal _ = natVal (Proxy :: Proxy n) : natListVal (Proxy :: Proxy ns) 

Ensuite, fromListNat prend la même forme que fromNat:

fromListNat :: KnownNatList ns => Proxy ns -> IO() 
fromListNat proxy = do 
    let (listNum :: [Integer]) = natListVal proxy 
    putStrLn $ "Some list of num: " <> show listNum 

Splicing dans ces changements à votre code initial, je reçois la sortie attendue:

$ ghc Main.hs 
$ ./Main 
Some num: 5 
Some list of num: [2,3,10]