[Haskell-cafe] Type vs TypeClass duality

[Tristan Allwood]

On Wed, Oct 24, 2007 at 11:00:14AM +0800, TJ wrote:
> Tristan Allwood:
> 
> Very cool. I don't understand some (a lot of) parts though:
> 
> > instance Show a => Reify (ShowConstraint a) where reify = ShowC
> 
> ShowC has type "(Show a) => ShowConstraint a", whereas reify is
> supposed to have type "ShowConstraint a".
Yes.  ShowC is a constant that wraps up the knowledge of (Show a =>) for
ShowConstraint.  So (in this case) 

reify :: ShowConstraint a
reify = ShowC  

(since ShowC is the only non-bottom value ShowConstraint can take)

But in order to return ShowC, we must know that a 'is in' Show, which is
why the instance declaration requires that at the point you use reify
you can demonstrate that a is in Show:

instance Show a => Reify (ShowConstraint a) where
         ^^^^^^^^^

If the Show a => bit is removed, then the type checker rightly
complains, because the ShowC doesn't have a Show a context that it
needs.

So the trick is that in the cons (#) function which uses reify, you need
to prove 'Reify (a b)', and it just so happens that by the instance
declaration above, wherever you have 'Show a' then you have 'Reify
(ShowConstraint a)' which is why testList needs nothing more than the
values to put into it like a normal list.

> 
> > data SingleList (a :: * -> *) where Cons :: (a b) -> b -> SingleList
> > a -> SingleList a Nil :: SingleList a
> 
> Cons has a type variable "b" in its signature, but no forall. I
> suppose it comes from the * -> * in SingleList's type?
Nope.  The (a :: * -> *) is a kind annotation and means that the a is a
type that is parameterised by a type (e.g. Maybe :: * -> *, whereas
Maybe Int :: *), which is why you can write (a b).  I think technically
it's a redundant annotation here as it can be inferred from the (a b)
useage.

The b is 'just' a normal, exisistentially quantified variable - GADTs
don't require you to write forall in their declarations - see the very
last sentence on
http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html
> 
> 
> That's all I can come up with for now. A great deal of high level
> coding flying around above my head now.
Hope that helps some, 

Regards,

Tris