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

About Shayan

Researcher/Programmer at Chalmers University of Technology
This entry was posted in Articles. Bookmark the permalink.

4 Responses to Giving Kinds a Demotion

  1. I’m just a layman, I don’t know formal type theory, but this resembles a system I saw somewhere else, the calculus of constructions.

    • In CoC or any system with dependent typing there is no distinction between types and values, therefore they are handled in a rather similar way . Here we have a vanilla Haskell 2010 typechecker , that doesn’t even support local assumptions (GADTs , Typefamilies and etc). I just demonstrated a simple trick to use the same system to infer kinds. I assume any typechecker with a reasonable design would reuse the same machinery.

  2. noname says:

    How is this Haskell 2010 when you’re using KindSignatures?

    • Indeed, the original typechecker does not accept the standard Haskell 2010 code since it “demands type terms to be explicitly kinded”. As I mentioned in the reply above it is a vanilla Haskell 2010 typechecker, i.e. there is no kind inference. With the bootstrapping method described in the post we add the support.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s