Previous | Contents | Next

The basics: primitive types and operations

Edwin Brady

Idris defines primitive types Int, Char, Float and String (although Float is not yet implemented). There are also Bools, with values True and False. We can declare some constants with these types:

x   = 42;                -- Int
foo = "Sausage machine"; -- String
bar = 'Z';               -- Char
quux = False;            -- Bool

A library file prelude.idr is automatically imported by every Idris program, including facilities for IO, arithmetic, data structures and various common functions. The prelude defines several arithmetic and comparison operators, which we can use at the Idris prompt. Evaluating things at the prompt gives an answer, and the type of the answer:

Idris> 6*6+6
42 : Int
Idris> x == 6*6+6
True : Bool

Boolean expressions can be tested with the if...then...else construct

Idris> if (x==6*6+6) then "The answer!" else "Not the answer"
"The answer!" : String

The string.idr library allows some conversions between primitive types and Strings, as well as some primitive operations on Strings. We can import the library with an include declaration (this is likely to change - Idris needs a module system at some point.)

include "string.idr";

This library includes showInt to convert an Int to a String, strLen to get the length of a string, among other things. We can try these at the Idris prompt:

Idris> showInt x
"42" : String
Idris> strLen (showInt x)
2 : Int

Source for this chapter

Previous | Contents | Next