Musasabi wrote:
data Proxy a = Proxy
I do this, only I call it "Type". Anyway, ignoring that bikeshed, it can be considered the "universal type-witness". Consider a typical type-witness: data MyType a where MyBool :: MyType Bool MyInt :: MyType Int You can use type-witnesses like this to construct a type-witness for heterogenous lists: data ListType w a where Nil :: ListType w () Cons :: w a -> ListType w b -> ListType w (a,b) So now "ListType MyType" is a witness for heterogenous lists containing only Ints and Bools. But if you want a list that can contain any type, then "ListType Type" (your "ListType Proxy") will do the trick. If you prefer classes for passing witnesses around, that's easy: class Is w a where witness :: w a instance Is (ListType w) () where witness = Nil instance (Is w a,Is (ListType w) b) => Is (ListType w) (a,b) where witness = Cons witness witness instance Is MyType Bool where witness = MyBool instance Is MyType Int where witness = MyInt You can use your list type like this: addInts :: (Is (ListType MyType) list) => list -> Int addInts = addInts' witness where addInts' :: ListType MyType list -> list -> Int addInts' Nil _ = 0 addInts' (Cons (MyType Int) wl) (i:ms) = i + addInts' wl ms addInts' (Cons _ wl) (_:ms) = addInts' wl ms addInts (True,(3,(False,(4,())))) ==> 7