유형 수준 맵에서 추가 정보가있는 유형 수준 목록 꾸미기

Question

유형이 포함 된 이질적 목록이 포함 된 값 유형을 반영합니다. 내가 좋아하는 것 무엇

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeApplications #-} 

import GHC.Exts 
import GHC.TypeLits 

import Data.Proxy 

type family AllSatisfy (f :: k -> Constraint) (xs :: [k]) :: Constraint where 
    AllSatisfy f '[] =() 
    AllSatisfy f (x ': xs) = (f x, AllSatisfy f xs) 

data HList (as :: [*]) where 
    HNil :: HList '[] 
    HCons :: a -> HList as -> HList (a ': as) 

type family Keys (xs :: [(a, b)]) :: [a] where 
    Keys '[] = '[] 
    Keys ('(a, b) ': xs) = a ': Keys xs 

type family Values (xs :: [(a, b)]) :: [b] where 
    Values '[] = '[] 
    Values ('(a, b) ': xs) = b ': Values xs 

showHList :: AllSatisfy Show xs => HList xs -> [String] 
showHList HNil = [] 
showHList (HCons x xs) = show x : showHList xs 

인 식 레벨 연관리스트를 통해 몇 가지 추가 정보를 지정하면된다 할 수 있도록 : 나는 모든 종류의 만족을 제약 조건을 포함 것을 확인하여 문자열의 모든 요소를 ​​변환 할 수 있습니다 HList의 유형에 따라 색인화됩니다. 뭔가 같이 : 이제

showWithKey :: forall (keyMap :: [(*, Symbol)]) (b :: Symbol) (rest :: [(*, Symbol)]). 
       (AllSatisfy Show (Keys keyMap) 
       ,AllSatisfy KnownSymbol (Values keyMap) 
       ) => 
       Proxy keyMap -> HList (Keys keyMap) -> [(String, String)] 
showWithKey _ HNil = [] 
showWithKey _ (HCons (x :: a) (xs :: HList as)) = 
    let p = (Proxy @keyMap) :: Proxy ('(a, b) ': rest) 
    in (show x, symbolVal (Proxy @b)) : (showWithKey (Proxy @rest) xs) 

, 그것은 (Keys keyMap) 다음, keyMap 비어 있지 않은,하지만 GHC이 알아 낸 어려움을 겪고있는 경우 있는지 분명하다 :

Could not deduce: keyMap ~ ('(a, b) : rest) 
     from the context: (AllSatisfy Show (Keys keyMap), 
         AllSatisfy KnownSymbol (Values keyMap)) 
     bound by the type signature for: 
        showWithKey :: (AllSatisfy Show (Keys keyMap), 
            AllSatisfy KnownSymbol (Values keyMap)) => 
            Proxy keyMap -> HList (Keys keyMap) -> [(String, String)] 
     or from: Keys keyMap ~ (a : as) 
     bound by a pattern with constructor: 
        HCons :: forall a (as :: [ghc-prim-0.5.0.0:GHC.Types.*]). 
          a -> HList as -> HList (a : as), 
       in an equation for ‘showWithKey’ 
     ‘keyMap’ is a rigid type variable bound by 
     the type signature for: 
      showWithKey :: forall (keyMap :: [(ghc-prim-0.5.0.0:GHC.Types.*, 
              Symbol)]) (b :: Symbol) (rest :: [(ghc-prim-0.5.0.0:GHC.Types.*, 
                       Symbol)]). 
         (AllSatisfy Show (Keys keyMap), 
          AllSatisfy KnownSymbol (Values keyMap)) => 
         Proxy keyMap -> HList (Keys keyMap) -> [(String, String)] 
     Expected type: Proxy ('(a, b) : rest) 
     Actual type: Proxy keyMap 

내가 있도록이를 다시 작성할 수있는 방법 GHC 물건을 알아낼 수 있니?

Answer 1

user2407038이 말한 것에 대한 몇 가지 단서를 가지고, depMap 유형의 구체적인 표현을 작성한 다음 형식에서 최소한 단순하지 않지만 최소한 표준적인 값을 설명하는 유형 클래스를 작성했습니다.

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeApplications #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE AllowAmbiguousTypes #-} 

import GHC.Exts 
import GHC.TypeLits 

import Data.Proxy 

type family AllSatisfy (f :: k -> Constraint) (xs :: [k]) :: Constraint where 
    AllSatisfy f '[] =() 
    AllSatisfy f (x ': xs) = (f x, AllSatisfy f xs) 

data HList (as :: [*]) where 
    HNil :: HList '[] 
    HCons :: a -> HList as -> HList (a ': as) 

type family Keys (xs :: [(a, b)]) :: [a] where 
    Keys '[] = '[] 
    Keys ('(a, b) ': xs) = a ': Keys xs 

type family Values (xs :: [(a, b)]) :: [b] where 
    Values '[] = '[] 
    Values ('(a, b) ': xs) = b ': Values xs 

showHList :: AllSatisfy Show xs => HList xs -> [String] 
showHList HNil = [] 
showHList (HCons x xs) = show x : showHList xs 

data SKeyMap :: [(*, Symbol)] -> * where 
    SKeyNil :: SKeyMap '[] 
    SKeyCons :: Proxy a -> Proxy s -> SKeyMap xs -> SKeyMap ('(a, s) ': xs) 

class KnownKeyMap (keyMap :: [(*, Symbol)]) where 
    sKeyMap :: SKeyMap keyMap 


instance KnownKeyMap '[] where 
    sKeyMap = SKeyNil 

instance KnownKeyMap keyMap => KnownKeyMap ('(a, s) ': keyMap) where 
    sKeyMap = SKeyCons Proxy Proxy sKeyMap 

showWithKey' :: forall (keyMap :: [(*, Symbol)]) . 
       (AllSatisfy Show (Keys keyMap) 
       ,AllSatisfy KnownSymbol (Values keyMap) 
       ) => 
       SKeyMap keyMap -> HList (Keys keyMap) -> [(String, String)] 
showWithKey' SKeyNil HNil = [] 
showWithKey' (SKeyCons _ sp skRest) (HCons (x :: a) (xs :: HList as)) = 
    (show x, symbolVal sp) : (showWithKey' skRest xs) 

showWithKey :: forall (keyMap :: [(*, Symbol)]) . 
       (KnownKeyMap keyMap 
       ,AllSatisfy Show (Keys keyMap) 
       ,AllSatisfy KnownSymbol (Values keyMap) 
       ) => 
       HList (Keys keyMap) -> [(String, String)] 
showWithKey = showWithKey' (sKeyMap @keyMap)