Further to this,
| Fri Nov 10 05:31:23 PST 2006 [EMAIL PROTECTED]
| * Use implication constraints to improve type inference
Here is the commit message for the patch. Do try it out.
I have tested it quite a lot but I might have broken something
Simon
This major patch adds implication constraints to GHC's type inference
mechanism. (The name "implication constraint" is due to Martin
Sulzmann.)
>From a programmer point of view, there are several improvements
1. Complete(r) type inference
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC's type inference becomes complete (or perhaps more complete!)
Particularly, Karl-Filip Faxen's famous example in "Haskell and principal
types" (Haskell workshop 2003) would type check when the program text
was written in one order, and then fail when the text was re-ordered.
Now it works regardless. The test is tc218.
2. Lifting the "quantified-here" restriction
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The restriction that every constraint in a type signature must mention
at least one of the quantified type variables is lifted. So you can write
f :: C Int => ...
or g :: forall b. Eq a => ...
This may seem odd, but the former was recently requested by a Haskell
user; see this message:
http://www.haskell.org/pipermail/glasgow-haskell-users/2006-September/011137.html
3. Dictionaries are packaged in data constructors
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A very useful new feature is this. When a data type is declared in in
GADT syntax, the context of the constructor is
*required* when constructing
*available* when matching
For example
data T a where
T1 :: Num a => a -> T a
T2 :: Bounded a => T a
f :: T a -> a
f (T1 x) = x+1
f T2 = maxBound
Notice that f is not overloaded. The Num needed in the first branch
is satisfied by the T1 pattern match; and similarly for the T2 pattern
match.
This feature has been often requested, becuase it allows you to
package a dictionary into an ordinary (non-existential) data type, and
be able to use it.
NOTE: the Haskell 98 syntax for data type declarations
data Num a => T a = T1 a
behaves exactly as specified in H98, and *not* in the new way.
The Num dictionary is
*required* when constructing, and
*required* when matching
I think this is stupid, but it's what H98 says. To get the new
behaviour, use GADT-style syntax, even though the data type being
defined is does not use the GADT-ness.
4. Type classes and GADTs
~~~~~~~~~~~~~~~~~~~~~~~~~
The proper interaction between GADTs and type classes is now
respected. For example:
data GADT a where
MkG :: Num a => a -> GADT [a]
g :: forall b. Read b => GADT b -> String -> b
g (MkG n) s = n : read s
Inside the branch we know that b=[a], so the (Read b)
dictionary is a (Read [a]) dictionary, which is why we can
use the result of read in the tail of a cons.
Functional dependencies and equality predicates
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The treatment of functional dependencies is still ad hoc
and unsatisfactory. I do not promise that they will work
nicely in conjunction with GADTs. Trac #345 has a good
example.
More generally, we want to add
- indexed type synonyms
(aka associated type synonyms)
- equality constraints in contexts
Both will require us to furher overhaul constraint
handling. So this patch is just a (big) step on the way.
Implementation notes
~~~~~~~~~~~~~~~~~~~~
The changes only affect the type checker. By far the biggest change
is to TcSimplify.lhs, which deals with simplifying type-class
constraints. It has been almost entirely rewritten. This is a
big deal, beause it's one of the biggest modules in the compiler.
This patch adds 100 lines of code (800 up to 900) to TcSimplify.
[TcSimplify also has a lot fo comments, over 1,700 lines!]
The main changes are these
* The Inst type gets a new constructor, ImplicInst, for implication
constraints
* Implication constraints are
built by TcSimplify.makeImplicationBind
simplified by TcSimplify.reduceImplication
* Improvement is now handled more cleanly, with a boolean
ImprovementDone flag in Avails (which is now a proper data type) to
keep track of when we must iterate
* I put quite a bit of effort into cleaning up the way that error and
location information is tracked and reported. For example, I
cleaned up SkolemInfo, and the printing thereof.
The total change is not too big: an extra 210 lines of code across
the whole compiler. But took a lot of work: diff says I have
1133 new lines written.
_______________________________________________
Cvs-ghc mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/cvs-ghc
