Save 37% on Type-Driven Development with Idris. Just enter code fccbrady into the discount code box at checkout at manning.com.

One of the most fundamental features of Idris is that types and expressions are part of the same language—you use the same syntax for both. Expressions can appear in types. For example, in the type of append on Vect, we’ve n and m (both Nats), and the resulting length is n + m:

 
 append : Vect n elem -> Vect m elem -> Vect (n + m) elem
 

Here, n, m, and n + m all have type Nat, which can also be used in ordinary expressions. Similarly, you can use types in expressions and therefore write functions that calculate types. Two common situations where you might want to do this:

To give more meaningful names to composite types—For example, if you’ve a type (Double, Double) representing a position as a 2D coordinate, you might prefer to call the type Position to make the code more readable and self-documenting.

To allow a function’s type to vary based on contextual information—For example, the type of a value returned by a database query varies depending on the database schema and the query itself.

In the first case, you can define composite types, which give alternative type synonyms names to types. In the second case, you can define type-level functions (synonyms are a special case) that calculate types from some input. In this article, we’ll look at both.

Type synonyms: giving informative names to complex types

Let’s say you’re writing an application that deals with complex polygons, such as a drawing application. You might represent a polygon as a vector of the coordinates of each corner. A triangle, for example, might be initialized as follows:

 
 tri : Vect 3 (Double, Double) 
 tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)] 
  
 

The type, Vect 3 (Double, Double) says exactly what the form of the data will be, which is useful to the machine, but it doesn’t give any indication as to the purpose of the data. Instead, you can refine the type using a type synonym for a position represented as a 2D coordinate:

 
 Position : Type 
 Position = (Double, Double)
 

Here you’ve a function called Position that takes no arguments and returns a Type. This is an ordinary function; there’s nothing special about the way it’s declared or implemented. Now, anywhere you can use a Type, you can use Position to calculate that type. For example, the triangle can be defined as follows with a refined type:

 
 tri : Vect 3 Position 
 tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]
 

This kind of function is a type synonym because it provides an alternative name for some other type.

NOTE Naming convention: By convention, we usually use an initial capital letter for functions that are intended to compute types.

Because they’re ordinary functions, they can also take arguments. For example, the following listing shows how you can use type synonyms to more clearly express that the Vect is intended to represent a polygon.

 
 import Data.Vect 
   
 Position : Type 
 Position = (Double, Double)             ❶    
 Polygon : Nat -> Type 
 Polygon n = Vect n Position             ❷ 
    tri : Polygon 3 
 tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]
 

❶   A type synonym for describing positions as (x, y) coordinates

❷   A type synonym for describing polygons with n corners

Because Polygon is an ordinary function, you can evaluate it at the REPL:

 
 *TypeSynonyms> Polygon 3 
 Vect 3 (Double, Double) : Type
 

Also, notice that if you evaluate tri at the REPL, Idris will display tri’s type in the evaluated form. Evaluation at the REPL evaluates both the expression and the type:

 
 *TypeSynonyms> tri 
 [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)] : Vect 3 (Double, Double)
 

Using :t displays tri’s types in its original form:

 
 *TypeSynonyms> :t tri 
 Polygon 3
 

Finally, you can see what happens when you try to define tri interactively using an expression search in Atom. Enter the following into an Atom buffer, along with the previous definition of Polygon:

 
 tri : Polygon 3 
 tri = ?tri_rhs
 

The interactive editing tools and expression search are aware of how type synonyms are defined, and if you try an expression search on tri_rhs, you’ll get the same result as if the type were written directly as Vect 3 (Double, Double):

 
 tri : Polygon 3 
 tri = [(?tri_rhs1, ?tri_rhs2), (?tri_rhs3, ?tri_rhs4), (?tri_rhs5, ?tri_rhs6)]
 

The type synonyms defined in this section, Position and Polygon, are ordinary functions that happen to be used to compute types. This gives you a lot of flexibility in how you describe types, as you’ll see in the rest of this article.

Type-level functions with pattern matching

Type synonyms are a special case of type-level functions, which are functions that can be used anywhere Idris is expecting a Type. Nothing special about type-level functions exist as far as Idris is concerned; they’re ordinary functions that happen to return a Type, and they can use the language constructs available elsewhere. Nevertheless, it’s useful to consider them separately, to see how they work in practice.

Because type-level functions are ordinary functions that return a type, you can write them by case-splitting. For example, listing 2 shows a function that calculates a type from a Boolean input.

 
 StringOrInt : Bool -> Type 
 StringOrInt False = String 
 StringOrInt True = Int
 

Using this, you can write a function where the return type is calculated from or depends on an input. Using StringOrInt, you can write functions that return either type, depending on a Boolean flag.

As a small example, you can write a function that takes a Boolean input and returns the string "Ninety four" if it’s False, or the integer 94 if it’s True. Begin with the type:

NOTE Dependent pattern matching: The getStringOrInt example illustrates a technique often useful when programming with dependent types: dependent pattern matching. This refers to a situation where the type of one argument to a function can be determined by inspecting the value of (by case-splitting) another.

Type-level functions can be used anywhere a Type is expected, meaning they can be used in place of argument types too. For example, you can write a function that converts either a String or an Int to a canonical String representation, based on a Boolean flag. This function behaves as follows:

You can define this function with the following steps:

The simple examples in this section, getStringOrInt and valToString, illustrate a technique that can be used more widely in practice.

There’s more that you can achieve with type-level expressions. The fact that types are first class means not only that types can be computed like any other value, but also that any expression form can appear in types.

Using case expressions in types

Any expression that can be used in a function can also be used at the type level, and vice versa. For example, you can leave holes in types as your understanding of a function’s requirements develops, or you can use more complex expression forms such as case. Let’s briefly look at how this can work, by using a case expression in the type of valToString instead of a separate StringOrInt function.

That’s all for now.

Hopefully you have a better understanding of type-level functions after reading this article. For more information on Idris, check out the whole book on liveBook here.