Lightning Intro to Functional Programming and Dependent Types with Idris

Contents

• Getting Started
  • First Commands
• Constants
• Functions I
• Basic Data Declarations
• Functions II: the finer points of recursion
• First IO
• Polymorphic Data Types
  • Lists
• Generalized Algebraic Data Types
  • Vectors
  • Propositions

The purpose of this tutorial is to introduce the key concepts of functional programming and dependent type theory, convince you that these ideas can be powerful tools both for writing useful software and obtaining strong guarantees of its correctness, and to specifically demonstrate how to utilize these ideas with the Idris programming language.

While Idris has solid and ever-improving official documentation, it does not focus on teaching fundamental concepts, leaving a significant pedagogical gap for someone without previous experience in functional programming. This work-in-progress tutorial is an attempt to bridge that gap.

Let’s first introduce, in broad strokes, the meaning of these two main ideas we refer to in this title.

Functional Programming

Two different properties can be said to define a functional programming language, both of which apply to Idris. The more modest sense of the term is that functions are “first-class citizens” of the language. They’re one of the basic kinds of values that the language deals with, so there’s no absolute distinction between functions and other forms of data. A stronger sense of the term requires that the functions in our language are really bona-fide mathematical functions. In other words, the output of a function depends only on the inputs. This means that functions can neither refer to nor alter any external state. In contrast, many programming languages refer to as “functions” things which do not satisfy this definition, and could more correctly be called subroutines.

The motivation for this distinction is a familiar one in computing: Separation of concerns. There are really two very different kinds of operations a computer program might need to do, and it can benefit us to treat them differently: Operations that interact with the world in some way, like reading data or writing a file, and pure functions that do the main work of transforming our data. Enormous classes of errors can be avoided simply by not conflating these two kinds of operations.

In a pure functional language like Idris, any function that interacts with the outside world must be clearly identified in its type: it will have a result type of IO a where a is whatever type is to be returned by the operation. Conversely, any function that does not have such a type is guaranteed to be free of any side effects. The only thing such a function can do is produce its output type.

Dependent Types

Dependent types simply means that types can depend upon values. This rather innocuous looking statement leads to some profound consequences.

Type systems as traditionally used in programming languages are a limited form of formal verification. They can preventing us from mistaking one sort of data from another.

Dependent types dramatically expand the range of what kinds of properties can be enforced during type checking. Rather than being limited only to the general kinds of data that can be expressed in the language, dependent types can descriminate the actual values of the data in question. To take a very simple/contrived example, a dependently typed programming language could demand something not just of type Bool, but a Bool with the value True. We will soon see in detail how something like this works.

The most dramatic possibility afforded to us by working with dependent types is that we can express propositions as ordinary data types. Indeed, it has proven a powerful approach to logic to consider propositions as dependently-typed data types whose inhabitants are their proofs.

Getting Started

We’re going to assume you’ve already installed Idris. Start it up by entering idris at your command line and you should be greeted by the following banner:

     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.18
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

The idris REPL provides a number of facilities that will prove incredibly helpful while we develop, but first let’s cover the basics. The most common REPL commands we’ll be using are :l, which loads and type-checks the idris source file of the supplied name (this is equivalent to starting idris with idris file.idr or simply idris file), and :r which reloads the file.

First Commands

Of course the main function of a REPL is to evaluate the expressions we enter. Let’s try some basic values.

You can see that in each case the compiler is reporting the type along with the entered value, and the symbol : can be read to mean “has the type”. In Idris every value occupies a type.

One of the most jarring differences in syntax compared to more traditional languages is that function application is denoted simply by space. No parentheses or commas are required.

While most functions are defined with alphanumeric character names, there are also functions identified by one or more operator characters, which go between their arguments.

As we noted in the introduction, the fact that functions are themselves first-class values, which in particular can be passed as arguments just like anything else, will play key role in almost everything we do. Just to whet your appetite for what’s to come, here’s one simple example where this property is clearly visible.

Here we have a function, map which takes 2 arguments. The first argument (2*) is itself a function, and the second is a data structure, here a List Integer, which the function is “mapped over”. If you want to impress your friends, a function that depends on another function is called a functional.

One important rule that I’ve steered clear of addressing so far is that every term must have an unambiguous type. You might have run into this if you attempted to define a list of integers in the most apparently straightforward way:

The familiar list syntax [x,y,..] is syntactic sugar for a constructor ::, which takes an element and a list and returns the list with the element appended to the beginning, along with an empty list constructor Nil. But all identifier names in Idris are bound to a namespace, and thus can be overloaded. This error is informing us that 3 different namespaces have versions of these constructors in scope, all of which consequently share the list syntax.

One easy way we can specify the type at the REPL is with the well-named function the.

This is a function that takes a type, and a term of that type, and then simply returns the term argument unchanged. So this is an elegant way to specify a type without using any special syntax, but instead this trivial function, whose behavior happens to be entirely specified by its type.

Another idea that will be explored in detail later, but which we only hint at for now, is the idea of types representing propositions. In particular Idris has a data type representing equality.

There are a number of useful REPL commands allow us to retrieve information from the compiler. For example :doc followed by a name prints out any documentation information associated with that value/function, data type, or type class. Similarly :t followed by any expression tells us the type of that expression. The :apropos command is useful when you want to find something but don’t know exactly what it’s called; it returns information on anything that contains the word you provide anywhere in it’s definition, including in its docstrings. Finally, the :search command allows you to search by type! I strongly encourage utilizing these capabilities while following this tutorial. To see the complete list of commands type :?.

Finally I note in passing that, though we won’t explicitly cover it in this tutorial, much of this functionality is also available from within text editors, especially via the idris modes for emacs and vim.

Modules

For now, we’ll only attempt to cover the minimal essentials necessary to get you up and running. Every Idris module begins with a module declaration, followed by optional import statements, like this:

module LearnIdris

import MyOtherModule

below which the contents of the module is defined. In general all Idris code may only depend on what has been defined above it in the module, or in the imported modules. The only exception to this is for mutually-defined data and functions which we’ll see later.

All identifiers, including module names, are allowed to start with either capital or lowercase letters.

Modules introduce a namespace for all identifiers defined within. This means that you’re free to reuse any names from the standard libraries, however if you do you’ll often then have to give the namespace explicitly when using them. So for example, if we are to redefine Bool in a module called Tutorial, we’d then have to write Tutorial.Bool prevent ambiguities while using it. In some cases this may not be neccessary when its sufficiently clear from the context which verion is being invoked.

Constants

In definitions for constants and functions, we begin by declaring the type using :, and then we assign the value with =. Here are some simple examples.

mybool : Bool
mybool = True

mylist : List Integer
mylist = [1,0,0,1]

mystring : String
mystring = "green curry"

mytype : Type
mytype = String

Note that Idris enforces no capitalization requirements on any identifiers, but we usually follow the convention that names of data types and data constructors are capitalized while names of functions and constants start with a lowercase.

Functions I

Function definitions will follow the same basic format that we used above. One major difference is that we’ll in general use more than one = to describe the function. Consider the following simple example.

-- boolean NOT, a single-argument function
not : Bool -> Bool
not True  = False
not False = True

First, notice that we’ve used the -> symbol to express the fact that the not function takes a Bool as input and produces a Bool as an output. This specification of the function’s input and output types is called the function’s type signature. In the body, we used the most straightforward way to define a function, which is to write an equation for all possible input values. While this is the most conceptually straightforward way, it will become prohibitively tedious for most input types.

A more powerful approach is to abstract over the possible input values by binding them to variables on the right-hand side. Check out this implementation of exclusive-or:

-- boolean XOR, a 2-argument function
xor : Bool -> Bool -> Bool
xor False x = x
xor True  x = not x

Binding one of our inputs to the variable x allowed us to express in 2 equations what otherwise would have taken 4 if we explicitly wrote out all the possible input values.

This process of writing functions in terms of partly-explicit and partly-abstract data is called pattern matching. While it tends to take some getting used to, when you do it’s an incredibly powerful and elegant way of describing functions.

One property of our last function that won’t always hold is that the patterns (of left-hand-side data) are mutually exclusive. When this isn’t the case, we’ll use the fact that Idris attempts to match the patterns in the order that we write them. One particular way we can do this is by using _ which matches anything.

isZero : Integer -> Bool
isZero 0 = True
isZero _ = False

If we wrote these two lines in the opposite order, the function would always return False because _ would “match” on any possible input and so the other pattern would never be tried.

Infix Operators

For another example, we could define two more standard boolean logical operators.

-- specify the order of precedence when defining operators:
infixl 4 &&, ||

-- boolean AND
(&&) : Bool -> Bool -> Bool
(&&) True True = True
(&&) _    _    = False

-- boolean OR
(||) : Bool -> Bool -> Bool
(||) False False = False
(||) _     _     = True

Note that the first non-comment line of this code snippet is what’s called a fixity declaration, which we supply whenever we name a function with these special operator characters. Such a function is called an infix operator because they’re invoked by inserting the operator between the two inputs, as for example when we add 5 + 3. The fixity declaration is needed because it clarifies which operators take precedence over which others; that’s what the ‘4’ in the above fixity declaration means. Operators with the highest precedence are evaluated first, from the maximum of 10 down to the minimum of 0. It also specifies whether evaluation proceeds from the right or the left, denoted by infixr and infixl respectively. This means, for example, that x && y && z evaluates the same way as (x && y) && z. In this particular case the distinction is irrelevant, but in general this is an ambiguity that needs to be fixed.

Whenever we have an infix operator, we can use it like a regular (‘postfix’) function by wrapping it in parentheses. (In particular we need to do this when writing their type declarations, as in the above code.) For example these two ways of multiplying are equivalent:

Incidentally can also use a regular function in the infix position by wrapping it in backticks.

By the way, you can always check the fixity declaration of any operator by looking it up at the REPL.

Here we see two features that will be discussed in more detail shortly. (+) doesn’t have a concrete type, the type is only specified in terms of a type variable a. The beginning of the signature, Num a => is a typeclass constraint. It says that the type variable a is restricted to be a member of the Num typeclass, because that’s the class for which (+) must be defined. If you want to see the rest of the information about Num, type in :doc Num.

Currying & Higher-order Functions

At this point it’s important to clarify a detail about function types that’s so far been glossed over. You might be wondering why we write the type signature of two-argument functions in the form a -> b -> c. On first glance this form almost doesn’t seem to distinguish between input and output types. It appears as though the type signature is defined in terms of just a binary type-level operator ->.

These observations are absolutely valid. Fundamentally, there are no multi-argument functions in Idris. When we write a type signature like a -> b -> c what it really means is a -> (b -> c). In other words, the function that takes one argument a and returns a function from b to c. In particular this means that such functions are really higher-order functions, i.e. functions that themselves either depend on or return other functions. This is one of the most important concepts to understand when learning to program in Idris and many similar languages. Note that it fundamentally relies on the idea that functions are first-class values of the language that can be computed and returned like anything else.

Representing multi-argument functions in this way is called currying, after Haskell Curry, and it has many virtues. One is conceptual simplicity: There is no need to have multi-argument functions as a primitive notion since we can easily represent them as higher-order, single-argument functions. A more practical benefit for the user is that any multi-argument functions we have automatically give us families of lower-order functions we can use by feeding it only some of the arguments it takes.

Lets consult the REPL to verify I’m telling the truth.

Idris> :t xor
xor : Bool -> Bool -> Bool
Idris> :t xor False
xor False : Bool -> Bool

Indeed, when we supply one value to the 2-argument function, we get back a single-argument function. This is called partial application. It’s one of many benefits we’ll reap from treating functions as first-class language values.

Currying also gives us added flexibility when defining functions. We can always use the standard approach of defining multi-argument functions directly by expressing their final output in terms of the input values. However we can also utilize the fact that multi-argument functions are curried to directly define them as higher-order functions. For example we could have alternatively defined our xor function as:

-- 2-argument function as a 1-argument higher-order function
xor' : Bool -> Bool -> Bool
xor' False = id
xor' True  = not

To emphasize the difference, in the first xor definition we introduced two arguments on the left-hand-side, so the expression on the right-hand-side needed to be a Bool. In this case we only introduce one value on the LHS, so in order to be consistent with the type signature, the expressions on the RHS need to be of type Bool -> Bool. Here id is of course the identity function, which is defined for all types, and we’ve already described not.

Overall, it’s much more common to define higher-order functions in the former way, but the possibility of this other approach can sometimes make things easier. More importantly for our purposes, it can be very helpful for understanding this critical concept to see at least see one example of this other approach.

Computing Types

Since types are just a kind of value, we can compute them like we could anything else. One place where this can be useful is for defining a shorthand for certain type structures we intend to use.

For a first example, take this type synonym function for lists of lists of a supplied type.

array : Type -> Type
array a = List (List a)

We can also write a type-function describing the dependency of an arbitrary return type on a particular number of copies of a given input type.

arity : Nat -> Type -> Type -> Type
arity Z     a b = b
arity (S n) a b = a -> (arity n a b)

Basic Data Declarations

Data types are the mechanism by which a user introduces new values and types into the system.

a critical concept to understand, being the single way a user can expand the range of possible types and values the language knows how to deal with. In this section we will introduce them at a level that is extremely simple and easy, but later on we will see some more sophisticated examples.

We can define our own basic data types with a data declaration like the following.

data Bool = True | False

We first give the name of our data type, then after the = sign we supply a list of data constructors separated by vertical bars. In this simple example the two data constructors, True and False, correspond directly to the two possible values of the data type.

A more general situation is to follow each data constructor by other types of values that must be supplied. For example, the following data declaration might be used to represent two different types of users of a service: Registered users have an ID number and a String for their name, while unregistered users have only an ID number.

data Visitor = Unregistered Int
             | Registered Int String

These kinds of data declarations define what are called Algebraic data types. The name refers to how, as we’ve seen, the data types can be combined in two different ways, roughly analgous in structure to addition and multiplication.

module Seminar

data Grade = A | B | C | F

data Year = Fresh
          | Soph
          | Junior
          | Senior

data Student = MkStudent String Year Grade

data Teacher = MkTeacher String

data Person = S Student
            | T Teacher

*Tutorial> MkStudent "Joe" Soph A
MkStudent "Joe" Soph A : Student

Functions II: the finer points of recursion

Natural Numbers

The natural numbers – integers starting from zero and counting up – are, as the name implies, an intuitively natural number system, and are a good place to begin examining how to describe numbers as data types. After all they’re the first form of numbers humans understood (sans zero), and they’re generally the first one we all learn about in school.

The key property of the natural numbers we’re going to exploit is the fact that all of them can be described by only two data constructors. Zero Z and the successor function S whose interpretation is to increase the number by 1. Thus naturals are described by this remarkably simple definition:

data Nat = Z | S Nat

{-  0  ~  Z
    1  ~  S Z
    2  ~  S (S Z)
    3  ~  S (S (S Z)) ...  -}

Here we’ve also introduced the syntax for multi-line comments to show what the first few Nats look like in terms of these constructors. Simple as it is, this way of representing the naturals will be unfamiliar to many, so it may help to see them written explicitly. This form for the naturals is often called the Peano axioms.

Many will justifiably wonder why we should bother with such a system, given that encoding integers in any of the standard ways are certainly more efficient and intuitive. The first reason is conceptual and pedagocial: Nats are first of all the simplest possible example of an inductive datatype. Many other data types that we’ll encounter will involve this same general property of being defined by repeated application of a data constructor acting on that same data type. More to the point, defining operations like addition and multiplication are almost inevitably structurally recursive functions. This means they are defined in a recursive way, in direct correspondence to the recursive structure of the data on they operate. It is this property that we focus on now.

Another reason, which we’ll take up further on, is this: Defining Nats in this recursive way makes them amenable to having the properties of the functions on them formally proven. This is where the dependent type system will really shine for us. Proofs are also first class data types in idris, and we’ll see this when we examine, for example, proofs of the commutative and associative properties of addition and multiplication.

For now though, lets turn to our first example of a structurally recursive function.

Addition and multiplication of natural numbers

plus : Nat -> Nat -> Nat
plus Z     m = m
plus (S n) m = S (plus n m)

Here we see prototypical example of a common format to be repeated in many different contexts. Our data type has a base case, Z, for which we can define the answer directly, and we also must describe the step case which defines the answer at level S n in terms of the same function one level lower, at level n. This suffices to define addition for all natural numbers.

Similarly, just as addition is defined as the repeated application of the successor function, we can define multiplication recursively as repeated application of addition.

mult : Nat -> Nat -> Nat
mult Z     m = Z
mult (S n) m = plus m (mult n m)

First IO

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

getName : IO String
getName = do x <- getLine
             return x

greet : IO ()
greet = do putStrLn "What's your name?"
           n <- getLine
           putStrLn $ "Hello, " ++ n ++ "!"

Polymorphic Data Types

Maybe

data Maybe a = Nothing | Just a

safeDiv : Float -> Float -> Maybe Float
safeDiv x y   = Just (x / y)
safeDiv _ 0.0 = Nothing

Either

data Either a b = Left a | Right b

Lists

Lists are, of course, one of the most basic and ubiquitous data structures around. We’ve already seen an example of a list invoked in the usual way by square braces [1,0,0,1], but as you may guess, this is only syntactic sugar. Lists are a proper idris data type so let’s see how they’re defined:

infixr 7 ::

data List a = Nil | (::) a (List a)

There are a couple important things to notice about this definition. For one thing, while we’ve already seen infix operators used as functions, here we see they can be used as a data constructor as well (which, anyway, is a special kind of function). Another important element is that the declaration refers to an abstract type a, because we want to define lists for all possible types simultaneously. Notice that the left-hand side of the equation doesn’t just say List, it says List a. This means that List by itself is not a type. To make a concrete type we must fill in the a, so for example List Int or List String are types, but List by itself is not, it is actually a function with signature Type -> Type.

As the declaration says, we can construct a list with either Nil which creates an empty list of any particular type, or with (::) which takes an element of type a on the left, and a list of a’s on the right, and returns back a new list with the first element appended to the front of the list.

So an example of a fully-explicit list definition is the following:

-- [0,1,2]
lst : List Integer
lst = 0 :: 1 :: 2 :: Nil

Generalized Algebraic Data Types

Vectors

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect n a -> Vect (S n) a

Propositions

Evenness

data Even : Nat -> Type where
  EvenZ : Even Z
  EvenS : Even n -> Even (S (S n))

Comparison

||| Proof that one number is less than or equal to another
data LTE : Nat -> Nat -> Type where
  LTEZero : LTE Z r
  LTESucc : LTE l r -> LTE (S l) (S r)

||| A correct-by-construction ordered list of Nats
data OrdList : List Nat -> Type where
  Nil  : OrdList []
  (::) : LTE x y -> OrdList (y :: l) -> OrdList $ x :: (y :: l)

To be continued…