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