CODEWITHSUNDEEP
haskell
Nol
Nol

Reputation: 75

Constrain elements of a type-level list in Haskell

I'm trying to write a type family I can use to constrain the elements of a type level list. I have this code:

{-# 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"])

From what I understand this should work, but when I compile ghc spits out this:

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)

Upvotes: 2

Views: 363

Answers (2)

dfeuer
dfeuer

Reputation: 48591

I don't know much about type families, so I'll point you to gallais's answer for an explanation of what went wrong in your code. Here is a very different approach, with a number of demo functions. There might be better ways; I don't know.

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

This gives

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

To get something more like what you sought,

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)

This gets

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

And here's another fun function:

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)

Upvotes: 3

gallais
gallais

Reputation: 12103

The problem here is that Head does not reduce when fed xs in test so Haskell has no way to deduce KnownSymbol (Head xs) from AllHave KnownSymbol xs. And it shouldn't: what should happen in case xs is empty?

To solve this problem, you can make it explicit that xs is not empty like so:

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

Upvotes: 4

Related Questions