Proposal: Data.Proxy

[Ashley Yakeley]

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