It's using the type system as a language in which to perform computations. For example, you can do type level programming in c++. As an easy example, 'std::list

It's using the type system as a language in which to perform computations. For example, you can do type level programming in c++. As an easy example, 'std::list<x>' is a function that maps the type 'x' into a type that represents a linked list of 'x's. You can type systems compute many interesting invariants. For example, in a language like Idris, you can define the type of arrays of length 'n' and with elements of type 'a' as 'Vector n a'. Then, if you want to append two arrays together, you can use a function: append : (x : Vector m a) -> (y : Vector n a) -> Vector (m + n) a The '+' operator here is a function that takes two types ('n' and 'm') and returns another type that represents the arithmetic sum of 'n' and 'm'.