By Edwin Brady

Save 37% off Type-Driven Development with Idris with code fccbrady.

 

Idris programs can contain holes, which stand for parts of a function definition that haven’t yet been written. This is one way in which programs can be developed interactively: you write an incomplete definition containing holes, check the types of the holes to see what Idris expects in each, and then continue by filling in the holes with more code. Additional ways exist in which Idris can help you by integrating interactive development features with a text editor:

  • Add definitions—Given a type declaration, Idris can add a skeleton definition of a function that satisfies that type.
  • Case analysis—Given a skeleton function definition with arguments, Idris can use the types of arguments to help define the function by pattern matching.
  • Expression search—Given a hole with a precise enough type, Idris can try to find an expression that satisfies the hole’s type, refining the definition.

In this article, we’ll begin writing some complex Idris functions, using its interactive editing features to develop those functions, step by step, in a type-directed way. We’ll use the Atom text editor, because there’s an extension available for editing Idris programs, which can be installed directly from the default Atom distribution. The rest of this article assumes you have the interactive Idris mode up and running.


Interactive command summary

Interactive editing in Atom involves several keyboard commands in the editor, which are summarized in table 1.

NOTE Command mnemonics for each command, the shortcut in Atom is to press Ctrl, Alt, and the first letter of the command.


Table 1 Interactive editing commands in Atom

Shortcut Command Description

Ctrl-Alt-A Add definition Adds a skeleton definition for the name under the cursor
Ctrl-Alt-C Case split Splits a definition into pattern matching clauses for the name under the cursor
Ctrl-Alt-D Documentation Displays documentation for the name under the cursor
Ctrl-Alt-L Lift hole Lifts a hole to the top level as a new function declaration
Ctrl-Alt-M Match Replaces a hole with a case expression that matches on an intermediate result
Ctrl-Alt-R Reload Reloads and type-checks the current buffer
Ctrl-Alt-S Search Searches for an expression that satisfies the type of the hole name under the cursor
Ctrl-Alt-T Type-check name Displays the type of the name under the cursor

 

Defining functions by pattern matching

The function definitions we’ve looked at involve a single equation to define that function’s behavior. For example, this function calculates the lengths of every word in a list:

 

allLengths : List String -> List Nat
allLengths strs = map length strs

 

Here you used functions defined in the Prelude (map and length) to inspect the list. At some stage, though, you’re going to need a more direct way to inspect values. After all, functions like map and length need to be defined somehow!

In general, you define functions by pattern matching on the possible values of inputs to a function. For example, you can define a function to invert a Bool as follows:

invert : Bool -> Bool
invert False = True
invert True = False

 

The possible inputs of type Bool are True and False, and here you’ve implemented invert by listing the possible inputs and giving the corresponding outputs. Patterns can also contain variables, as illustrated by the following function, which returns “Empty” if given an empty list or “Non-empty” followed by the value of the tail if given a non-empty list:

 

describeList : List Int -> String
describeList [] = "Empty"
describeList (x :: xs) = "Non-empty, tail = " ++ show xs

 

Figure 1 illustrates how the patterns are matched in describeList for the inputs [1] (which is syntactic sugar for 1 :: []) and [2,3,4,5] (which is syntactic sugar for 2 :: 3 :: 4 :: 5 :: []).


Figure 1 Matching the pattern (x :: xs) for inputs [1] and [2,3,4,5]


NOTE: Naming conventions for lists

Conventionally, when working with lists and list-like structures, Idris programmers use a name ending in “s” (to suggest a plural), and then use its singular to refer to individual elements. If you’ve a list called “things”, you might refer to an element things of the list as thing.

A function definition consists of one or more equations matching the possible inputs to that function. You can see how this works for lists if you implement allLengths by inspecting the list directly, instead of using map. This is shown in listing 1.


Listing 1 Calculating word lengths by pattern matching on the list (WordLength.idr)

allLengths : List String -> List Nat
allLengths [] = []                                          ❶
allLengths (x :: xs) = length x :: allLengths xs            ❷

 

❶ If the input list is empty, the output list will also be empty.

❷ If the input list has a head element x and a tail xs, the output list will have the length of x as the head and then recursively a list of the lengths of xs as the tail.


To see in more detail how this definition is constructed, let’s build it interactively in Atom. Each step can be broadly characterized as Type (creating or inspecting a type), Define (making a definition or breaking it down into separate clauses), or Refine (improving a definition by filling in a hole or making its type more precise).

(Type) First, start up Atom and create a WordLength.idr file containing the type declaration for allLengths with only the following:

 

allLengths : List String -> List Nat

 

You should also start up an Idris REPL in a separate terminal to allow you to type-check and test your definition:

 

$ idris WordLength.idr
     ____ __ _
    / _/___/ /____(_)____
    / // __ / ___/ / ___/ Version 1.0
  _/ // /_/ / / / (__ ) http://www.idris-lang.org/
 /___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Holes: Main.allLengths

*WordLength>

 

(Define) In Atom, move the cursor over the name allLengths and press Ctrl-Alt-A. This will add a skeleton definition, and your editor buffer should now contain the following:

 

allLengths : List String -> List Nat
allLengths xs = ?allLengths_rhs

 

The skeleton definition is always a clause with the appropriate number of arguments listed on the left side of the =, and with a hole on the right side. Idris uses various heuristics to choose initial names for the arguments. By convention, Idris chooses default names of xs, ys, or zs for Lists.

(Type) You can check the types of holes in Atom by pressing Ctrl-Alt-T with the cursor over the hole you want to check. If you check the type of the allLengths_rhs hole you should see this:

 

  xs : List String
--------------------------------------
allLengths_rhs : List Nat

 

(Define) You’ll write this definition by inspecting the list argument, named xs, directly. This means that for every form the list can take, you need to explain how to measure word lengths when it’s in that form. To tell the editor that you want to inspect the first argument, press Ctrl-Alt-C in Atom with the cursor over the variable xs in the first argument position. This expands the definition to give the two forms that the argument xs could take:

allLengths : List String -> List Nat
allLengths [] = ?allLengths_rhs_1
allLengths (x :: xs) = ?allLengths_rhs_2

 

These are the two canonical forms of a list. Every list must be in one of these two forms: it can either be empty (in the form []), or it can be non-empty containing a head element and the rest of the list (in the form (x :: xs)). It’s a good idea to rename x and xs to something more meaningful than these default names:

 

allLengths : List String -> List Nat
allLengths [] = ?allLengths_rhs_1
allLengths (word :: words) = ?allLengths_rhs_2

 

In each case, there’s a new hole on the right side to fill in. You can check the types of these holes, which gives the expected return type and the types of any local variables. For example, if you check the type of allLengths_rhs_2, you’ll see the types of the local variables word and words as well as the expected return type:

 

  word : String
  words : List String
--------------------------------------
allLengths_rhs_2 : List Nat

 

(Refine) Idris has informed you which patterns are needed. Your job is to complete the definition by filling in the holes on the right side. In the case where the input is the empty list, the output is also the empty list, because there are no words for which to measure the length:

 

allLengths [] = []

 

(Refine) In the case where the input is non-empty, there is a word as the first element (word) followed by the remainder of the list (words). You need to return a list with the length of word as its first element. For the moment, you can add a new hole (?rest) for the remainder of the list:

 

allLengths : List String -> List Nat
allLengths [] = []
allLengths (word :: words) = length word :: ?rest

 

You can even test this incomplete definition at the REPL. Note that the REPL doesn’t reload files automatically, as it runs independently of the interactive editing in Atom, and you’ll need to reload explicitly using the :r command:

 

*WordLength> :r
Type Checking ./WordLength.idr
Holes: Main.rest
*WordLength> allLengths ["Hello", "Interactive", "Editors"]
5 :: ?rest : List Nat

 

For the hole rest, you need to calculate the lengths of the words in words. You can do this with a recursive call to allLengths, to complete the definition:

 

allLengths : List String -> List Nat
allLengths [] = []
allLengths (word :: words) = length word :: allLengths words

 

You now have a complete definition, which you can test at the REPL after reloading:

 

*WordLength> :r
Type Checking ./WordLength.idr
*WordLength> allLengths ["Hello", "Interactive", "Editors"]
[5, 11, 7] : List Nat

 

It’s also a good idea to check whether Idris believes the definition is total.

 

*WordLength> :total allLengths
Main.allLengths is Total

 


Totality checking

When Idris has successfully type-checked a function, it also checks whether it believes the function is total. If a function is total, it’s guaranteed to produce a result for any well-typed input, in finite time. Thanks to the halting problem, Idris can’t decide in general whether a function is total, but by analyzing a function’s syntax it can decide that a function is total in many specific cases.

Totality checking is a big topic in and of itself and needs its own article. For the moment, it’s sufficient to know that Idris will consider a function total if it has clauses that cover all possible well-typed inputs and all recursive calls converge on a base case. The definition of totality also allows interactive programs that run indefinitely, such as servers and interactive loops, provided that they continue to produce intermediate results in finite time.


Idris believes this is the total because there are clauses for all possible well-typed inputs, and the argument to the recursive call to allLengths is smaller (closer to the base case) than the input.

 

For more information on Type-Driven Development with Idris, download the free first chapter and don’t forget to use code fccbrady to save 37%.