[Haskell-cafe] Type vs TypeClass duality

[Tristan Allwood]

> > 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)