Giving Kinds a Demotion

Kind inference in Haskell is one of the first steps in typechecking. It allows programmers to write type signatures without mentioning their kind.
Having a sound typechecker that demands type terms to be explicitly kinded, I was thinking of using the typechecker itself to do the kind inference.
Up to date, I am not aware of any similar “bootstrapping” method for kind inference and I am not sure if the resulting system is sound.
For more information about kind inference in Haskell, you may refer to:

Haskell 2010 Report
“A Static Semantics for Haskell” by Karl-Filip Faxen
“Giving Haskell a Promotion” — about the new extensions to GHC

In the following, I am going to sketch my idea with concrete examples. I used GHCi 7.4.1 with -XNoMonomorphismRestriction, -XKindSignature and -XExplicitForAll flags.

{-# LANGUAGE NoMonomorphismRestriction, KindSignatures, ExplicitForAll #-}

First I define the * kind:

data Star :: *
star :: Star
star = undefined

Then, for each primitive type, I define a function with explicit type:

tInt :: Star
tInt = undefined

I also define a function to represent the function type constructor (->):


infixr 6 -->
(-->) :: Star -> Star -> Star
a --> b = undefined


With GHC 7.2, if I am not mistaken, we have the “constraint” kind reserved as the kind of class constraints.
I code it as:

data Constraint :: *
constraint :: Constraint
constraint = undefined

For example:

cEq :: Star -> Constraint
cEq = undefined

A combinator to represent the predicates:

infixr 5 ==>
(==>) :: Constraint -> Star -> Star
(==>) = undefined


Now it is time to use these combinators to represent type signatures. For example:

f1 :: a -> Int
f1 = undefined

f2 :: a
f2 = undefined

f3 :: Int
f3 = undefined

f4 :: Eq a => a -> Int
f4 = undefined

 

is modeled as:

-- inferred type: tf1 :: Star -> Star
tf1 a = a --> tInt

-- inferred type: tf2 :: forall (t :: *). t -> t
tf2 a = a

-- inferred type: tf3 :: Star
tf3 = tInt

-- inferred type: tf4 :: Star -> Star
tf4 a = cEq a ==> a --> tInt

Here is the trick; we demote the type living in the type-universe to a normal value. Consequently, the inferred type for this value, hopefully,
represents the kind of the original type. Therefore, by this technique we can use the typechecker to also infer kinds.
For example, the inferred type of tf1 represents the kind of f1.

GHCi> :t tf1
tf1 :: Star -> Star

Now let us go one step further and model ADTs by the same technique. We first define the sum operator.

infixr 4 <+>
(<+>) :: Star -> Star -> Star
(<+>) = undefined

and then we can represent

data T a b = T1 b Int
| T2 (b -> Int)
| T3 (a b)
-- | T4 a -- ill-kinded
-- | T5 c -- ill-kinded

with

-- inferred type: tT :: (Star -> Star) -> Star -> Star
tT a b = (b --> tInt --> tT a b)
<+> ((b --> tInt) --> tT a b)
<+> (a b --> tT a b)
-- <+> (a --> tT a b) -- ill-typed
-- <+> (c --> tT a b) -- ill-typed

Brilliant! If one part of the original definition is ill-kinded, the representation becomes ill-typed.

Now to add support for type classes, we model the cons operator in the same fashion:

infixr 4 <:>
(<:>) :: forall (a :: *). (a -> Star)-> Constraint -> Constraint
(<:>) = undefined

Now we model the following definition,

class C a where
c1 :: a b -> Int
c2 :: b (a c) -> Int
-- f3 :: a c b -> Int -- ill-kinded

class D a where
d0 :: a -> Int

class E a where
e1 :: E a => a -> Int

to:

cC a = (\b -> a b --> tInt)
<:>(\(b,c)-> b --> (a c) --> tInt)
-- <:> (\(b,c)-> a c b --> tInt) -- ill-typed
<:>constraint

cd a = (\() -> tInt)
<:>constraint

cD a = (\ () -> cD a ==> a --> tInt)
<:>constraint

Notice, the definition of class E is recursive through the use of predicate “E a” but typechecker has no difficulty inferring the right type.

Finally, the support for type synonyms is straightforward:

type S a b c d = T a b

sS a b c d = tT a b

According to Haskell report, definitions should be grouped by their dependency order. Having this framework we can reuse the dependency analysis of let bindings
by simply putting the definition in the same let binding.

This kind system, in addition to features of Haskell 2010, supports constraint kinds and kind polymorphism.

About these ads