Why can't it automatically construct them then? Assuming we do have a syntax for "A list of objects, each of which is of some possibly different type 'a', subject only to the restriction that a is a member of typeclass Show", as the following:
ls :: [a where Show a]
Then I would think that all the type checker has to do would be to check that, a) everything you cons onto ls is an instance of class Show b) where you extract items from ls, you only use them as you would use any instance of class Show. Not sure if anyone has mentioned something similar, and it's not quite what people have been suggesting - but with minimal boilerplate (that I'm sure a TH hacker could derive for you) you can get close to typeclass parameterised lists using GADTs (& ghc 6.8 snapshots ;)) at
the moment. Regards, Tris {-# LANGUAGE EmptyDataDecls, ScopedTypeVariables, PatternSignatures, GADTs, RankNTypes, KindSignatures, TypeOperators #-} {- A list where all elements are in class Show -} testList :: SingleList ShowConstraint testList = () # (LT,EQ,GT) # False # 'a' # (3.0 :: Double) # "hello" # nil {- My user functions over that list -} test = map' (\ShowC -> show) testList test2 = foldr' (\ShowC -> (+) . length . show) 0 testList {- A tiny bit of boilerplate for Show, later rinse repeat for other typeclasses -} data ShowConstraint a where ShowC :: (Show a) => ShowConstraint a instance Show a => Reify (ShowConstraint a) where reify = ShowC {- *Main> test ["()","(LT,EQ,GT)","False","'a'","3.0","\"hello\""] *Main> test2 30 -} {- The bit that is a library -} {- A generic list definition, - (a b) is the witness of the type class for this type, - b is the actual value we put in the list -} data SingleList (a :: * -> *) where Cons :: (a b) -> b -> SingleList a -> SingleList a Nil :: SingleList a {- helper functions to avoid having to pass in the witness explicitly -} nil :: SingleList a nil = Nil infixr 5 # (#) :: (Reify (a b)) => b -> SingleList a -> SingleList a val # rest = Cons reify val rest {- A way to get the type class constraint witness automagically -} class Reify a where reify :: a {- traditional(ish) map, note the function is passed the witness so it can use that - to get the typeclass constraint back into scope by pattern matching on it -} map' :: forall a c . ((forall b . a b -> b -> c) -> SingleList a -> [c]) map' _ Nil = [] map' f (Cons r v rest) = f r v : map' f rest {- and foldr -} foldr' :: forall a c . (forall b . a b -> b -> c -> c) -> c -> SingleList a -> c foldr' f d = go where go Nil = d go (Cons r v rest) = (f r v) (go rest)