 |
From Type-Driven Development with Idris by Edwin Brady 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. This article assumes you have the interactive Idris mode up and running.
|
Save 37% on Type-Driven Development with Idris. Just enter code fccbrady into the discount code box at checkout at manning.com.
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.
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.
If you want to know more about the book, check it out on liveBook here.