Idris: A Functional Programming Language with Dependent Types

Programming Languages and Compiler Construction Department of Computer Science Christian-Albrechts-University of Kiel

Seminar Paper

Idris: A Functional Programming Language with Dependent Types

Author: B.Sc. Finn Teegen Date: 20th February 2015 Advised by: M.Sc. Sandra Dylus

Contents 1 Introduction 2 Fundamentals 2.1 Universes . . . . . . . . . . . . 2.2 Type Families . . . . . . . . . . 2.3 Dependent Types . . . . . . . . 2.4 Curry-Howard Correspondence

1 . . . .

3 Language Overview 3.1 Simple Types and Functions . . . 3.2 Dependent Types and Functions 3.3 Implicit Arguments . . . . . . . . 3.4 Views . . . . . . . . . . . . . . . 3.5 Lazy Evaluation . . . . . . . . . 3.6 Syntax Extensions . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . .

2 2 2 3 4

. . . . . .

5 5 6 7 8 8 9

4 Theorem Proving 10 4.1 Propositions as Types and Terms as Proofs . . . . . . . . . . . . . . . . . 10 4.2 Encoding Intuitionistic First-Order Logic . . . . . . . . . . . . . . . . . . . 12 4.3 Totality Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 5 Conclusion

15

ii

1 Introduction In conventional Hindley-Milner based programming languages, such as Haskell1 , there is typically a clear separation between values and types. In dependently typed languages, however, this distinction is less clear or rather non-existent. In fact, types can depend on arbitrary values. Thus, they become first-class citizens and are computable like any other value. With types being allowed to contain values, they gain the possibility to describe properties of their own elements. The standard example for dependent types is the type of lists of a given length - commonly referred to as vectors - where the length is part of the type itself. When starting to encode properties of values as types, the elements of such types can be seen as proofs that the stated property is true. This encoding allows the use of programming languages with dependent types as a logic. In order for this logic to be consistent, programs have to be required to be total, meaning that they are not allowed to crash or to be non-terminating. By using dependent types to encode not only properties of values but also properties of functions, we get the ability to make precise statements about the correctness of programs, giving us a higher reliability. This paper gives a brief introduction to Idris2 , a general-purpose functional programming language with dependent types. It is heavily influenced by Haskell and Agda3 and has support for tactic based theorem proving similar to Coq4 . Idris is mainly designed for verifiable systems programming and, to this end, it is a compiled language.[1, 4, 2] The further chapters are structured as follows. At first, some basic background knowledge is provided. This includes, inter alia, a formal definition of dependent types and a short introduction to the Curry-Howard correspondence that formulates the relationship between programs and proofs. In Chapter 3, we describe and exemplify the basic features of Idris as well as a few advanced ones. In addition, some programming techniques are demonstrated which are made available by those features. Afterwards, we demonstrate how Idris can be used for proving theorems in Chapter 4. We further show an encoding of intuitionistic first-order logic in Idris. At the very end, we discuss the pros and cons that may result from the use of Idris (and dependently typed languages in general) and relate Idris to other dependently typed languages.

http://www.haskell.org http://www.idris-lang.org/ 3 http://wiki.portal.chalmers.se/agda/pmwiki.php 4 https://coq.inria.fr/ 1 2

1

2 Fundamentals This chapter gives an introduction to the theoretical foundations of dependent types, which include universes and type families. Furthermore, the Curry-Howard correspondence is shortly explained.

2.1 Universes With types being first-class citizens, they necessarily have types themselves. One could naively wish for a type U that contains all types (including itself). Such types whose elements are types are called universes. By definition the universe U itself then would also have the type U for which we write U : U. However, U : U leads to a paradox, known as Russell’s paradox.[8] Let R be the set of all sets which are not members of themselves, so R = {x | x ∈ / x}. If R contains itself, then it contradicts its own definition as the set of all sets that are not members of themselves. On the other hand, if R is not a member of itself, then its definition dictates that it has to contain itself. Symbolically: R∈R⇔R∈ /R An elegant solution to Russell’s paradox is the introduction of hierarchical universes. In this hierarchy every universe Ui is a member of the next universe Ui+1 . Moreover, these universes are cumulative, i.e., if A : Ui then also A : Ui+1 : U0 : U1 : U 2 : . . . By saying that A has a type, we actually mean that A : Ui for some i. However, usually we just write A : U and omit the level i. This way, we even can write U : U which basically means Ui : Ui+1 for some i.

2.2 Type Families A collection of types B indexed by a given type A is called a family of types or indexed type family and is modeled by a function B : A → U whose codomain is a universe. Such collections are also denoted as dependent types.[8] An example of a family of types is the family VectR : N → U where VectR (n) is a real vector of length n. Parameterized data types are another example of indexed type families. For instance, List : U → U is the family of lists where List(A) is the type of lists that contains only elements of type A.

2

2 Fundamentals

2.3 Dependent Types Like in this paper, when speaking of dependent types, often an indexed type family is meant (see Section 2.2), although that term would also include the dependent product type and the dependent sum type.

Dependent Product Type The dependent product type - also called dependent function type or pi-type - is the type of functions that, given a type A : U in a universe of types U and a family of types B : A → U, assign to each element x : A an element of the type B(x) : U. In other words, the inhabitants of a dependent product type are functions whose codomain type may vary depending on their argument. The type of such dependent functions would be noted as follows: Π(x:A) B(x) For example, let VectR (n) again be the type of real vectors of length n. Π(n:N) VectR (n) would then be the type of functions that return a real vector of length n for a given natural number n. Note, the type of polymorphic functions is a dependent function type, too. The type of a polymorphic function returning elements of type C would be Π(A:U ) A → C. If B is a constant, the dependent product type simply becomes the ordinary function type A → B.

Dependent Sum Type Given again a type A : U and a family of types B : A → U, the dependent sum type, dependent pair type or sigma-type is the type of pairs that, having an element x : A as its first component, have an element of the type B(x) : U as its second component. Thus, the type of a pair’s second value may depend on its first value. The depending sum type is notationally written in the following way: Σ(x:A) B(x) Once more, we use real vectors as example. If (l, v) is a dependent pair of type Σ(n:N) VectR (n), then l has the type N and v has the type VectR (l). If B is a constant, then the dependent pair type is judgmentally equal to the Cartesian product type A × B.

3

2 Fundamentals

2.4 Curry-Howard Correspondence The Curry-Howard correspondence is the observation that there is an isomorphism between computational calculi as found in type theory and systems of formal logic as encountered in proof theory.[8, 7] The dependent type theory, for instance, corresponds to intuitionistic first-order logic. In general, the correspondence says that types correlate with propositions, terms with proofs and type inhabitation with provability. In particular, the unit type behaves the same as the true proposition, the empty type as the false proposition, a function type as implication, a product type as conjunction, and a sum type as disjunction. The dependent product type and dependent sum type are isomorphic to universal quantification and existential quantification, respectively.[8] Table 2.1 summarizes the correspondence between types and propositions: Type theory 1 0 P →Q P ×Q P +Q Π(x:X) P(x) Σ(x:X) P(x)

Logic True False P ⇒Q P ∧Q P ∨Q ∀x ∈ X : P(x) ∃x ∈ X : P(x)

Table 2.1: Analogy between type theory and logic

4

3 Language Overview This chapter covers Idris in its role as a general-purpose language. In this and the following chapters, it is assumed that the reader is familiar with Haskell. Therefore, we focus in this chapter mainly on the differences between Idris and Haskell and on the introduction of features that are specific to Idris.

3.1 Simple Types and Functions In this section, we describe how simple data types and function are defined and used in Idris.

Primitive Types Just like Haskell, Idris has built-in a number of primitive types: Int for integers, Float for floating point numbers, Char for characters and String for character sequences. A noticeable difference to Haskell is that String in Idris is not a list of Char, but a primitive data type.

Data Types Data types are declared in a similar way to Haskell data types, with a similar syntax. Natural numbers and lists, for example, can be declared as follows: data Bool = True | False data Nat = Z | S Nat data List a = Nil | (::) a ( List a )

Note that Idris automatically desugars the Peano representation of Nat into a more human readable format. The other way around, Idris allows us to write numerics for natural numbers, where it is clear that the number has the type Nat.

Functions Functions are implemented by pattern matching. Again, the syntax is similar to Haskell. The main difference is that Idris requires a type declaration for every function with one or more arguments using a single colon (instead of Haskell’s double colon). For example, the unary addition on natural numbers can be defined as follows:

5

3 Language Overview (+) : Nat -> Nat -> Nat (+) Z m = m (+) ( S n ) m = S ( n + m )

The notation \x => val constructs an anonymous function. Here, the only difference to Haskell is that we write => instead of ->.

3.2 Dependent Types and Functions As already mentioned, dependent types allow types to be predicated on values. Idris uses full-spectrum dependent types, meaning that there is no restriction on which values may appear in types.[2]

Type Families Dependent types are declared as a family of types using a syntax similar to that for Generalized Algebraic Data Types in Haskell.For example, vectors, i.e., lists which carry their size in the type, can be defined as follows: data Vect : Nat -> Type -> Type where Nil : Vect Z a (::) : a -> Vect n a -> Vect ( S n ) a

Here, we explicitly state the type of the type constructor Vect. It takes a natural number and a type as arguments and returns a new type. We say that Vect is parameterized by a type and indexed over natural numbers. The constructor Nil can only be used to construct vectors with zero length. In contrast, the constructor (::) can only create vectors with non-zero length.

Dependent Functions The dependent function type Π(x:X) P(x) would be written as (x : X) -> P in Idris, where the name x can occur inside of P. We can define such functions in the same way as on simple types such as List and Nat: by pattern matching. For example, the following function (++) appends two vectors and returns a vector which is the sum of the lengths of the input vectors: (++) : Vect n a -> Vect m a -> Vect ( n + m ) a (++) [] ys = ys (++) ( x :: xs ) ys = x :: xs ++ ys

Type-checking the code automatically establishes its correctness against the specifications encoded in the function type.

6

3 Language Overview

Dependent Pairs Dependent pairs allow the type of the second element of a pair to depend on the value of the first element. In Idris, (x : X ** P) is the notation for Σ(x:X) P(x). Again, the name x can occur inside of P. A value of this type is constructed using almost the same notation (x ** p), where x is a value of type X and p a value of type P. For example, we can construct a dependent pair out of a natural number and a vector of a particular length: vec : ( n : Nat ** Vect n Int ) vec = (2 ** [0 , 1])

Here, the type checker is able to infer the value of the first element from the length of the given vector. In place of values which we expect the type checker to fill in, we can write an underscore. Hence, we can write the above definition as: vec : ( n : Nat ** Vect n Int ) vec = ( _ ** [0 , 1])

It is also possible to omit the type of the first element of the pair, since it can be inferred as well: vec : ( n ** Vect n Int ) vec = ( _ ** [0 , 1])

Dependent pairs can be used to return values of dependent types where the index is not known in advance. For example, if we want to filter elements out of a vector according to some predicate, we will not know in advance what the length of the resulting vector will be. Thus, we have to use a dependent pair for the result: filter : ( a -> Bool ) -> Vect n a -> ( l ** Vect l a )

If the given vector is empty, the result is simply the following dependent pair: filter p Nil = ( _ ** [])

In the case that the given vector is not empty, the result depends on the result of a recursive call to filter. In order to obtain and use the result of that call, we use the with notation (see Section 3.4): filter p ( x :: xs ) with ( filter p xs ) | ( _ ** xs ') = if ( p x ) then ( _ ** x :: xs ') else ( _ ** xs ')

3.3 Implicit Arguments In the definition of (++) in Section 3.2, we have used undeclared names in the type, for example, n in Vect n a. In general, the type checker tries to infer the types for these

7

3 Language Overview names and will add them as implicit arguments. Alternatively, the type of (++) could be written as follows: (++) : { a : Type } -> { n : Nat } -> { m : Nat } -> Vect n a -> Vect m a -> Vect ( n + m ) a

The braces {} indicate that the arguments a, n and m are implicit. They can be omitted when applying the function (++).

3.4 Views Since types can depend on values, it is possible to determine the form of an argument by another one. This programming technique is called views.

Dependent Pattern Matching We have already seen how to implement a function that appends two vectors by using pattern matching on the first argument. As an alternative, we can distinguish the cases for the length that is encoded in the type Vect n a. By pattern matching on the implicit argument n, we can determine whether the given vector is empty or not: (++) : Vect n a -> Vect m a -> Vect ( n + m ) a (++) { n = Z } xs ys = ys (++) { n = S _ } xs ys = ( head xs ) :: ( tail xs ) ++ ys

Intermediate Value Matching Often, it can be very useful to match on the result of an intermediate computation. For this purpose, Idris provides a construct, namely the with rule. Effectively, the with rule adds another argument to the function being defined. In Section 3.2 we have already defined a vector filter function as follows: filter filter filter | (_

: ( a -> Bool ) -> Vect n a -> ( l ** Vect l a ) p [] = ( _ ** []) p ( x :: xs ) with ( filter p xs ) ** xs ') = if ( p x ) then ( _ ** x :: xs ') else ( _ ** xs ')

Here, the with clause allows us to deconstruct the result of filter p xs. This result is added as an extra argument which we place after the vertical bar.

3.5 Lazy Evaluation Although Idris uses eager evaluation (for more predictable performance), sometimes lazy evaluation may be useful or even necessary. Consider the following function:

8

3 Language Overview ifThenElse : Bool -> a -> a -> a ifThenElse True e1 e2 = e1 ifThenElse False e1 e2 = e2

This function uses only one of the two arguments e1 and e2, but not both. In order to evaluate only the argument which was used, Idris provides a special data type Lazy: data Lazy : Type -> Type where Delay : a -> Lazy a Force : Lazy a -> a

A value of the type Lazy a is unevaluated until it is forced by Force. The type checker of Idris automatically inserts conversions between the types Lazy a and a, and vice versa. Therefore, we can rewrite ifThenElse as follows, without using Force or Delay explicitly: ifThenElse : Bool -> Lazy a -> Lazy a -> a ifThenElse True e1 e2 = e1 ifThenElse False e1 e2 = e2

3.6 Syntax Extensions Idris allows the extension of its own syntax by using so-called syntax extensions. For example, the conditional if...then...else is not built-in in Idris, but predefined as a syntax extension based on the function ifThenElse from Section 3.5 as follows: syntax if [ b ] then [ e1 ] else [ e2 ] = ifThenElse b e1 e2

The left hand side of a syntax declaration describes the syntax rule, the right hand side its expansion. In general, a syntax rule consists of: • Keywords • Non-terminals • Names • Symbols Keywords have to be valid identifiers. In the given example, if, then and else are keywords. Non-terminals have to be included in square brackets and stand for arbitrary expressions. In order to avoid parsing ambiguities, these expressions cannot use syntax extensions at the top level (though they can be used in parentheses). In the example above, [b], [e1] and [e2] are non-terminals. Names are included in braces. They stand for names which may be bound on the right hand side of a syntax rule. Last, symbols have to be included in quotations marks. They can also be used to include reserved words in syntax rules, such as let or in.

9

4 Theorem Proving In this chapter, we go into detail on the Curry-Howard correspondence and explore the use of Idris for theorem proving.

4.1 Propositions as Types and Terms as Proofs According to the Curry-Howard correspondence, propositions and proofs are isomorphic to types and terms. In Idris, this means that by constructing a value of a certain type, we have simultaneously constructed a proof that the proposition encoded by that type holds. In order to illustrate this relationship, we will establish a simple logic based on the Peano representation of natural numbers we introduced earlier in Section 3.1.[6] We are going to define two predicates named Even and Odd which should state that a given natural number is even and odd, respectively. Before we start to encode this logic in Idris, we will specify its axioms and rules by writing them in the form of inference rules. For our purposes, we need two axioms. One axiom presumes that zero is even and the other one presumes that one is odd: (evenZero)

Even(0)

(oddOne)

Odd(1)

Based on inductive reasoning, we can define the following two rules that express that if some number n is even, n + 2 is also even, and if some number n is odd, n + 2 is odd as well: Even(n) Even(n + 2)

(evenSuc)

Odd(n) Odd(n + 2)

(oddSuc)

Having these rules and axioms, we are able to construct a proof for any natural number that it is even or odd. For example, we can prove that four is even by applying the rule evenSuc twice, leaving the obligation Even(0) which is shown by the axiom evenZero. Using the rule oddSuc and the axiom oddOne, it can be proven analogously that five is an odd number: (evenZero)

Even(0) Even(2) Even(4)

(oddOne)

Odd(1) Oddd(3) Odd(5)

(evenSuc) (evenSuc)

10

(oddSuc) (oddSuc)

4 Theorem Proving We now want to implement this logic in Idris. Since propositions correlate with types, our first step is to define the two type families Even and Odd. Because our logic is defined over the language of natural numbers, we index the type constructors for our propositions by the type Nat. As constructors for values of these types, we simply use the rules and axioms: data Even : Nat -> Type where evenZero : Even Z evenSuc : Even n -> Even ( S ( S n )) data Odd : Nat -> Type where oddOne : Odd ( S Z ) oddSuc : Odd n -> Odd ( S ( S n ))

In a similar manner as before, we are again able to prove that four is even and five is odd by constructing values for the types Even 4 and Odd 5: fourIsEven : Even 4 fourIsEven = evenSuc ( evenSuc evenZero ) fiveIsOdd : Odd 5 fiveIsOdd = oddSuc ( oddSuc oddOne )

By having Idris type-checked our program, our proofs are verified. Note that it is impossible to find a value of the type Odd 4, which means that it is unprovable, i.e., false, that four is odd. Having the predicates Even and Odd, we can further define a rule which states that the sum of two odd natural numbers is even: Odd(n) Odd(m) Even(n + m)

(oddOddEven)

In Idris, this implication can be expressed as a function type according to Section 2.4. The premises become the parameter types and the conclusion becomes the result type. When we implement this function, we define how a new proof can be obtained from the proofs passed as arguments: oddOddEven oddOddEven oddOddEven oddOddEven

: Odd n -> Odd m -> Even ( n + m ) oddOne oddOne = evenSuc evenZero oddOne ( oddSuc y ) = evenSuc $ oddOddEven oddOne y ( oddSuc x ) y = evenSuc $ oddOddEven x y

As an example, the proposition that ten is even can now be proven in Idris using the function oddOddEven and our previously defined proof fiveIsOdd: tenIsEven : Even 10 tenIsEven = oddOddEven fiveIsEven fiveIsEven

11

4 Theorem Proving

4.2 Encoding Intuitionistic First-Order Logic After we have seen how to implement a simple logic in Idris, we want to generalize this approach by encoding the intuitionistic first-order logic in Idris at type level. In order to illustrate the analogies stated by the Curry-Howard correspondence, we simply use syntax extensions as introduced in Section 3.6. This way, we will be able to write logic formulas without manually translating them into their type representation in Idris.

True and False Proposition According to the Curry-Howard correspondence, the true position correlates with the unit type, i.e., the type that allows only one value, whereas the false proposition correlates with the empty type: syntax ">" = () syntax "⊥" = Void

Since the empty type has no constructor and therefore has no values at all, it is impossible to prove that the false proposition is true.

Implication We already know, that an implication corresponds to an ordinary function type. Thus, we can define the following syntax extension: syntax [ P ] "⇒" [ Q ] = P -> Q

The proposition P ⇒ Q is considered true if there is an actual function that transforms any proof of P into a proof of Q.

Conjunction A conjunction corresponds to a pair type: syntax [ P ] "∧" [ Q ] = (P , Q )

A proof of the conjunction P ∧ Q can only be constructed if both a proof of P and a proof of Q is given.

Bijection The logical equivalence of two propositions can be expressed as a conjunction of two implications: syntax [ P ] "⇔" [ Q ] = ( P ⇒ Q ) ∧ ( Q ⇒ P )

12

4 Theorem Proving

Disjunction A disjunction is a sum type, also known as an Either type: syntax [ P ] "∨" [ Q ] = Either P Q

A proof of a disjunction P ∨ Q only requires a proof of P or a proof of Q in order to hold. It can be constructed with Left or Right, respectively.

Negation The logical negation of some proposition P is usually defined as an abbreviation for the implication P ⇒ ⊥: syntax "¬" [ P ] = P ⇒ ⊥

In other words, ¬P is true if we can map every proof of P to a proof of ⊥. But we can only do so if P has no proofs, because ⊥ has no proofs neither. In contrast, ¬P is false if there is no map from a proof of P to a proof of ⊥. This happens as soon as P has a proof.

Universal Quantification Universal quantification is represented as a dependent function type: syntax "∀" { x } "∈" [ X ] ":" [ P ] = ( x : X ) -> P

In order to prove the proposition ∀x ∈ X : P(x), we would define a function that constructs a proof of P(x) for any given x of the type X.

Existential Quantification An existential quantification can be written as a dependent pair type: syntax "∃" { x } "∈" [ X ] ":" [ P ] = ( x : X ** P )

A proof for the proposition ∃x ∈ X : P(x) has to provide both an element x of the type X and a proof for the proposition P (x).

13

4 Theorem Proving

4.3 Totality Checking In order to be verifiably, proofs need to be defined by total functions. A function is total if it is defined for all possible inputs (that is, partial functions are always not total) and is guaranteed to terminate. Unfortunately, the termination of a function is undecidable due to the halting problem. We can work around this problem by only permitting functions with primitive recursion, structural recursion or no recursion at all. However, by restricting the space of allowed functions to such ones we may reject some total functions as being not total.[3] For example, the following implementation of the quicksort algorithm cannot be verified to be total because the totality checker cannot decide that the results of filter (< x) xs and filter (>= xs) xs will always be smaller than (x :: xs): quicksort : Ord a = > List a -> List a quicksort [] = [] quicksort ( x :: xs ) = quicksort ( filter ( < x ) xs ) ++ ( x :: quicksort ( filter ( >= x ) xs ))

In such cases, it is possible to give hints for the totality of a function. The predefined function assert_smaller addresses this problem: assert_smaller : a -> a -> a assert_smaller x y = y

This function evaluates to its second arguments while also asserting to the totality checker that y is structurally smaller than x. Using assert_smaller we can change the definition of quicksort as follows to obtain a function which is verifiably total - indicated also by the optional keyword total: total quicksort : Ord a = > List a -> List a quicksort [] = [] quicksort ( x :: xs ) = quicksort ( assert_smaller ( x :: xs ) ( filter ( < x ) xs )) ++ ( x :: quicksort ( assert_smaller ( x :: xs ) ( filter ( >= x ) xs ))

In extreme cases, one could use the predefined function assume_total which marks an expression as always being total: assert_total : a -> a assert_total x = x

Nevertheless, the use of assume_total should be avoided.

14

5 Conclusion As we have seen, Idris - as a dependently typed programming language - makes some interesting new programming techniques available, such as views for pattern matching on implicit arguments and intermediate value matching. These techniques help us to greatly improve the structure and expressiveness of our source code. In addition, the possibility to refine type signatures using dependent types is a major advantage of Idris over conventional programming languages and can increase the robustness of programs. Type checking is equivalent to the verification of the properties encoded in a certain type. Thus, we obtain more reliable results by getting our programs type-checked than we would get from traditional testing. On the other hand, programming with dependent types can sometimes make things more difficult as we have seen in Section 3.2 or Section 4.3. Furthermore, totality checking is (necessarily) very conservative and programs or functions may require some extra effort in order to become verifiably total. In comparison to other dependently typed languages, for instance, Agda, Idris emphasises general-purpose programming, rather than theorem proving.[5] As a result, Idris supports high-level programming constructs, such as type classes and do notation which make programming in Idris very comfortable. Although not covered in this paper, it has moreover a foreign function interface for easy interoperability with external C libraries.[1] All in all, Idris definitely meets its design goal to be a programming language suitable for verifiable systems programming.

15

References [1]

Edwin Brady. Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation. Sept. 15, 2013. url: http://eb.host.cs.st-andrews. ac.uk/drafts/impldtp.pdf (visited on 01/30/2015).

[2]

Edwin Brady. “Idris – Systems Programming Meets Full Dependent Types”. In: Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification. PLPV ’11. Austin, Texas, USA: ACM, 2011, pp. 43–54.

[3]

Edwin Brady. On Partial Functions in Idris. url: https://edwinb.wordpress.com/ 2013/02/19/on-partial-functions-in-idris/ (visited on 01/30/2015).

[4]

The Idris Community. Programming in Idris: A Tutorial. Oct. 26, 2014. url: http: / / eb . host . cs . st - andrews . ac . uk / writings / idris - tutorial . pdf (visited on 01/30/2015).

[5] Idris Language FAQ. url: http://www.idris-lang.org/documentation/faq/ (visited on 02/06/2015). [6]

Liam O’Connor-Davis. Learn You an Agda. url: http://williamdemeo.github.io/ 2014/02/27/learn-you-an-agda/ (visited on 02/03/2015).

[7]

Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., 2006.

[8]

The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory. org/book, 2013.

16