Indexed constraint families
simonpj at microsoft.com
Mon Sep 12 15:57:12 CEST 2011
I've added some implementation notes to
They could doubtless do with expansion: please ask away and/or edit.
| -----Original Message-----
| From: Manuel M T Chakravarty [mailto:mchakravarty at me.com]
| Sent: 10 September 2011 14:16
| To: Simon Peyton-Jones
| Cc: GHC; Dominic Orchard
| Subject: Re: Indexed constraint families
| This is fantastic stuff!! Thanks, Max!
| I wonder about the difference between lifted and unlifted constraints, though. The
| wiki page doesn't seem to mention it.
| Simon Peyton-Jones:
| > Folks
| > Max has just pushed a patch that adds a major new feature: indexed constraint
| families; see http://hackage.haskell.org/trac/ghc/wiki/KindFact
| > Internally, a big change is that there is no PredTy any more. So TypeRep has gotten
| simpler (hooray).
| > Julien, Dimitrios: this will conflict with your in flight stuff -- but will
| basically make it simpler.
| > Many thanks to Max; and Dominic for expressing the original idea so persuasively.
| > Simon
| > commit 9729fe7c3e54597ccf29c43c8c8ad0eaa2402ced
| > Author: Max Bolingbroke <batterseapower at hotmail.com>
| > Date: Tue Sep 6 17:22:47 2011 +0100
| > Implement -XConstraintKind
| > Basically as documented in http://hackage.haskell.org/trac/ghc/wiki/KindFact,
| > this patch adds a new kind Constraint such that:
| > Show :: * -> Constraint
| > (?x::Int) :: Constraint
| > (Int ~ a) :: Constraint
| > And you can write *any* type with kind Constraint to the left of (=>):
| > even if that type is a type synonym, type variable, indexed type or so on.
| > The following (somewhat related) changes are also made:
| > 1. We now box equality evidence. This is required because we want
| > to give (Int ~ a) the *lifted* kind Constraint
| > 2. For similar reasons, implicit parameters can now only be of
| > a lifted kind. (?x::Int#) => ty is now ruled out
| > 3. Implicit parameter constraints are now allowed in superclasses
| > and instance contexts (this just falls out as OK with the new
| > constraint solver)
| > Internally the following major changes were made:
| > 1. There is now no PredTy in the Type data type. Instead
| > GHC checks the kind of a type to figure out if it is a predicate
| > 2. There is now no AClass TyThing: we represent classes as TyThings
| > just as a ATyCon (classes had TyCons anyway)
| > 3. What used to be (~) is now pretty-printed as (~#). The box
| > constructor EqBox :: (a ~# b) -> (a ~ b)
| > 4. The type LCoercion is used internally in the constraint solver
| > and type checker to represent coercions with free variables
| > of type (a ~ b) rather than (a ~# b)
| > _______________________________________________
| > Cvs-ghc mailing list
| > Cvs-ghc at haskell.org
| > http://www.haskell.org/mailman/listinfo/cvs-ghc
More information about the Cvs-ghc