获得常规列表从类型列表

问题描述：

我已经找到一种方法来一个Nat转换成Integer使用Proxy和natVal，你可以在下面的代码中看到：获得常规列表从类型列表

{-# 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

但我不能想直截了当地列表类型转换为常规列表，下面的代码甚至不类型检查：

{-# 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

我如何转换列表类型为常规列表？

答

答案是做类似KnownNat但类型级别列表Nat。我们继续使用类型类在类型级别列表中进行归纳。这个类型类通过它的超类约束将检查你列表中的所有元素是否满足KnownNat，然后它将使用该事实来重构术语级列表。

{-# 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)

然后，fromListNat采用相同的形状fromNat：这些变化对你的初始代码

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

拼接，我得到的预期输出：

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

获得常规列表从类型列表

相关推荐