It's a Kind of Magic: Kinds in Type Theory
It's a Kind of Magic: Kinds in Type Theory
The type theory is some Kind of magic.
Join the DZone community and get the full member experience.Join For Free
Get the Edge with a Professional Java IDE. 30-day free trial.
The Beginning of All the Sadness
To make things simple, we start with the Java programming language. In Java, you can define a class (a type), which takes the input parameter another type. It is called a generic class. For example, think of the
List<T> type. There is a type parameter
T that one should provide to the compiler when dealing with a
List to obtain concrete and usable types. Then, we have
List<Optional<Double>>, and so on.
What about if we do not provide a concrete type as the value of the type parameter? What about
List<List>, for example? Well, the Java compiler transforms this type into the more safer
List<List<Object>>, warning you that you are using
List in a non-generic way. And yes,
List<Object> is an awful concrete type.
So, it seems that the Java type system allows filling type parameters only with concrete types. Fair enough. What about the Scala programming language? Well, Scala introduces a feature that is called Higher Kinded Types (HKT). HKTs allow us to define things like the following:
What does that strange symbol,
F[_], mean? It means that
Functor is something (a type class, indeed), which the type parameter can be filled with any other generic type that accepts one, and only one, type parameter, i.e.
Option[T], and so on.
The Scala vision of types comes from how the type system of Haskell was thought. Also in Haskell, you can define a functor.
Different syntax, same semantic.
So, in some programming languages, we need a way to distinguish between the available types. As we just saw, some types are concrete, and types that need some information to become concrete. Type theory comes in help to us with Kinds, i.e. types of types.
However, first, we need to specify the small bricks we need to build the road through Kinds’ definition.
Types and Other Stuff
Starting from the beginning, we found values. Values are the information or data that our programs evaluate. Examples of values are things like
3.14, and so on. Each value in a program belongs to a type. A value can be assigned to a name, that is called a variable.
Types give information to our program about how to treat values at runtime. In other terms, they set constraints to values. Saying that a variable has the type
e: bool; it means that it can have only two values —
So, a type is a compile-time constraint on the values an expression can be at runtime.
In statically-typed programming languages, the definition of types for values is made at compile time. You must give to each value (or variable) a type while you are writing your code. In dynamically-typed programming languages, the type of values is determined at runtime, that is during the execution of the program.
In functional programming languages, in which functions are first-order citizens, each function has an associated type, too. For example, the function
sum, which takes two integers and returns their sum, has type
(Int, Int) => Int in Scala or
Int -> Int -> Int in Haskell.
As we previously said, there can be “types” that are parametric. Generic types uses type parameters to exploit this feature. So, we can define a “type” using a type parameter such as
Tcan be instantiated with any concrete type we want.
Using type parameters is an attempt to justify the fact that, let’s say, the behavior of a
List[Int] is very similar to the behavior of a
List[String]. It is nothing more than a way to generify and abstract over types.
So, in the same way (value) constructors take as input a list of values to generate new values, type constructors take as input a type to create new types.
Option[T], and so on are all classified as type constructors. In Java, we call them generics. In C++, they call them templates.
Now, we have two different “kinds” of objects dealing with types: The former is represented by concrete types; the latter by type constructors. We have just said that we need to define the type of a type.
Some Kind (of Monsters)
Kinds are the types of objects that are related to types, more or less. A kind is more of an arity specifier. In their simplest form, we use the character
* to refer to kinds.
* is the kind of simple and concrete types. A concrete type is a type that doesn’t take any parameters.
What about type constructors? Let’s take a step back. A (value) constructor is nothing more than a function that takes a tuple of values in input and returns a new value.
The above is nothing more than a function of type
(String, String) => Person.
Now, lift this concept to type constructors: values are now represented by types and (value) constructors by type constructors. Then, a type constructor is a function that takes in input a tuple of types and produces a new type.
Think about a list. It’s definition is
List[T]. So, it takes a type in input to produce a concrete type. It is similar to a function having only one parameter.
Option, and so on, has kind
* -> *.
Map[K, V] has kind
* -> * -> *, because it needs two concrete types in input to produce a concrete type.
The fact that type constructors are similar to functions is underlined by the use of currying to model situations, in which more than one parameter takes place.
In Haskell, you can ask the kind of a type to the compiler, using the function
However, a question should arise into your mind: what the hell are Kinds useful for? The answer is typeclasses.
A type class is a concept that not all the programming languages have. For example, it is present in Haskell, and (in some way) Scala, but not in Java.
A type class defines some behaviour, and the types that can behave in that way are made instances of that type class. So when we say that a type is an instance of a type class, we mean that we can use the functions that the type class defines with that type.
A type class is very similar to the concept of
interface in Java. In Scala, it is obtained using a
trait. In Haskell, there is a dedicated construct that is the
class construct. In Haskell, there are type classes for a lot of features that a type could have: The
Eq type class marks all the types that be checked for equality; the
Ord type class marks all the types that can be compared; the
Show type class is used by the types that can be pretty-printed in the standard output.
Functor that we defined earlier is, in fact, a type class. The
fmap function defines the behavior of the type of class.
Type classes are not native citizens of Scala, but they can be simulated quite well. The example below declares the type class
While the Haskell type classes have native support, the compiler recognizes them and automatically generates the binary code associated with them. In Scala, you need to revamp some intricated mechanisms, involving implicits (see Type classes in Scala for more details on the topic).
So, to let a type to belong to a type class contained in the standard library, in Haskell, you have simple to declare it in the type definition using the
In general, to make a type to belong to a type class, you have to provide the implementation of the methods (behaviors) of the type class. The following code shows a possible implementation of the
Functor type class by the
Maybe type (
Option in Scala). As you can see, there are dedicated constructs of the language, as
where, to support type classes.
Anyway, describing abstract behavior, type classes are inherently abstract, too. The way the abstraction is achieved is using type parameters. Usually, type classes declare some constraints on the type represented by the type parameter.
The problem is that type classes can declare some strange type parameters. Reasoning on the kind of types allows us to understand which type can be used to fulfill the type parameter.
Let’s do a simple example. Looking back at the
Functor type class definition, the type
f must have a kind
* -> *, which means that the type class requests types that take only one parameter. The function
f to a type
a and a type
b, which are concrete types in absence of any other indication. As previously said, such kinds of objects are similar to the
Option in Scala, and
Optional in Java),
Set type constructors.
What if we want to apply such type class to the
Either type constructor? Both in Haskell and Scala, it is defined as
Either[L, R], defining two type parameters, respectively left and right. For the definition we gave of a kind,
Either has kind
* -> * -> *. The kind of
Either and of the type parameter requested by the
Functor class are not compatible, so we need to partially apply
Either type, to obtain a new type having kind
* -> *.
For sake of completeness (and for those of you that know Haskell syntax), the partial application to make
Either a member of
Functor results in something like the following. Here, we mapped the case of the right type parameter.
In conclusion, Kinds let us know how to use type classes, and type constructors, to obtain concrete type, sharing their behavior.
Our journey through an edulcorated extract of type theory has finished. We saw many different concepts along the way. Many of these should be more detailed, but one post would not have been enough. We should now understand that we need kinds only when we have to manage Higher Kinded Types in Scala or Haskell (or in any programming language that provides a version of such types).
Long story short — Kinds help you to understand which type can be a member of a type class.
Sorry for the long, boring post. Here is a lambda potato.
- Scala: Types of a higher kind
- Making Our Own Types and Typeclasses
- Functors, Applicative Functors, and Monoids
- Kind (type theory)
- Correct terminology in type theory: types, type constructors, kinds/sorts and values
- Type classes in Scala
- Can type constructors be considered as types in functional programming languages?
Published at DZone with permission of Riccardo Cardin , DZone MVB. See the original article here.
Opinions expressed by DZone contributors are their own.