[Haskell] Type Class Question

[Simon Peyton-Jones]

GHC insists that every type class constraint mentions a type variable
that is quantified just outside the constraint.  E.g.
	forall a b c.  (C a c, D b) => ...

The constraints (C a c), (D b) must each mention at least one of a,b,c.


Why?  Because it makes it much easier to know when a constraint must be
solved. Consider

	f :: K a => ...

	g :: E b => b -> b
	g x = let h :: D b => ...
		   h x = ....(f e)....
		in ...

Notice that there is no 'forall' on the type sig for h, so it disobeys
GHC's rule.  Suppose the call to f is at type (Tree [b]).  That gives
rise to the constraint (K (Tree [b])).  Now, can the constraint (K (Tree
[b])) be satisfied by the (D b)?  Or by the enclosing constraint (E b)?
Or by a combination of the two?

At the moment GHC's rule means it can use the rule "a constraint C
floats outwards until it hit a 'forall' that binds one of the type
variables mentioned in C. Then C must be solved using the constraints
bound at that forall".

All this makes solving easier.  Everything would work fine without the
restriction, but inference would be a bit harder.  So far, solving that
harder inference problem hasn't seemed important enough, but it's
certainly soluble.  (Martin Sulzmann's implication constraints suggest
how.)

Simon

| -----Original Message-----
| From: haskell-bounces at haskell.org [mailto:haskell-bounces at haskell.org]
On Behalf Of Paul Govereau
| Sent: 22 November 2005 07:56
| To: haskell at haskell.org
| Subject: Re: [Haskell] Type Class Question
| 
| 
| Ah yes, but this forces me to write my instance of Show right away. I
| cannot write:
| 
| module A where data X = X
| module B where
|   import A
|   bar x = show x  -- here is the problem
| moduel C where
|   import A
|   instance Show X where show x = "X"
| module Main where
|  import A
|  import B -- Show instance used
|  import C -- Show instance defined
| 
| I am not saying that this is terribly useful, I am just wondering why
| it is a problem to allow it?
| 
| Paul
| 
| BTW, The above program is a translation of an idiomatic use of
| functors in ML (pardon my syntax):
| 
|   module A : sig type t = ... end
|   module B : funsig(X:SHOW where t = A.t) sig bar : A.t -> string end
|   module C : SHOW where t = A.t
|   open A
|   open B(C)
| 
| 
| On Nov 21, Cale Gibbard wrote:
| > data X = X deriving Show
| >
| > bar :: X -> String
| > bar x = show x
| >
| > There's no need for the class constraint at all. If it's an instance
| > of Show, then you're okay with just applying show to it. There's no
| > need to actually assert that it's actually an instance of Show
again.
| >
| > The only purpose of class constraints is to restrict polymorphism.
If
| > a function isn't polymorphic to begin with, you should never need
| > them.
| >
| >  - Cale
| >
| > On 21/11/05, Paul Govereau <govereau at eecs.harvard.edu> wrote:
| > > Hello,
| > >
| > > I was hoping that someone could answer a question I have about the
| > > type class system. In Haskell, I cannot write a term with an exact
| > > constraint:
| > >
| > > > data X = X
| > > > bar :: Show X => X -> String
| > > > bar x = show x
| > >
| > > According to the Haskell 98 report, a qualifier can only be
applied to
| > > type variables, but I don't see where the trouble is. The term
seems
| > > to have reasonable type, and I don't see any reason why the
| > > dictionary-passing translation shouldn't work out; I am wondering
what
| > > problems you run into if this restriction is lifted?
| > >
| > > Note, with GHC and Glasgow extensions you can write this program:
| > >
| > > > data Y a = Y
| > > > foo :: Show (Y a) => Y a -> String
| > > > foo x = show x
| > >
| > > However, the first program is still ruled out. Are there any
| > > type-class experts out there that can offer an explanation?
| > >
| > > Thanks,
| > > Paul
| > > _______________________________________________
| > > Haskell mailing list
| > > Haskell at haskell.org
| > > http://www.haskell.org/mailman/listinfo/haskell
| > >
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell