約束Haskell中的類型級別列表的元素

Question

我正在嘗試編寫一個類型族，我可以使用它來約束類型級別列表的元素。我有這樣的代碼：

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies #-} 

import GHC.TypeLits (KnownSymbol, symbolVal) 
import GHC.Exts (Constraint) 
import Data.Proxy (Proxy(..)) 

type family AllHave (c :: k -> Constraint) (xs :: [k]) :: Constraint 
type instance AllHave c '[] =() 
type instance AllHave c (x ': xs) = (c x, AllHave c xs) 

type family Head (xs :: [k]) :: k where 
    Head (x ': xs) = x 

headProxy :: proxy xs -> Proxy (Head xs) 
headProxy _ = Proxy 

test :: AllHave KnownSymbol xs => proxy xs -> String 
test p = symbolVal (headProxy p) 

main :: IO() 
main = putStrLn $ test (Proxy :: Proxy '["a", "b"]) 

據我所知這應該工作，但是當我編譯GHC吐出了這一點：

Test.hs:18:10: 
    Could not deduce (KnownSymbol (Head xs)) 
     arising from a use of ‘symbolVal’ 
    from the context (AllHave KnownSymbol xs) 
     bound by the type signature for 
       test :: AllHave KnownSymbol xs => proxy xs -> String 
     at Test.hs:17:9-52 
    In the expression: symbolVal (headProxy p) 
    In an equation for ‘test’: test p = symbolVal (headProxy p) 

Answer 1

這裏的問題是，在test喂xs當Head不減少因此Haskell無法從AllHave KnownSymbol xs推斷KnownSymbol (Head xs)。它不應該：在xs爲空的情況下會發生什麼？

爲了解決這個問題，你可以把它明文規定xs不爲空，如下所示：

test :: AllHave KnownSymbol (x ': xs) => proxy (x ': xs) -> String 

Answer 2

我不知道很多關於家庭類型，所以我會點你gallais's answer一個解釋你的代碼出了什麼問題。這是一個非常不同的方法，具有許多演示功能。可能有更好的方法;我不知道。

data CList :: (k -> Constraint) -> [k] -> * where 
    CNil :: CList c '[] 
    CCons :: c t => proxy t -> CList c ts -> CList c (t ': ts) 

mapCSimple :: (forall a . c a => Proxy a -> b) -> CList c as -> [b] 
mapCSimple f CNil = [] 
mapCSimple f (CCons (t :: proxy t) ts) = f (Proxy :: Proxy t) : mapCSimple f ts 

toStrings :: CList KnownSymbol v -> [String] 
toStrings = mapCSimple symbolVal 

class KnownSymbols (xs :: [Symbol]) where 
    known :: proxy xs -> CList KnownSymbol xs 

instance KnownSymbols '[] where 
    known _ = CNil 

instance (KnownSymbol x, KnownSymbols xs) => KnownSymbols (x ': xs) where 
    known _ = CCons Proxy $ known Proxy 

exampleG :: KnownSymbols xs => proxy xs -> String 
exampleG p = show . toStrings $ known p 

這給

> putStrLn $ exampleG (Proxy :: Proxy '["Hello", "Darkness"]) 
["Hello","Darkness"] 

要得到的東西更喜歡你追求什麼，

cHead :: CList c (a ': as) -> Dict (c a) 
cHead (CCons prox _) = Dict 

test :: forall x xs . CList KnownSymbol (x ': xs) -> String 
test xs = case cHead xs of Dict -> symbolVal (Proxy :: Proxy x) 

test2 :: (KnownSymbols xs, xs ~ (y ': ys)) => proxy xs -> String 
test2 prox = test (known prox) 

這得到

> putStrLn $ test2 (Proxy :: Proxy '["Hello", "Darkness"]) 
Hello 

這裏還有另一個有趣的功能：

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

mapC :: (forall a . c a => Proxy a -> f a) -> CList c as -> HList f as 
mapC f CNil = HNil 
mapC f (CCons (t :: proxy t) ts) = HCons (f (Proxy :: Proxy t)) (mapC f ts)