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 type-level functions in Idris and how expressions can appear in types.

Save 37% off Type-Driven 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 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.

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.

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.

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:

  1. (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
     
    
  2. (Define) Because isInt appears in the required type for getStringOrInt_rhs, case-splitting on isInt will cause the expected return type to change based on the specific value of isInt for each case. Case-splitting on isInt leads to this:

     
     getStringOrInt : (isInt : Bool) -> StringOrInt isInt 
     getStringOrInt False = ?getStringOrInt_rhs_1 
     getStringOrInt True = ?getStringOrInt_rhs_2
     
    
  3. (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.

  4. (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 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:

  • If the input is a String, it returns the String with leading and trailing space removed using trim.

  • If the input is an Int, it converts the input to a String using cast.

You can define this function with the following steps:

  1. (Type) Begin by writing a type for valToString, again using StringOrInt, 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
     
    
  2. (Define) You can define this by case-splitting on isInt. The type of y is calculated from isInt, and if you case-split on isInt, you should see refined types for y in each resulting case:

     
     valToString : (isInt : Bool) -> StringOrInt isInt -> String 
     valToString False y = ?valToString_rhs_1 
     valToString True y = ?valToString_rhs_2
     
    
  3. (Type) Inspecting the types of valToString_rhs_1 and valToString_rhs_2 shows how the type of y is refined in each case:

     
       y : String 
     -------------------------------------- 
     valToString_rhs_1 : String 
          y : Int 
     -------------------------------------- 
     valToString_rhs_2 : String
     
    
  4. (Refine) To complete the definition, fill in the right side to convert y to a trimmed String, if it was a String, or a string representation of the number if it was an Int:

     
     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 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.

  1. (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
     
    
  2. (Define) Even though you’ve an incomplete type, you can proceed with the definition by case-splitting on isInt, because you know that isInt is a Bool:

     
     valToString : (isInt : Bool) -> ?argType -> String 
     valToString False y = ?valToString_rhs_1 
     valToString True y = ?valToString_rhs_2
     
    
  3. (Type) Inspecting the types of valToString_rhs_1 and valToString_rhs_2 will reveal that you don’t know the type of y yet:

     
       y : ?argType 
     -------------------------------------- 
     valToString_rhs_1 : String
     
    
  4. (Refine) At this stage, you need to refine the type with more details of ?argType. You can fill in ?argType with a case expression:

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

     
     valToString : (isInt : Bool) -> (case isInt of 
                                           case_val => ?argType) -> String 
     valToString False y = ?valToString_rhs_1 
     valToString True y = ?valToString_rhs_2
     
    
  6. (Refine) Case-splitting gives you the two case_val possible values isInt 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 with String and ?argType_2 with Int:

     
     valToString : (isInt : Bool) -> (case isInt of 
                                           False => String 
                                           True => Int) -> String 
     valToString False y = ?valToString_rhs_1 
     valToString True y = ?valToString_rhs_2
     
    
  7. (Type) Inspecting ?valToString_rhs_1 and ?valToString_rhs2 now shows you the new types for the input y, calculated from the first argument:

     
       y : String 
     -------------------------------------- 
     valToString_rhs_1 : String 
       
       y : Int 
     -------------------------------------- 
     valToString_rhs_2 : String
     
    
  8. (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
     
    

 

Totality and type-level functions

That’s all for now. Hopefully you have a better understanding of type-level functions after reading this article. For more information on Idris, download the first chapter of Type-Driven Development with Idris.