Over a million developers have joined DZone.
{{announcement.body}}
{{announcement.title}}

It's a Kind of Magic: Kinds in Type Theory

DZone's Guide to

It's a Kind of Magic: Kinds in Type Theory

The type theory is some Kind of magic.

· Java Zone ·
Free Resource

Get the Edge with a Professional Java IDE. 30-day free trial.

I am not an expert of functional programming, nor the type theory. I am currently trying to enter the world of Haskell after I mess around in the Scala world for a while. When I first read about Kinds, I remember I was surprised, and a little bit scared. Is it possible that types have types? If so, what does this mean? In this little introductory post, I will try to explain what I understood during my journey through Kinds in Haskell.

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<Integer>List<String>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:

trait Functor[F[_]] {
  def map[A, B](fa: F[A])(f: A => B): F[B]
}


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. List[T]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.

class Functor f where  
    fmap :: (a -> b) -> f a -> f b 


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

Values

Starting from the beginning, we found values. Values are the information or data that our programs evaluate. Examples of values are things like 1"hello"true3.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

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 boole: bool; it means that it can have only two values — true or false.

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.

Type Constructors

As we previously said, there can be “types” that are parametricGeneric types uses type parameters to exploit this feature. So, we can define a “type” using a type parameter such as List[T], where 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. List[T]Map[K, V]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.

class Person(name: String, surname: String) = {
    //...
}


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. ListOption, 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 :k.

ghci> :k List  
List :: * -> *  


However, a question should arise into your mind: what the hell are Kinds useful for? The answer is typeclasses.

Type Classes

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.

Our 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 Show.

trait Show[A] {
  def show(a: A): String
}


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 deriving keyword.

data List a = Empty | Cons a (List a) deriving (Show, Read, Eq, Ord) 


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 instance and where, to support type classes.

instance Functor Maybe where  
    fmap f (Just x) = Just (f x)  
    fmap f Nothing = Nothing 


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 fmap applies 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 ListMaybe (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 applyEither 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.

instance Functor (Either a) where  
    fmap f (Right x) = Right (f x)  
    fmap f (Left x) = Left x  


In conclusion, Kinds let us know how to use type classes, and type constructors, to obtain concrete type, sharing their behavior.

Conclusion

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.

My sweet lambda-potato

References

Get the Java IDE that understands code & makes developing enjoyable. Level up your code with IntelliJ IDEA. Download the free trial.

Topics:
java ,kind ,type ,kinds ,types ,functional programming ,fp ,haskell ,scala ,hkt

Published at DZone with permission of

Opinions expressed by DZone contributors are their own.

{{ parent.title || parent.header.title}}

{{ parent.tldr }}

{{ parent.urlSource.name }}