タイプ一覧

Question

から定期的にリストを取得する私はあなたが以下のコードで見ることができるようProxyとnatValを使用してIntegerにNatを変換する方法見つけた：

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

は、どのように私は、通常のリストにタイプリストを変換することができますか？

Answer 1

答えは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と同じ形を取ります。

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

：あなたの最初のコードにこれらの変更で

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

スプライシングは、私が期待される出力を得ます