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

NOTE

The Prelude

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 Nat later.
  • 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 
: Integer 
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 Double, and 3 and 12 are also treated as Doubles.

TIP

REPL results

The most recent result at the REPL can always be retrieved, and used in further calculations, using the special value it.

Idris> 6 + 3 * 12
42 : Integer
Idris> it * 2
84 : Integer

It is also possible to bind expressions to names at the REPL, using the :let command:

Idris> :let x = 100
Idris> x
100 : Integer
Idris> :let y = 200.0
Idris> y
200.0 : Double

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) 
: Int 
Idris> the Double (6 + 3 * 12) 
42.0 : Double 
           

NOTE

theexpressions

In fact, the is not built-in syntax, but an ordinary Idris function, defined in the Prelude, which takes advantage of first-class types.

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 
Idris> integerval 
36 : Integer 
Idris> doubleval 
0.1 : Double

 If we try to add integerval and 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)
         and
                 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 Double:

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 Integer!

NOTE

Specifying the target of a cast

You can also use the to specify which type you want to cast to. For example:

Idris> the Integer (cast 9.9) 9 : Integer Idris> the Double (cast (4 + 4)) 8.0 : Double            

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 'a'.
  • String literals (of type String) are written in double quotation marks, for example "Hello world!"

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 \n:

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
  • \n for a new line character
  • \t for 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 Nat since a String cannot 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 Strings.

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

NOTE

Function syntax

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.

Booleans

Idris provides a type Bool, for representing truth values. A Bool can take the value True False or . The operators && and || 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

NOTE

Inequality

The inequality operator in Idris is /=, which follows Haskell syntax, rather than != which would follow the syntax of C and Java-like languages.

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!