To ensure that they are valid, type expressions are classified into different kinds, which take one of two possible forms:
The symbol ∗ represents the kind of all nullary type constructors.
If κ1 and κ2 are kinds, then κ1 → κ2 is the kind of types that take a type of kind κ1 and return a type of kind κ2.
Kind inference checks the validity of type expressions in a similar way that type inference checks the validity of value expressions. However, unlike types, kinds are entirely implicit and are not a visible part of the language.
Kind inference
The first step in the kind inference process is to arrange the set of datatype, synonym, and class definitions into dependency groups. This can be achieved in much the same way as the dependency analysis for value declarations that was described in Section 4.5. For example, the following program fragment includes the definition of a datatype constructor D, a synonym S and a class C, all of which would be included in the same dependency group:
data C a => D a = Foo (S a)
type S a = [D a]
class C a where
bar :: a -> D a -> Bool
The kinds of variables, constructors, and classes within each group are determined using standard techniques of type inference and kind-preserving unification [8]. For example, in the definitions above, the parameter a appears as an argument of the function constructor (->) in the type of bar and hence must have kind ∗. It follows that both D and S must have kind ∗ → ∗ and that every instance of class C must have kind ∗.
It is possible that some parts of an inferred kind may not be fully determined by the corresponding definitions; in such cases, a default of ∗ is assumed. For example, we could assume an arbitrary kind κ for the a parameter in each of the following examples:
data App f a = A (f a)
data Tree a = Leaf | Fork (Tree a) (Tree a)
This would give kinds (κ → ∗) → κ → ∗ and κ → ∗ for App and Tree, respectively, for any kind κ, and would require an extension to allow polymorphic kinds. Instead, using the default binding κ = ∗, the actual kinds for these two constructors are (∗ → ∗) → ∗ → ∗ and ∗ → ∗, respectively.
Defaults are applied to each dependency group without consideration of the ways in which particular type constructor constants or classes are used in later dependency groups or elsewhere in the program. For example, adding the following definition to those above does not influence the kind inferred for Tree (by changing it to (∗ → ∗) → ∗, for instance), and instead generates a static error because the kind of [], ∗ → ∗, does not match the kind ∗ that is expected for an argument of Tree:
type FunnyTree = Tree [] -- invalid
This is important because it ensures that each constructor and class are used consistently with the same kind whenever they are in scope.
From the Haskell2010 report:
To ensure that they are valid, type expressions are classified into different kinds, which take one of two possible forms:
Kind inference checks the validity of type expressions in a similar way that type inference checks the validity of value expressions. However, unlike types, kinds are entirely implicit and are not a visible part of the language.
Kind inference
The first step in the kind inference process is to arrange the set of datatype, synonym, and class definitions into dependency groups. This can be achieved in much the same way as the dependency analysis for value declarations that was described in Section 4.5. For example, the following program fragment includes the definition of a datatype constructor D, a synonym S and a class C, all of which would be included in the same dependency group:
The kinds of variables, constructors, and classes within each group are determined using standard techniques of type inference and kind-preserving unification [8]. For example, in the definitions above, the parameter a appears as an argument of the function constructor (->) in the type of bar and hence must have kind ∗. It follows that both D and S must have kind ∗ → ∗ and that every instance of class C must have kind ∗.
It is possible that some parts of an inferred kind may not be fully determined by the corresponding definitions; in such cases, a default of ∗ is assumed. For example, we could assume an arbitrary kind κ for the a parameter in each of the following examples:
This would give kinds (κ → ∗) → κ → ∗ and κ → ∗ for App and Tree, respectively, for any kind κ, and would require an extension to allow polymorphic kinds. Instead, using the default binding κ = ∗, the actual kinds for these two constructors are (∗ → ∗) → ∗ → ∗ and ∗ → ∗, respectively.
Defaults are applied to each dependency group without consideration of the ways in which particular type constructor constants or classes are used in later dependency groups or elsewhere in the program. For example, adding the following definition to those above does not influence the kind inferred for Tree (by changing it to (∗ → ∗) → ∗, for instance), and instead generates a static error because the kind of [], ∗ → ∗, does not match the kind ∗ that is expected for an argument of Tree:
This is important because it ensures that each constructor and class are used consistently with the same kind whenever they are in scope.