Taking values out of a heterogenous list

Question

I'm trying to create a heterogenous list of values that all belong to a certain typeclass. In my case, the typeclass is a multi-parameter typeclass with functional dependencies, but for simplicity's sake, I'll use the Show typeclass here as an example (using GADTs):

data ShowList :: * where
    Nil :: ShowList
    (:::) :: Show a => a -> ShowList -> ShowList

This works fine, and I can start putting values in the ShowList

True ::: (3,4) ::: "abc" ::: 3 ::: Nil

I can write many of the standard list functions like, map, filter, reverse, append, etc. with no problem, but as soon as I try to take out a single element,

head (x ::: xs) = x

I get an errror

Could not deduce (t ~ a)
    from the context (Show a)
      bound by a pattern with constructor
                 ::: :: forall a. Show a => a -> ShowList -> ShowList,
               in an equation for `head'
      at <interactive>:34:12-19
      `t' is a rigid type variable bound by
          the inferred type of head :: ShowList -> t at <interactive>:34:5
      `a' is a rigid type variable bound by
          a pattern with constructor
            ::: :: forall a. Show a => a -> ShowList -> ShowList,
          in an equation for `head'
          at <interactive>:34:12
    In the expression: x
    In an equation for `head': head (x ::: xs) = x

This error makes sense because the type of head would have to be Show a => ShowList -> a, which isn't a reasonable type.

In this example situation, it would be feasible, instead of storing a list of Show a's, to store a list of Strings, since the only thing that can be done with an instance of Show is apply show and get a String.

In my situation, however, the typeclass I've defined is a little more complex:

typeclass Playable a b | a -> b where
    play :: a -> Int -> b

and so I can't just store play x instead of x.

Is there any way be able to have a list of values belonging to a typeclass and be able to take out a single value from the list?

Answer 1

A better alternative to this classic typeclass anti-pattern is to use a simple data type instead. Your Playable class becomes

newtype Playable a b = Playable { play :: a -> Int -> b }

now you can easily work on [Playable a b] and still have all the functionality of the typeclass version (at least as much functionality as mentioned in your question).

Playable forms a monad:

instance Functor (Playable a) where
    fmap f (Playable k) = Playable (\a -> f . k a)

instance Monad (Playable a) where
    return b = Playable (\_ _ -> b)
    Playable k >>= f = Playable (\a i -> play (f (k a i)) a i)

Answer 2

The Issue

Your ShowList type is called an "existential" type, roughly meaning that given a value of type ShowList there exists some type a for its contituents (the list elements, in your case). The point is that nothing is known about this type a, except for the fact that it belongs to the type class Show.

Hence, a function such as head can not be easily typed

head :: ShowList -> ???
head (x ::: _) = x

Using a non-Haskell syntax, the type would be

head :: ShowList -> (exists a. Show a => a)
head (x ::: _) = x

but this is not allowed in Haskell.

A Possible Solution

The main idea is this: Haskell does not let you return the head since that would be untypeable, but Haskell does let you take the head and use it to build something else (which has to have a valid type). For instance

foo :: ShowList -> String
foo Nil = "Nil"
foo (x ::: _) = show x

is alright: we take the head and we use it to build a value of type String. We can also put x back into another existential type

data Showable :: * where
   S :: Show a => a -> Showable

foo :: ShowList -> Showable
foo []        = error "unexpected Nil"
foo (x ::: _) = S x

We can also ask the user of foo to specify which function should be applied to x.

{-# LANGUAGE RankNTypes #-}
foo :: ShowList -> (forall a. Show a => a -> r) -> r
foo []        _ = error ""unexpected Nil"
foo (x ::: _) f = f x

test :: Int
test = foo (123 ::: ("aa" ::: Nil)) f
       where f :: Show a => a -> Int
             f = length . show

The type of the f argument here is sophisticated. It specifies that f must work on any a of class Show. I.e., that the type a is chosen by function foo, not by f: so, f is required to be polymorphic in a.

A Final Note

The ShowList type is nearly equal to [Showable]. Using [Showable] allows to use standard list functions such as head without any issue. The downside is that it requires to box/unbox the data adding/removing constructor S.

Answer 3

Take a look at HList.

As a preliminary, consider the following hack to make head work:

data ShowList :: * -> * where
    Nil :: ShowList z
    (:::) :: Show a => a -> ShowList b -> ShowList a

head :: ShowList a -> a
head (x ::: xs) = x

We store the type of the element in ShowList's type, we can bind to it in our signature for head, and GHC is satisfied. Never mind the empty z, this is just an illustration!

*Main> Main.head $ "five hundred" ::: (123 ::: (True ::: Nil))
"five hundred"

... but now your error has moved to tail:

tail :: ShowList a -> ShowList b
tail (x ::: xs) = xs

Could not deduce (b1 ~ b)
from the context (Show a)
  bound by a pattern with constructor
             ::: :: forall a b. Show a => a -> ShowList b -> ShowList a,
           in an equation for `tail'

Each ::: creates a ShowList parameterised by the type of its head, making it hard to reach the type of the tail. So, we can't access b, and we can't tell GHC that tail should be of type ShowList b.

One way around this (that I know of, anyway) is to parameterise ShowList by a type-level list. Adding TypeOperators and EmptyDataDecls to our extensions:

{-# LANGUAGE GADTs, KindSignatures, TypeOperators, EmptyDataDecls #-}
data Empty

instance Show Empty where
    show = "Empty"

type a :+: b = (a, b)

data ShowList :: * -> * where
     Nil :: ShowList Empty
     (:::) :: Show a => a -> ShowList b -> ShowList (a :+: b)

head :: ShowList (a :+: b) -> a
head (x ::: xs) = x

tail :: ShowList (a :+: b) -> ShowList b
tail (x ::: xs) = xs

This works! Now we are preserving the pairs of types that accompany each pair in our HList.

*Main> head . tail $ "abcde" ::: (True ::: Nil)
True

Answer 4

Your ShowList is essentially a list of existentially quantified values. You could write it isomorphically as:

data Showy = forall a. Show a => Showy a

-- or in GADT syntax:
data Showy' where
    Showy' :: Show a => a -> Showy'

type ShowList' = [Showy]

Your ShowList does not know anything about the values besides that they have a Show instance; there is not even a type variable by which it is parametrized. You can take a value out of the list if you wrap the value in a construction similar to ShowList but only with a single element. Showy happens to be such a data type:

head' :: ShowList -> Showy
head' (x ::: xs) = Showy x

Of course you can't do anything with a Showy aside from showing it, but you couldn't do more with a ShowList either.