= Kind inference for types and classes =
This page summarises several alternative designs for doing kind inference for
types and classes, under `-XPolyKinds`. See the extensive discussion on #9200. (See also #9201.)
== Current strategy (GHC 7.8) ==
Running example:
{{{
data T a f = T1 Int (T a f) | T2 (f a)
data S a f = S1 (S Maybe (S Int))
}}}
Here is GHC 7.8's strategy:
1. Sort data/type/class declarations into strongly connected components. In our example, there are two recursive SCCs, one for `T` and one for `S`.
2. Then, for each SCC in turn:
* Bind the type constructor to a fresh meta-kind variable:
{{{
T :: kappa0
}}}
* Kind-check all the declarations of the SCC in this environment. This will generate some unifications, so in the end we get
{{{
kappa0 ~ kappa1 -> (kappa1 -> *) -> *
}}}
* Generalise. So we get
{{{
T :: forall k. k -> (k -> *) -> *
}}}
Following the same three steps for `S` fails, because we need polymorphic recursion. Srarting with `S :: kappa0`, we get
{{{
kappa0 ~ kappa1 -> kappa2 -> * -- S has two arguments
kappa1 ~ *->* -- From (S Maybe)
kappa1 ~ * -- From (S Int)
...and some more...
}}}
So in GHC 7.8 you can supply a "complete user-supplied kind" (CUSK) for `S`, thus:
{{{
data S (a :: k) (f :: k -> *) where
S1 :: S Maybe (S Int) -> S a f
}}}
The real step 2 works thus:
* Bind the each non-CUSK type constructor to a fresh meta-kind variable, and each CUSK type constructor to its polymorphic kind.
{{{
S :: forall k. k -> (k->*) -> *
}}}
* Kind-check all the declarations of the SCC in this environment. With this new kind for `S`, kind checking succeeds.
* Generalise any non-CUSK type constructors.
== Proposed new strategy ==
The main proposed change is to the definition of a "complete user-supplied kind" (CUSK). The current story is in [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind-polymorphism.html#complete-kind-signatures Section 7.8.3 of the user manual]. Alas, it does not allow CUSKs for class declarations.
The new proposal is this:
* A class or datatype is said to have a CUSK if and only if all of its type variables are annotated.
* A closed type family is said to have a CUSK if and only if all of its type variables and its return type are annotated.
* An open type family always has a CUSK -- unannotated type variables (and return type) default to `*`. (This is not a change.)
This is somewhat simpler, it covers classes. See comment:19:ticket:9200 for more exposition.
This change alone is enough to satisfy #9200.
'''Simon''' What about type synonym declarations? Don't we need a kind signature on the RHS? Also what about specifying the return kind of a type family (open or closed)? Does it default to `*`, or must you specify it to get a CUSK?
'''Richard''' Type synonym declarations can never be recursive, right? So, this issue doesn't affect them. I've answered the other questions above.
'''Simon''' Wrong: type synonyms can be recursive through a data type:
{{{
data S (a :: k) (f :: k -> *) = S1 (SSyn (S Int) Maybe)
type SSyn f a = S a f
}}}
This will fail despite the CUSK for `S` because `SSyn` lacks one. (The variation below would fix this particular example.) I think #9151 is another example.
== A possible variation ==
This algorithm is not quite as expressive as it could be. Consider
{{{
data SS f a b = MkSS (TT a f) (SS f a b)
data TT (a::k) (f::k -> *) :: * where
MkTT :: f a -> SS f a Maybe -> SS f a Int -> TT a f
}}}
Here `TT` has a CUSK, but `SS` does not. Hence in step 1 we'd bind `SS :: kappa0`. But in the RHS of `TT` we use `SS` at two different kinds, so infernece will fail. We could solve this by giving a CUSK to `SS` as well.
However, we can ''also'' solve it using a plan due to Mark Jones, and one that GHC 7.8 already follows for ordinary, recursive term-level functions. As usual, divide the declarations into SCCs, and then for each SCC do the following:
* Identify which type constructors have Complete User Type Signatures (CUSK). In this example, `TT` does. Extend the environment with these, fixed, kinds:
{{{
TT :: forall k. k -> (k->*) -> *
}}}
* Perform a new strongly-connected component (SCC) analysis on the non-CUSK decls in the SCC, ''ignoring dependencies on a type constructor with a CUSK''. In our example, we get a single recursive SCC, containing `SS`.
* For each SCC in turn:
* Bind the type constructor to a fresh meta-kind variable:
{{{
SS :: kappa0
}}}
* Kind-check all the declarations of the SCC in this environment. This will generate some unifications, so in the end we get
{{{
kappa0 ~ (kappa1 -> *) -> kappa1 -> kappa2 -> *
}}}
The `kappa1` arises from instantiating `TT` at its call site in `SS`
* Generalise. So we get
{{{
SS :: forall k1 k2. (k1->*) -> k1 -> k2 -> *
}}}
* Extend the environment with these generalised kind bindings, and kind-check the CUSK declarations.
The Key Point is that we can kind-check `SS` ''without looking at `TT`'s definition at all'', because we completely know `TT`'s kind. That in turn means that we can exploit ''inferred'' polymorphism for `SS` when kind-checking `TT`. As we do here: `TT` uses `SS` in two different ways `(SS f a Maybe)` and `(SS f a Int)`.
This strategy is more complicated than the initial proposal, but allows fewer annotations. It's not clear whether it is wroth the bother.
=== Typing rule for the new proposal ===
An algorithm is all very well, but what about the typing judgements?
We will pretend that data, type, type family, class declarations look something like this:
{{{
T :: forall k1 k2. (k1 -> *) -> k1 -> _ -> *
data/type/class T a b c = rhs
}}}
That is, there is a possibly-partial kind signature, with holes denoted by "_", and a definition "rhs" (eg the consructors of a data type, or equations of a closed type family). In reality there isn't a separate kind signature; instead, it is integrated in the definition; e.g.
{{{
data T (a::k1 -> *) (b::k1) c = MkT (a b) c
}}}
The kind variables mentioned in the partial kind signature scope over the "rhs".
Then we have two typing rules, one for CUSK, and one for non-CUSK.
We give the rule for data types but modulo keyword it works for classes, closed
type families, etc. We ignore arity/saturation issues for type families.
{{{
k has at least one missing bit (non-CUSK)
k2 = k[k'1 .. k'n/_] -- k'1 .. k'n are magically known
kvs2 = fkv(k2)
G, kvs2, T : k2 |- (data T tvs = rhs) ok -- Monomorphic recursion
----------------------------------------------------- NoCUSK
G |- (T :: forall kvs. k; data T tvs = rhs) :: {T :: forall kvs2. k2}
k has no missing bits (CUSK)
G, T : forall kvs. k |- (T tvs = rhs) ok -- Polymorphic recursion
----------------------------------------------------- CUSK
G |- (T :: forall kvs. k; data T tvs = rhs) :: {T :: forall kvs. k}
}}}
We need two rules, depending on whether or not a CUSK is detected.
The first rule requires the equations to be fully parametric in its kinds, whereas the second allows non-parametric equations and polymorphic recursion. '''Simon:''' I don't know what this means. '''Richard:''' "Non-parametric" here refers to using a kind-indexed closed type family, where the equations match on the kinds, not just the types. It has a flavor of polymorphic recursion in that the instantiations for the kind variables are not always the same at every usage. '''Simon'' does it really matter? Could we simply nuke this paragraph? Introducing an entirely new term, that then has to be explained, and is not necessary to the exposition, seems to add nothing.
For closed type families, these rules are ''different'' than the implementation today, because kind inference for closed type families today is ill-specified. See comment:18:ticket:9200.
----------------------------------
Now here are some design alternatives that we rejected.
== Partial kind signature strategy (PARTIAL) ==
The key idea is that ''all polymorphism is declared'', so nothing gets to be kind-polymorphic unless you say so. But the payoff is that you can give partial kind signatures. Here's the strategy.
1. Sort the declarations into SCCs. No special treatment for CUSKs.
2. For each declaration, extend the environment with a kind binding that has a forall for each ''explicit'' user-written kind variable, but meta-kind variables otherwise. These kind annotations amount to partial kind signatures. For example
{{{
data Foo (a :: k1 -> k1) b c = ...
}}}
would get a kind binding
{{{
Foo :: forall k1. (k1->k1) -> kappa1 -> kappa2 -> *
}}}
Our earlier example would give
{{{
T :: forall k. k -> (k->*) -> *
S :: kappa3 -> kappa4 -> kappa5 -> *
}}}
3. Kind-check the declartions in this environment. At a call of `Foo`, say, we'd instantiate the `forall k1` with a fresh meta-kind variable, but would share `kappa1`, `kappa2` among all calls to `Foo`.
4. Default any unconstrained meta kind variables to `*`
That's it! No generalisation step. The ''only'' polymorphism is that declared by the user.
So our earlier `SS`/`TT` example would be rejected because it relies on S being polymorphic in its third parameter. If you want the `SS`/`TT` example to work you could write
{{{
data SS (f::k1->*) (a::k1) (b::k2) = MkSS (TT a f) (SS f a b)
data TT (a::k) (f::k->*) where
MkTT :: f a -> SS f a Maybe -> SS f a Int -> TT a f
}}}
=== Declarative typing rules for (PARTIAL) ===
I think that (PARTIAL) has a nice declarative typing rule.
Here is what the conventional declarative typing rule, ''in the absence of polymorphism'' for a single self-recursive function looks like. (I'm using the term language but the same thing happens at the type level.)
{{{
G, f:t |- e:t
G, f:t |- b:t'
---------------------------
G |- letrec f = e in b : t'
}}}
Here the "t" is a monotype (no foralls) that the declarative typing rules clairvoyantly conjures up out of thin air.
Once you add Hindley-Milner style polymorphism, the rule gets a bit more complicated
{{{
G, f:t |- e:t
G, f:gen(G,t) |- b:t'
---------------------------
G |- letrec f = e in b : t'
}}}
where 'gen' is generalising.
The (PARTIAL) rule might look like this:
{{{
t = forall vs. sig[t1..tn/_]
vs \not\in ti
G, f : t |- e : forall vs.t
G, f : t |- b:t'
--------------------------- (T-PARTIAL)
G |- letrec f :: forall vs. sig; f = e in b : t'
}}}
Here I'm expressing the user-specified knowledge as a signature `forall vs.sig`, with '_' for bits you don't want to specify.
{{{
f :: forall a. _ -> a -> _
}}}
Then the rule intantiates each '_' independently with
a clairvoyantly guessed monotype (provided it does not mention
the 'vs', or 'a' in this example), and off you go.
=== A tricky point about (PARTIAL) ===
Notice that in this typing rule I say `vs \not\in ti`. If you don't have that side condition I think
complete inference becomes very hard. Suppose `MT :: (*->*) -> *`, and consider
{{{
data Foo f (a::k) = MkFoo (Foo Maybe Int) (Foo MT Maybe)
}}}
Because of the partial kind signature we'll kind-check `Foo`'s RHS with this kind signature for `Foo`:
{{{
Foo :: forall k. kappa1 -> k -> *
}}}
using the unification variable `kapp1` for `f`. Now, if we clairvoyantly decide `kappa1 := k->*`, as would be allowed by (T-PARTIAL), then indeed the definition if well-kinded. So we'd better infer that, if we are to be complete wrt (T-PARTIAL). But the algorithm will share `kappa1` among both calls to `Foo`, and will therefore unify `Maybe` with `MT` and fail.
To gain completeness we need to be less ambitious; hence the side condition in (T-PARTIAL) `vs \not\in ti`.
But that side condition, in turn, means that this will fail:
{{{
data Foo f (a::k) = MkFoo (f a) (Foo f a)
}}}
because here `kappa1` must be unified with `k->*`, which isn't allowed by (T-PARTIAL).
Maybe that is acceptable; you can always decorate both of `Foo`'s arguments.
== Generalised partial kind signature strategy (PARGEN) ==
The (PARGEN) strategy is exactly like (PARTIAL) except that step 4 is different:
4. Generalise over any unconstrained meta kind variable, rather than defaulting to `*`. Since we are operating at top level, there are no kind variables mentioned in the environment, so no need for the ususal "not free in the environment" check.
So we use the partial kind signatures to express any polymorphism necessary for recursion ''inside'' the SCC,
but perhaps infer yet more polymorphism that can be used ''after'' the SCC. Thus:
{{{
data T1 f a = MkT1 (f a) (T f a)
-- Success: T1 :: forall k. (k->*) -> k -> *
data T1a f (a::k) = MkT1a (f a) (T f a)
-- Failure: f's kind is unified with skolem k
-- See "tricky point" above
data T2 f a = MkT2 (f a) (T2 Maybe Int) (T2 Monad Maybe)
-- Failure: needs polymorphic recursion
data T3 (f::k->*) (a::k) = MkT3 (f a) (T3 Maybe Int) (T3 Monad Maybe)
-- Success: polymorphic recursion declared
data T4 (f::k->*) a = MkT4 (f a) (T4 Maybe Int) (T4 Monad Maybe)
-- Failure: not all polymorphism in k is declared
-- See "tricky point" above
}}}
=== Declarative typing rules for (PARGEN) ===
The declarative rule for (PARGEN) is a combination of the one for (PARTIAL) with
the standard generalisation:
{{{
t = forall vs. sig[t1..tn/_]
vs \not\in ti
G, f : t |- e : forall vs.t
G, f : gen(G,t) |- b:t'
--------------------------- (T-PARGEN)
G |- letrec f :: forall vs. sig; f = e in b : t'
}}}
The difference from (PARTIAL) is that before type-checking `b` we generalise `t`.
Here is the declarative rule for closed type families:
{{{
k2 = forall fkv(k1). k1[k'1 .. k'n/_]
fkv(k1) \not\in k'j
forall i: G, F:k2 |- (F ps_i = t_i) ok
k3 = gen(G, k2)
---------------------------------------------------
G |- type family F :: k1 where { F ps_i = t_i } : k3
}}}
This is very similar to the declarative typing rule for `letrec` above. Here, I am ignoring issues with arity/saturation and using a syntax where the kind signature of a type family is given as `k1` with blanks, instead of the tyvarbndr syntax used in source code.
This is in fact an improvement over the current state of affairs, which is essentially this rule ''without'' the side condition. Because of the omitted side condition, we don't have principal types! For example,
{{{
type family X (a :: k) where
X True = False
}}}
`X` could be `X :: k -> k` or `X :: k -> Bool`. Neither is more general than the other. GHC chooses `X :: k -> Bool`, but it's not principled. This is what I get for implementing kind inference for closed type families without writing out declarative rules! In any case, the solution to this problem (closed type families) seems to be the same as the solution for datatypes and classes, quite happily: add the side condition.
=== How does (PARGEN) differ from (BASELINE)? ===
(PARGEN) and (BASELINE) are incomparable.
* The `SS/TT` example under (BASELINE) will be rejected by (PARGEN) becuase `SS` will get kind `kappa1 -> kappa2 -> kappa3 -> *` when kind-checking the `SS/TT` strongly connected component. But (BASELINE) accepts it by breaking the SCC into two.
* There are obviously examples that are accepted by (PARGEN) but not (BASELINE).
So moving from (BASELINE) to (PARGEN) would be a breaking change, but only in rather obscure circumstances. I am intensely relaxed about that particular backward-compatibility problem!
== All of the above (ALL) ==
Combine (BASELINE) and (NEWCUSK), for the CUSK stuff, with (PARGEN) for type with partial kind signatures. This would type the
most programs, but is the most complicated.
== Type signatures ==
Another place that we currently (i.e. using (BASELINE)) do kind generalisation is in ''type signatures''. If you write
{{{
f :: m a -> m a
f = ...
}}}
then the type signature is kind-generalised thus:
{{{
This user-written signature
f :: m a -> m a
means this (BASELINE)
f :: forall k (a:k) (m:k->*). m a -> m a
}}}
And f's RHS had better ''be'' that polymorphic.
However (PARTIAL) does no kind generalisation, and it would be consistent to cease doing so for type signatures too. so:
{{{
This user-written signature
f :: m a -> m a
means this (PARTIAL)
f :: forall (a:*) (m:k->*). m a -> m a
}}}
If you want the kind-polymorphic one, you'd have to write thus
{{{
This user-written signature
f :: forall k (a:k) (m:k->*). m a -> m a
means this (PARTIAL)
f :: forall k (a:k) (m:k->*). m a -> m a
}}}
== Reflection ==
I think we could reasonably switch to (PARTIAL) throughout.
As Richard's comments in `TcHsType` point out, we don't want maximal polymorphism. His example is:
{{{
type family F a where
F Int = Bool
F Bool = Char
}}}
We could generate
{{{
F :: forall k1 k2. k1 -> k2
}}}
so that `(F Maybe)` is well-kinded, but stuck. But that's probably not what we want. It would be better to get `F :: * -> *`
But what about
{{{
type family G a f b where
G Int f b = f b
G Bool f b = Char -> f b
}}}
You could just about argue that the programmer intends
{{{
F :: forall k. * -> (k->*) -> k -> *
}}}
It's quite similar to this:
{{{
data PT f a = MkPT (f a)
}}}
which today, using (BASELINE), we infer to have kind
{{{
PT :: forall k. (k->*) -> k -> *
}}}
But I'd be perfectly happy if PT got a ''monomorphic'' inferred kind,
which is what (PARTIAL) would do:
{{{
PT :: (*->*) -> * -> *
}}}
If you want the poly-kinded PT, use a signature:
{{{
-- Any of these would do
data PT f (a :: k) = MkPT (f a)
data PT (f :: k -> *) a = MkPT (f a)
data PT (f :: k -> *) (a :: k) = MkPT (f a)
}}}
One oddity is that we'd do (BASELINE) for terms and (PARTIAL) for types. But perhaps that's ok. They are different.
* Terms ought to be as polymorphic as possible but arguably not types. Examples above. Also, since kind polymorphism is still in its infancy, maybe it's no bad thing if all kind polymorphism is explicitly signalled every time a kind-polymorphic binder is introduced.
* Terms have well-established separate type signatures, but we don't have a syntax for separate kind signatures of types and classes.
If we moved from (BASELINE) to (PARTIAL), some programs that work now would fail:
* the original S/T example above
* a data type like `PT` where the user did actually want the kind-polymorphic version.
But that might be a price worth paying for the simplicity, uniformity, and predictability you'd get in exchange.
'''Richard:''' I think changing to (PARTIAL) throughout would be a mistake, as lots of code would fail to compile. Kind polymorphism by default in datatypes and classes has been around since 7.4, and I suspect there is quite a bit of code that such a change would disrupt.
On the other hand, I think changing to (PARGEN) throughout would work nicely. I believe that it would allow all current code to type-check (except for the weird example that probably should be rejected in #9201). If we were to choose (PARGEN) over (ALL), it's possible that some code would become ''more'' polymorphic, as (PARGEN) is more polymorphic than (BASELINE) in the presence of a CUSK. However, I don't believe that this could be a ''breaking'' change, and I would prefer going with (PARGEN) over (ALL) for the sake of simplicity -- no need to have two systems around.
I can't figure out a way that (BASELINE) and (PARGEN) are different in type signatures for terms. This version doesn't have quite as nice a declarative typing rule because the type is generalized over kind variables that go completely unmentioned in the type -- a straightforward `forall ftv(t). t` doesn't quite do it. We need to generalize over seen variables, infer kinds, and then generalize over meta-kind variables. But, this is what is done today.
(Because open type families do not have a body, they ''would'' still be considered to have a CUSK, where un-annotated type variables default to have kind `*`.)
In comment:5:ticket:9200, I discuss "good" polymorphism and "bad" polymorphism. This discussion, in retrospect, seems tangential at this point. It really only makes sense when discussing closed type families, which aren't at the heart of the problems here. '''End Richard'''