टाइप स्तर सूची को एक मान

Question

मॉड्यूल GHC.TypeLits वर्तमान में natVal और symbolVal प्रदान करता है, जो हमें Nat या Symbol प्रकार से रनटाइम मान प्राप्त करने की अनुमति देता है। [String] प्रकार के रनटाइम मान को '[Symbol] के प्रकार से बाहर करने का कोई तरीका है? मुझे ऐसा करने का एक स्पष्ट तरीका नहीं दिख रहा है। मैं उस व्यक्ति के बारे में सोच सकता हूं जो OverlappingInstances के साथ टाइपक्लास का उपयोग करता है, लेकिन ऐसा लगता है कि जीएचसी के पास पहले से ही एक फ़ंक्शन होना चाहिए।

Answer 1

symbolVal टाइप स्तर सूचियों पर मैप किया जा सकता है। ऐसा करने के लिए हमें DataKinds और TypeOperators के अतिरिक्त ScopedTypeVariables और PolyKinds की आवश्यकता होगी।

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE PolyKinds #-} 

import Data.Proxy 
import GHC.TypeLits 

हम (किसी भी तरह के) जिसके लिए हम "प्रकार [String] के क्रम मूल्य प्राप्त" कर सकते हैं प्रकार के वर्ग में परिभाषित किया जाएगा।

class SymbolVals a where 
    symbolVals :: proxy a -> [String] 

हम किसी भी खाली सूची के लिए तारों की एक सूची प्राप्त कर सकते हैं।

instance SymbolVals '[] where 
    symbolVals _ = [] 

हम प्रकार जहाँ हम पहले प्रकार और शेष के लिए स्ट्रिंग की एक सूची के लिए एक स्ट्रिंग प्राप्त कर सकते हैं की किसी भी सूची के लिए स्ट्रिंग की एक सूची प्राप्त कर सकते हैं।

instance (KnownSymbol h, SymbolVals t) => SymbolVals (h ': t) where 
    symbolVals _ = symbolVal (Proxy :: Proxy h) : symbolVals (Proxy :: Proxy t) 

Answer 2

मैं singletons लाइब्रेरी का उपयोग करने का सुझाव देता हूं। -> HList XS -> [स्ट्रिंग] `या` forall (

$ stack ghci --package singletons 
Configuring GHCi with the following packages: 
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help 
Prelude> :set -XDataKinds 
Prelude> import Data.Singletons.Prelude 
Prelude Data.Singletons.Prelude> fromSing (sing :: Sing '["a","b"]) 
["a","b"] 
Prelude Data.Singletons.Prelude> :t fromSing (sing :: Sing '["a","b"]) 
fromSing (sing :: Sing '["a","b"]) :: [String]