Lambda calculus

Programming language specification

Very high-level programming language

Language primitive

Inductive programming

Syntax

Biology

Unification

Functional logic programming

Programming domain

Artificial intelligence

High-level programming language

Ecology

Programming language

Dependent type

Type (biology)

Programming paradigm

Computer science

First-generation programming language

Type theory

Journal of Functional Programming

Many components of a dependently typed programming language are by now well understood, for example, the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high-level language is, however, folklore, discovered anew by successive language implementors. In this paper, I describe the implementation of Idris , a new dependently typed functional programming language. Idris is intended to be a general-purpose programming language and as such provides high-level concepts such as implicit syntax, type classes and do notation. I describe the high-level language and the underlying type theory, and present a tactic-based method for elaborating concrete high-level syntax with implicit arguments and type classes into a fully explicit type theory. Furthermore, I show how this method facilitates the implementation of new high-level language constructs.

Idris, a general-purpose dependently typed programming language: Design and implementation