By Edwin Brady In Idris, types and expressions are part of the same language and you use the same syntax for both. This article talks about typelevel functions in Idris and how expressions can appear in types. Save 37% off TypeDriven Development with Idris with code fccbrady 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 Nat
s), 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 selfdocumenting.
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 typelevel 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.
Listing 1 Defining a polygon using type synonyms (TypeSynonym.idr)
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.
Typelevel functions with pattern matching
Type synonyms are a special case of typelevel functions, which are functions that can be used anywhere Idris is expecting a Type
. Nothing special about typelevel 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 typelevel functions are ordinary functions that return a type, you can write them by casesplitting. For example, listing 2 shows a function that calculates a type from a Boolean input.
Listing 2 A function that calculates a type from a Bool
(TypeFuns.idr)
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:

(Type) Begin by giving a type declaration, using
StringOrInt
:getStringOrInt : (isInt : Bool) > StringOrInt isInt getStringOrInt isInt = ?getStringOrInt_rhs
If you look at the type of
getStringOrInt_rhs
now, you’ll see this:isInt : Bool  getStringOrInt_rhs : StringOrInt isInt

(Define) Because
isInt
appears in the required type forgetStringOrInt_rhs
, casesplitting onisInt
will cause the expected return type to change based on the specific value ofisInt
for each case. Casesplitting onisInt
leads to this:getStringOrInt : (isInt : Bool) > StringOrInt isInt getStringOrInt False = ?getStringOrInt_rhs_1 getStringOrInt True = ?getStringOrInt_rhs_2

(Type) Looking at the types of the newly created holes, you can see how the expected type is changed in each case:
 getStringOrInt_rhs_1 : String  getStringOrInt_rhs_2 : Int
In getStringOrInt_rhs_1, the type is refined to StringOrInt False because the pattern for isInt is False, which evaluates to String. Then in getStringOrInt_rhs_2, the type is refined to StringOrInt True, which evaluates to Int.

(Refine) To complete the definition, you need to provide values of different types in each case:
getStringOrInt : (isInt : Bool) > StringOrInt isInt getStringOrInt False = "Ninety four" getStringOrInt True = 94
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 casesplitting) another.
Typelevel 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:

If the input is a
String
, it returns theString
with leading and trailing space removed usingtrim
. 
If the input is an
Int
, it converts the input to aString
usingcast
.
You can define this function with the following steps:

(Type) Begin by writing a type for
valToString
, again usingStringOrInt
, but this time to calculate the input type:valToString : (isInt : Bool) > StringOrInt isInt > String valToString isInt y = ?valToString_rhs
Inspecting the type of
valToString_rhs
, you’ll see the following:isInt : Bool y : StringOrInt isInt  valToString_rhs : String

(Define) You can define this by casesplitting on
isInt
. The type ofy
is calculated fromisInt
, and if you casesplit onisInt
, you should see refined types fory
in each resulting case:valToString : (isInt : Bool) > StringOrInt isInt > String valToString False y = ?valToString_rhs_1 valToString True y = ?valToString_rhs_2

(Type) Inspecting the types of
valToString_rhs_1
andvalToString_rhs_2
shows how the type ofy
is refined in each case:y : String  valToString_rhs_1 : String y : Int  valToString_rhs_2 : String

(Refine) To complete the definition, fill in the right side to convert
y
to a trimmedString,
if it was aString
, or a string representation of the number if it was anInt
:valToString : (isInt : Bool) > StringOrInt isInt > String valToString False y = trim y valToString True y = cast y
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 typelevel 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.

(Type) Start by giving a type for
valToString
, but because you don’t immediately know the input type, you can leave a hole:valToString : (isInt : Bool) > ?argType > String

(Define) Even though you’ve an incomplete type, you can proceed with the definition by casesplitting on
isInt
, because you know thatisInt
is aBool
:valToString : (isInt : Bool) > ?argType > String valToString False y = ?valToString_rhs_1 valToString True y = ?valToString_rhs_2

(Type) Inspecting the types of
valToString_rhs_1
andvalToString_rhs_2
will reveal that you don’t know the type ofy
yet:y : ?argType  valToString_rhs_1 : String

(Refine) At this stage, you need to refine the type with more details of
?argType
. You can fill in?argType
with acase
expression:valToString : (isInt : Bool) > (case _ of case_val => ?argType) > String valToString False y = ?valToString_rhs_1 valToString True y = ?valToString_rhs_2

(Refine) Remember that when Idris generates a
case
expression, it leaves an underscore in place of the value thecase
expression will branch on. You’ll need to fill this in before the program will compile. You can compute the argument type from the inputisInt
:valToString : (isInt : Bool) > (case isInt of case_val => ?argType) > String valToString False y = ?valToString_rhs_1 valToString True y = ?valToString_rhs_2

(Refine) Casesplitting gives you the two
case_val
possible valuesisInt
can take:valToString : (isInt : Bool) > (case isInt of False => ?argType_1 True => ?argType_2) > String valToString False y = ?valToString_rhs_1 valToString True y = ?valToString_rhs_2
You can then complete the type in the same way as your implementation of
StringOrInt
, refining?argType_1
withString
and?argType_2
withInt
:valToString : (isInt : Bool) > (case isInt of False => String True => Int) > String valToString False y = ?valToString_rhs_1 valToString True y = ?valToString_rhs_2

(Type) Inspecting
?valToString_rhs_1
and?valToString_rhs2
now shows you the new types for the inputy
, calculated from the first argument:y : String  valToString_rhs_1 : String y : Int  valToString_rhs_2 : String

(Refine) Finally, now that you know the type of the input
y
in each case, you can complete the definition as before:valToString : (isInt : Bool) > (case isInt of False => String True => Int) > String valToString False y = trim y valToString True y = cast y
That’s all for now. Hopefully you have a better understanding of typelevel functions after reading this article. For more information on Idris, download the first chapter of TypeDriven Development with Idris.