타입 목록

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 

접합, 내가 예상 출력을 얻을