PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Simon PeytonJones
simonpj at microsoft.com
Tue Sep 18 09:10:40 CEST 2012
I think I was a little hasty below, and need a little help.
Making 'Any' an type family, even an injective one, does not work for the use that Richard and Iavor make of it, eg in TypeLits. Here's an example from TypeLits:
instance SingE (Any :: Nat) Integer where
where SingE :: forall k. k > * > Constraint
Here Iavor is using Any as a proxy kind argument. He really wants
SingE :: forall k. * > Constraint
with kindindexed instances. But (much as with the Typeable class at the value level) he is giving it a type argument so that he can later say things like
SingE (Any :: *>*) v
Without this trick we'd need kind application, something like
SingE {*>*} v
None of this works if Any is a type family, because the type patterns in an instance decl aren't allowed to involve type families (and rightly so; value declarations don't have functions in patterns).
Nor can we fix this by introducing some *other* constant, Proxy :: forall k. k, because that suffers from the inconsistency problem that we started with. Another way to say this is as follows. In the value world we have often written
typeOf (undefined :: a)
using bottom as a proxy type argument. That works in Haskell, but not in a strict, or stronglynormalising language. And at the type level we are (mostly) strongly normalising.
The technicallystraightforward thing to do is to add kind application, but that's a bit complicated notationally. http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication Does anyone have any other ideas?
Simon
 Original Message
 From: Simon PeytonJones
 Sent: 16 September 2012 16:49
 To: Richard Eisenberg; Andrea Vezzosi
 Cc: Adam Gundry; Conor McBride; Stephanie Weirich; glasgowhaskell
 users at haskell.org; Simon PeytonJones
 Subject: RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
 functional dependency?

 Friends

 Thanks for this useful conversation, by email and at ICFP. Here's my
 summary. Please tell me if I'm on the right track. It would be great
 if someone wanted to create a page on the GHC wiki to capture the issues
 and outcomes.

 Simon

 Eta rules
 ~~~~~~
 * We want to add etarules to FC. Sticking to pairs for now, that
 would amount to
 adding two new type functions (Fst, Snd), and three new, builtin
 axioms
 axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
 axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
 axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
 Generalising to arbitrary products looks feasible.

 * Adding these axioms would make FC inconsistent, because
 axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
 and that has two different type constructors on each side.
 However, I think is readily solved: see below under "Fixing Any"

 * Even in the absence of Any, it's not 100% obvious that adding the
 above
 eta axioms retains consistency of FC. I believe that Richard is
 volunteering
 to check this out. Right, Richard?

 Type inference
 ~~~~~~~~~
 I'm a little unclear about the implications for inference. One route
 might be this. Suppose we are trying to solve a constraint
 [W] (a:'(k1,ks)) ~ '( t1, t2 )
 where a is an untouchable type variable. (if it was touchable we'd
 simply unify it.) Then we can replace it with a constraint
 [W] '(Fst a, Snd a) ~ '( t1, t2)

 Is that it? Or do we need more? I'm a bit concerned about constraints
 like
 F a ~ e
 where a:'(k1,k2), and we have a type instance like F '(a,b) = ...

 Anything else?

 I don't really want to eagerly etaexpand every type variable, because
 (a) we'll bloat the constraints and (b) we might get silly error
 messages. For (b) consider the insoluble constraint
 [W] a~b
 where a and b are both skolems of kind '(k1,k2). If we etaexpand both
 we'll get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b),
 and we DEFINITELY don't want to report that as a type error!

 Fixing Any
 ~~~~~~~
 * I think we can fix the Any problem readily by making Any into a type
 family,
 that has no instances. We certainly allow equalities with a type
 *family* application on the left and a type constructor on the
 right.
 I have implemented this change already... it seems like a good
 plan.

 * Several people have asked why we need Any at all. Consider this
 source program
 reverse []
 At what type should we instantiate 'reverse' and the empty list []?
 Any type
 will do, but we must choose one; FC doesn't have unbound type
 variables.
 So I instantiate it at (Any *):
 reverse (Any *) ([] (Any *))

 Why is Any polykinded? Because the above ambiguity situation
 sometimes
 arises at other kinds.

 * I'm betting that making Any into a family will mess up Richard's
 (entirely separate)
 use of (Any k) as a proxy for a kind argument k; because now (Any
 k1 ~ Any k2)
 does not entail (k1~k2). We need Any to be an *injective* type
 family. We want
 injective type families anyway, so I guess I should add the
 internal machinery
 (which is easy).

 I believe that injective type families are fully decomposable, just
 like data type families,
 correct? To make them available at the source level, we'd just
 need to
 a) add the syntax injective type family F a :: *
 b) check for injectivity when the user adds type instances
 Richard, would you like to do that part?
More information about the Glasgowhaskellusers
mailing list