Ограничить элементы списка типов в 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

Проблема здесь состоит в том, что Head не уменьшается при скармливании xs в test поэтому у Haskell нет способа вывести KnownSymbol (Head xs) от AllHave KnownSymbol 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)