|By Edwin Brady
In this article,excerpted from Type-Driven Development from Idris, I will introduce you to some standard basic types and functions for working with numbers of various forms, characters and strings.
Idris provides some standard basic types and functions, for working with numbers of various forms, characters, and strings. In this article, I will give an overview of these, along with some examples. These basic types are defined in the Prelude, which is a collection of standard types and functions automatically imported by every Idris program.
I’ll give several example expressions throughout this article. For many, it may seem fairly clear what they should do. Nevertheless, instead of simply reading them and nodding, I strongly recommend typing in the examples at the Idris REPL, because you will learn the syntax much more easily by using it than you will merely by reading it!
On the way, we’ll also encounter a couple of useful REPL features which allow us to store the results of calculations at the REPL.
The types and functions I’ll discuss are defined in the Prelude. The Prelude is Idris’ standard library, always available at the REPL and automatically imported by every Idris program. With the exception of some primitive types and operations, everything in the Prelude is written in Idris itself.
Numeric Types and Values
Idris provides several basic numeric types. These include:
Int, which is a fixed width signed integer type. It is guaranteed to be at least 31 bits wide, but the exact width is system-dependent.
Integer, which is an unbounded signed integer type. Unlike
Int, there is no limit to the size of the numbers that can be represented other than your machine’s memory, but they are more expensive in terms of performance and memory usage.
Nat, which is an unbounded unsigned integer type. This is very often used for sizes and indexing of data structures since they can never be negative. We will see much more of
Double, which is a double precision floating point type.
We can use standard numeric literals for values of each of these types. For example, the literal
333 can be of type
Int Integer Nat Double, , or . The literal
333.0 can only be of type
Double, due to the explicit decimal point. We can try some simple calculations at the REPL:
Idris> 6 + 3 * 12
Idris> 6.0 + 3 * 12
42.0 : Double
Note that Idris will treat a number as
Integer by default, unless there is some context, and both operands must be the same type. Therefore, in the second expression above, the literal
6.0 can only be a
Double, so the whole expression is a
12 are also treated as
The most recent result at the REPL can always be retrieved, and used in further calculations, using the special value
It is also possible to bind expressions to names at the REPL, using the
When an expression, such as
6 + 3 * 12, can be one of several types we can make the type explicit with the notation
the type expression, to say that
type is the required type of
expression. For example:
Idris> 6 + 3 * 12
42 : Integer
Idris> the Int (6 + 3 * 12)
Idris> the Double (6 + 3 * 12)
42.0 : Double
Type Conversions using cast
Arithmetic operators work on any numeric types, but both inputs and the output must have the same type. Sometimes, therefore, we need to convert between types. Let’s say we’ve defined an
Integer and a
Double at the REPL:
Idris> :let integerval = 6 * 6
Idris> :let doubleval = 0.1
36 : Integer
0.1 : Double
If we try to add
doubleval, Idris will complain that they are not the same type:
Idris> integerval + doubleval
(input):1:8-9:When checking an application of function Prelude.Classes.+:
Type mismatch between
Double (Type of doubleval)
Integer (Expected type)
To fix this, we can use the
cast function, which converts its input to the required type, as long as that conversion is valid. Here, we can
cast Integer the to a
Idris> cast integerval + doubleval
36.1 : Double
Idris supports casting between all of the primitive types, and it is possible to add user defined casts. Note that some casts may lose information, though, such as casting a
Double to an
Specifying the target of a
You can also use
Characters and Strings
Idris also provides Unicode characters and strings as primitive types, along with some useful primitive functions for manipulating these.
- Character literals (of type
Char) are written in single quotation marks, for example
- String literals (of type
String) are written in double quotation marks, for example
Like many other languages, Idris supports special characters in character and string literals using escape sequences, beginning with a backslash. For example, a new line character is indicated using
Idris> :t '\n'
'\n' : Char
Idris> :t "Hello world!\n"
"Hello world!\n" : String
The most common escape sequences are:
\'for a literal single quote
\"for a literal double quote
\\for a literal backslash
\nfor a new line character
\tfor a tab character
The Prelude defines several useful functions for manipulating
Strings. We can see some of these in action at the REPL:
Idris> length "Hello!"
6 : Nat
Idris> reverse "drawer"
"reward" : String
Idris> substr 6 5 "Hello world"
"world" : String
Idris> "Hello" ++ " " ++ "World"
"Hello World" : String
These functions are:
length, which gives the length of its argument, as a
Stringcannot have a negative length
reverse,which returns a reversed version of its input
substr, which returns a substring of an input string, given a position to start at and the desired length of the substring.
- An operator
++, which concatenates two
Notice the syntax of the function calls. In Idris, functions are separated from their arguments by whitespace. If the argument is a complex expression, then it must be bracketed. For example:
Idris> length ("Hello" ++ " " ++ "World")
11 : Nat
Calling functions by separating the arguments with spaces may seem strange at first. There’s a good reason for it, though, as we’ll discover when we look at function types later in this chapter. In short, it makes manipulating functions much more flexible.
Idris provides a type
Bool, for representing truth values. A
Bool can take the value
True False or . The operators
|| represent logical And and Or respectively:
Idris> True && False
False : Bool
Idris> True || False
True : Bool
The usual comparison operators ( ,
< <= == /= > >=, , , , ) are available:
Idris> 3 > 2
True : Bool
Idris> 100 == 99
False : Bool
Idris> 100 /= 99
True : Bool
The inequality operator in Idris is
There is also an
if...then...else construct. This is an expression, so must always include both a
then branch and an
else branch. For example, we can write an expression which evaluates to a different message, as a
String, depending on the length of a word:
Idris> :let word = "programming"
Idris> if length word > 10 then "What a long word!" else "Short word"
"What a long word!" : String
And that is your introduction to some basic types and a simple control structure. You should be ready to begin defining functions!