Type-level functions are called type families. They are really not just another function. But if you appreciate that beauty, check out a dependently types language like Idris where normal functions can be used on the type-level as well. So you might have a vector type with a length computed by a complicated expression.