Home > Posts > Beginner's Guide to Idris

Beginner's Guide to Idris

  ·   15 min read

Introduction to Idris #

What is Idris? #

Idris is a purely functional programming language with dependent types. This means it combines the benefits of functional programming (like immutability, referential transparency, and higher-order functions) with the power of dependent types, allowing you to express complex program properties and prove them correct within the type system. Unlike languages like Haskell, which have a separate type system, Idris’s type system is deeply integrated, allowing for powerful compile-time guarantees and enhanced code reliability. This makes Idris particularly well-suited for projects requiring high levels of correctness, such as formal verification and compiler development. It also excels in areas where precise control over data structures and their invariants is critical.

Why learn Idris? #

Learning Idris offers several compelling advantages:

  • Enhanced Code Correctness: Dependent types allow you to specify and verify properties about your data and functions during compilation. This drastically reduces the likelihood of runtime errors.
  • Improved Code Readability and Maintainability: The expressiveness of the type system allows for more concise and self-documenting code. The compiler helps catch errors early, reducing debugging time.
  • Deep Understanding of Programming Fundamentals: Learning Idris necessitates a deeper understanding of functional programming principles and type theory, which benefits your programming skills in other languages.
  • Formal Methods Exploration: Idris provides a practical entry point to the field of formal methods and program verification.
  • Unique Problem Solving Abilities: Idris allows you to solve problems in ways impossible or impractical in other languages due to its expressive type system.

Setting up your Idris development environment #

The simplest way to get started with Idris is using the official installer for your operating system. You can find the latest installers and instructions on the official Idris website https://www.idris-lang.org/. The installation process usually involves downloading and running an installer specific to your operating system (Windows, macOS, or Linux).

Alternatively, you can use a package manager such as apt (Debian/Ubuntu), brew (macOS), or pacman (Arch Linux). Consult the Idris website for the most up-to-date package manager instructions.

Once Idris is installed, you’ll need a text editor or IDE. While a simple text editor will suffice for small programs, an IDE with Idris support offers significant benefits like syntax highlighting, code completion, and type checking. Popular choices include:

  • VS Code with the Idris plugin: This provides a lightweight but powerful development experience.
  • Emacs/Vim with appropriate plugins: These editors, known for their extensibility, offer excellent Idris support through community-maintained plugins.

After installation, verify your Idris installation by opening a terminal or command prompt and typing idris --version. This should display the version number of your Idris installation.

Your first Idris program #

Let’s write a simple “Hello, world!” program in Idris:

main : IO ()
main = putStrLn "Hello, world!"

Save this code as a file named hello.idr. Then, compile and run it from your terminal using:

idris hello.idr
./hello

This will compile your code and then execute the main function, printing “Hello, world!” to the console. The main function’s type signature IO () indicates that it performs input/output operations and returns no value (represented by ()). putStrLn is a function that prints a string to the console and adds a newline character. This simple example introduces basic Idris syntax and the compilation/execution process.

Idris Basics #

Types and Type Inference #

Idris is a statically-typed language, meaning that the type of every expression is known at compile time. Idris uses a powerful type system based on dependent types, but even without delving into the complexities of dependent types, understanding basic type declarations and inference is crucial.

Type annotations in Idris are usually optional. Idris’s type inference system is sophisticated enough to deduce the types of many expressions automatically. However, providing explicit type annotations improves code readability, aids in understanding complex code, and can help catch errors early.

For example:

x : Int
x = 5

y = 10  -- Idris infers y to be of type Int

add : Int -> Int -> Int
add x y = x + y

In this example, x is explicitly declared to be of type Int. y’s type is inferred as Int by Idris. The function add is explicitly given the type signature Int -> Int -> Int, indicating it takes two integers as input and returns an integer.

Basic Data Types (Integers, Booleans, Strings) #

Idris provides several built-in data types:

  • Integers (Int): Represent whole numbers. Idris supports various integer types with different precisions (e.g., Int8, Int16, Int32, Int64). If not specified, Int is usually a system-dependent integer size.

  • Booleans (Bool): Represent truth values, with the literals True and False.

  • Strings (String): Represent sequences of characters. String literals are enclosed in double quotes, e.g., "Hello, world!".

Example:

myInt : Int
myInt = 42

myBool : Bool
myBool = True

myString : String
myString = "Idris is awesome!"

Functions and Function Definitions #

Functions in Idris are defined using the = symbol. The type signature (the type of the function’s input and output) is optional, but recommended for clarity and to aid type inference.

Example:

addOne : Int -> Int
addOne x = x + 1

greet : String -> String
greet name = "Hello, " ++ name ++ "!"

The addOne function takes an integer x as input and returns x + 1. The greet function concatenates strings using the ++ operator.

Pattern Matching #

Pattern matching is a powerful feature in Idris that allows you to define functions that behave differently based on the structure of their input. It’s often used with algebraic data types (discussed later), but can also be used with simpler types like integers.

Example:

factorial : Nat -> Nat
factorial 0 = 1
factorial n = n * factorial (n - 1)

This defines the factorial function using pattern matching. If the input n is 0, it returns 1; otherwise, it recursively calls itself with n-1. Nat is a natural number type (non-negative integers).

Working with Lists #

Lists in Idris are represented using the List type constructor. A list of integers would be denoted as List Int. You can create lists using square brackets [] or by using the :: (cons) operator to add an element to the head of a list.

Example:

myList : List Int
myList = [1, 2, 3, 4, 5]

anotherList : List Int
anotherList = 1 :: 2 :: 3 :: []

sumList : List Int -> Int
sumList [] = 0
sumList (x :: xs) = x + sumList xs

myList shows a list literal. anotherList demonstrates using the :: operator to construct a list. sumList recursively calculates the sum of elements in a list using pattern matching. The empty list [] is handled as the base case.

Dependent Types #

Understanding Dependent Types #

Dependent types are types that depend on values. This is a powerful concept that allows you to express relationships between data and types within the type system itself. In contrast to ordinary types, where the type of an expression is independent of the values it manipulates, a dependent type’s definition involves values. This allows for stronger compile-time guarantees and more expressive type specifications. For example, a vector of a specific length can be represented with a type that depends on the length value. This prevents you from accidentally accessing elements beyond the vector’s bounds at compile time.

Vectors and Their Dependent Types #

A prime example of dependent types in Idris is the Vect type. Vect n a represents a vector of length n containing elements of type a. The length n is a value that affects the type. You can’t create a Vect 5 Int and then try to access its 6th element; the type system will prevent this at compile time.

myVector : Vect 3 Int
myVector = [1, 2, 3]

-- This will cause a type error:
-- invalidVector : Vect 3 Int
-- invalidVector = [1,2,3,4]

The compiler ensures that the length specified in the Vect type matches the actual length of the vector at compile time.

Type-Level Computation #

Dependent types enable type-level computation. This means you can perform calculations and logic within the type system itself, before runtime. This is often used to enforce constraints and perform sophisticated static analysis. For example, you can define a type that represents the result of a computation, and the type system will guarantee that the computation has been performed correctly at compile time.

Consider a function that calculates the factorial:

factorial : Nat -> Nat
factorial zero = 1
factorial (suc n) = suc n * factorial n

-- We could define a type representing the result of a factorial calculation:
data FactorialResult (n : Nat) : Type where
  FactorialResult : (result : Nat) -> FactorialResult n

While a full exploration of this example would be quite advanced, the key idea is that FactorialResult is a type that depends on the input n. It would require further work to properly connect it with a verified factorial function.

Using Dependent Types for Data Validation #

Dependent types are exceptionally useful for data validation. You can use them to ensure that data structures adhere to specific invariants at compile time. This eliminates the need for runtime checks, improving performance and reliability.

For example, you could define a type for a date that includes validation constraints (e.g., ensuring the month is between 1 and 12, and the day is valid for the given month and year). The type system would then prevent the creation of invalid dates. This proactive error prevention is one of the main strengths of dependent types. Note that building such a robust date type would involve more advanced Idris concepts like records, dependent pairs, and potentially even custom type classes.

Advanced Concepts #

Type Classes #

Type classes in Idris provide a way to define a set of operations that can be applied to different types. They are similar to interfaces or traits in other languages but are integrated more deeply into the type system. A type class defines a signature (a set of functions with specified types), and types can be declared as instances of a type class by providing implementations for those functions.

Example:

class Show a where
  show : a -> String

instance showInt : Show Int where
  show x = showIntDec x

instance showBool : Show Bool where
  show True  = "True"
  show False = "False"

main : IO ()
main = do
  putStrLn (show 5)       -- Output: 5
  putStrLn (show True)    -- Output: True

This defines a Show type class with a show function that converts a value to a string. We then define instances for Int and Bool, providing implementations of show for each type.

Data Types (Records, Variants) #

Idris supports several ways to define custom data types:

  • Records: Records group together named fields of potentially different types. They are useful for representing structured data.
data Person = Person { name : String, age : Int }

myPerson : Person
myPerson = Person { name = "Alice", age = 30 }
  • Variants (Algebraic Data Types): Variants represent values that can be one of several possible types. They are fundamental to expressing complex data structures.
data Shape = Circle Float | Rectangle Float Float

This defines a Shape type that can be either a Circle (with a radius) or a Rectangle (with width and height).

Modules and Namespaces #

Modules in Idris organize code into separate files, providing namespaces and preventing naming collisions. A module declaration starts with module. You can export specific items from a module using the export keyword.

Example (file: MyModule.idr):

module MyModule where

export
myFunction : Int -> Int
myFunction x = x * 2

To use myFunction in another file:

import MyModule

main : IO ()
main = putStrLn (show (MyModule.myFunction 5)) -- Output: 10

Error Handling with Exceptions #

Idris uses exceptions for error handling. The IO monad provides facilities for exception handling. The try and catch keywords are used to handle exceptions.

Example:

import System.IO

main : IO ()
main = do
  result <- try (unsafePerformIO (readFile "nonexistent_file.txt"))
  case result of
    Left e  => putStrLn ("Error: " ++ show e)
    Right s => putStrLn s

This attempts to read a file. If the file doesn’t exist, it catches the exception and prints an error message.

Writing Your Own Types #

Creating custom types is a core part of Idris programming. You’ve already seen examples with records and variants. However, the power of Idris truly shines when you combine these with dependent types to create types that enforce complex invariants. The design of custom types is driven by the specific problem domain and the invariants that need to be enforced. This often requires a solid understanding of type theory and functional programming paradigms.

Practical Examples #

Building a Simple Calculator #

Let’s build a simple calculator that can perform addition, subtraction, multiplication, and division. We’ll use pattern matching to handle different operations:

data Operation = Add | Subtract | Multiply | Divide

calculate : Operation -> Int -> Int -> Maybe Int
calculate Add x y = Just (x + y)
calculate Subtract x y = Just (x - y)
calculate Multiply x y = Just (x * y)
calculate Divide x y = if y == 0 then Nothing else Just (x / y)

main : IO ()
main = do
  putStrLn "Enter first number:"
  input1 <- readLn
  putStrLn "Enter operation (+, -, *, /):"
  opStr <- getLine
  putStrLn "Enter second number:"
  input2 <- readLn

  let op = case opStr of
              "+" -> Add
              "-" -> Subtract
              "*" -> Multiply
              "/" -> Divide
              _   -> error "Invalid operation"

  case calculate op input1 input2 of
    Just result -> putStrLn ("Result: " ++ show result)
    Nothing     -> putStrLn "Division by zero!"

This code defines an Operation data type, a calculate function using pattern matching, and a main function to handle user input and output. Error handling for division by zero is included using the Maybe type. Note that robust error handling and input validation would require more sophisticated techniques in a production-ready calculator.

Implementing a Small Game #

Let’s create a simple number guessing game:

import System.Random

main : IO ()
main = do
  secret <- uniform 1 100
  putStrLn "I've chosen a number between 1 and 100. Guess it!"
  guessingLoop secret

guessingLoop : Int -> IO ()
guessingLoop secret = do
  putStrLn "Enter your guess:"
  guess <- readLn
  if guess == secret then
    putStrLn "Congratulations! You guessed it!"
  else if guess < secret then
    putStrLn "Too low! Try again." >> guessingLoop secret
  else
    putStrLn "Too high! Try again." >> guessingLoop secret

This uses System.Random to generate a random number. The guessingLoop function recursively prompts the user for guesses until the correct number is entered.

Working with External Libraries #

Idris can interact with external libraries through the use of Foreign Function Interfaces (FFIs). The specifics depend on the library and its availability as an Idris binding. If a direct Idris binding isn’t available, you might need to create one, which can be a complex undertaking.

A simplified example (assuming a hypothetical library for image processing):

-- Assuming an Idris binding exists for the hypothetical image library
import ImageProcessing

main : IO ()
main = do
  -- Load an image
  image <- loadImage "my_image.png"

  -- Process the image (hypothetical function)
  processedImage <- applyFilter image blurFilter

  -- Save the processed image
  saveImage processedImage "blurred_image.png"

This example demonstrates the basic interaction with a hypothetical image processing library. The actual implementation of such a binding would involve a significant amount of work to handle data marshaling between Idris and the foreign library. You’d typically need to consult the specific library’s documentation and any available Idris bindings. The Idris community provides packages and tutorials for interfacing with various external libraries; check the official package repository for details.

Conclusion and Further Learning #

Where to Go From Here #

This Beginner’s Guide has provided a foundational understanding of Idris. To further your skills, consider focusing on these areas:

  • Advanced Type Theory: Deepen your understanding of dependent types, type classes, and more advanced type-level programming techniques. Explore concepts like type families and higher-kinded types.
  • Idris Libraries: Familiarize yourself with the available Idris libraries to expand your programming capabilities. Many libraries provide functions for common tasks, such as working with data structures, interacting with the operating system, and more.
  • Formal Verification: Learn how to use Idris to formally verify the correctness of programs. This is a powerful application of Idris’s type system and a key reason why many choose to learn the language.
  • Larger Projects: Undertake more substantial programming projects to consolidate your understanding and apply your knowledge in realistic scenarios. This could involve building a compiler, a formal verification tool, or any project that benefits from Idris’s strong type system.
  • Contributing to the Idris Community: Contribute to the Idris compiler, libraries, or documentation. This is a great way to improve your Idris skills and help the community grow.

Useful Resources and Documentation #

  • Official Idris Website: The official website (https://www.idris-lang.org/) provides comprehensive documentation, tutorials, and links to the community.
  • Idris Book: Explore the official Idris book (available online) for a more in-depth treatment of various aspects of the language.
  • Idris Package Repository: The Idris package repository (https://idris-lang.org/packages/) hosts numerous community-contributed libraries and tools.
  • Online Tutorials and Blog Posts: Search online for tutorials, blog posts, and articles on specific aspects of Idris. Many resources are available for different skill levels.

Idris Community and Support #

The Idris community is active and supportive. You can find help and interact with other Idris users through various channels:

  • Idris Discourse Forum: The official Idris discourse forum is a great place to ask questions, discuss topics, and share your knowledge.
  • Idris Mailing List: The Idris mailing list provides another avenue for communication and support.
  • GitHub Issues: Report bugs or feature requests on the official Idris GitHub repository.
  • Stack Overflow: While not exclusively dedicated to Idris, Stack Overflow often has helpful answers to Idris-related questions.

Don’t hesitate to reach out to the community for assistance. The Idris community is generally welcoming and eager to help newcomers learn and use the language effectively.

←
Beginner's Guide to Dylan
Beginner's Guide to XSLT
→
back to top