CODEWITHSUNDEEP
haskellfunctional-programming
user3248346
user3248346

Reputation:

Kind Classification of Types

In Benjamin Pierce's book on Types and Programming Languages he classifies the different kinds of types as follows:

  1. * the kind of proper types (like Bool and Bool -> Bool)
  2. * -> * the kind of type operators (i.e., functions from proper types to proper types)
  3. * -> * -> * the kind of functions from proper types to type operators (i.e., two-argument operators)
  4. (* -> *) -> * the kind of functions from type operators to proper types

If we consider the tuple (1,2), if I query the type and kind of this in the Haskell GHCI I get:

Prelude> :t (1,2)
(1,2) :: (Num t1, Num t) => (t, t1)

Prelude> :k (,)
(,) :: * -> * -> *

I don't see how * -> * -> * falls into category 3 in his definition above. To my knowledge, (,) takes two proper types to produce another proper type, not as Pierce states which is a function from a proper type to a type operator.

I am probably not interpreting Pierce's categorisation properly. Please can someone expand category 3 using my 2-tuple example.

Upvotes: 1

Views: 148

Answers (1)

Carl
Carl

Reputation: 27003

Kinds are curried just like types.

The type of (,) (the value constructor) is a -> b -> (a, b). The type of (,) () is b -> ((), b). The type of (,) () () is ((), ()).

Kinds work exactly the same way. The kind of (,) (the type constructor) is * -> * -> *. The kind of (,) () is * -> *. That's exactly what Pierce is talking about. (And of course, the kind of (,) () () is *).

Edit

The fourth category is a type that looks like this:

newtype Fourth f = Fourth (f ())

The Fourth type constructor has kind (* -> *) -> *. It can take as an argument any type with kind (* -> *), like Maybe or []. So types like Fourth Maybe or Fourth [] have kind *.

Upvotes: 10

Related Questions