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
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
. for example, think of the
type. there is a
that one should provide to the compiler when dealing with a
to obtain concrete and usable types. then, we have
, and so on.
what about if we do not provide a concrete type as the value of the type parameter? what about
, for example? well, the java compiler transforms this type into the more safer
, warning you that you are using
in a non-generic way. and yes,
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,
, mean? it means that
(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.
, 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 are the information or data that our programs evaluate. examples of values are things like
, and so on. each value in a program belongs to a
. a value can be assigned to a name, that is called a
give information to our program about how to treat values at runtime. in other terms, they set
to values. saying that a variable has the type
; 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
, which takes two integers and returns their sum, has type
(int, int) => int
in scala or
int -> int -> int
as we previously said, there can be “types” that are
to exploit this feature. so, we can define a “type” using a type parameter such as
can 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
is very similar to the behavior of a
. 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,
take as input a type to create new types.
, and so on are all classified as type constructors. in java, we call them
. in c++, they call them
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)
are the types of objects that are related to types, more or less. a kind is more of an
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
. so, it takes a type in input to produce a concrete type. it is similar to a function having only one parameter.
, and so on, 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
in java. in scala, it is obtained using a
. in haskell, there is a dedicated construct that is the
construct. in haskell, there are type classes for a lot of features that a type could have: the
type class marks all the types that be checked for equality; the
type class marks all the types that can be compared; the
type class is used by the types that can be pretty-printed in the standard output.
that we defined earlier is, in fact, a type class. the
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
type class by the
in scala). as you can see, there are dedicated constructs of the language, as
, 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
type class definition, the type
must have a kind
* -> *
, which means that the type class requests types that take only one parameter. the function
to a type
and a type
, which are concrete types in absence of any other indication. as previously said, such kinds of objects are similar to the
in scala, and
what if we want to apply such type class to the
type constructor? both in haskell and scala, it is defined as
, defining two type parameters, respectively
. for the definition we gave of a kind,
* -> * -> *
. the kind of
and of the type parameter requested by the
class are not compatible, so we need to
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
a member of
results in something like the following. here, we mapped the case of the
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.