Matus Tejiscak and I have produced a new draft paper titled Practical Erasure in Dependently Typed Languages, in which we explain how Idris erases computationally irrelevant parts of programs. The abstract is:
Full-spectrum dependently typed languages and tools, such as Idris and Agda, have recently been gaining interest due to the expressive power of their type systems, in particular their ability to describe precise properties of programs which can be verified by type checking.
With full-spectrum dependent types, we can treat types as first- class language constructs: types can be parameterised on values, and types can be computed like any other value. However, this power brings new challenges when compiling to executable code. Without special treatment, values which exist only for compile-time checking may leak into compiled code, even in relatively simple cases. Previous attempts to tackle the problem are unsatisfying in that they either fail to erase all irrelevant information, require user annotation or in some other way restrict the expressive power of the language.
In this paper, we present a new erasure mechanism based on whole-program analysis, currently implemented in the Idris programming language. We give some simple examples of dependently typed functional programs with compile-time guarantees of their properties, but for which existing erasure techniques fall short. We then describe our new analysis method and show that with it, erasure can lead to asymptotically faster code thanks to the ability to erase not only proofs but also indices.
Comments, feedback, questions, etc, all welcome!
A new draft paper, Resource-dependent Algebraic Effects, is available. Abstract:
There has been significant interest in recent months in finding new ways to implement composable and modular effectful programs using handlers of algebraic effects. In my own previous work, I have shown how an algebraic effect system (called “
effects“) can be embedded directly in a dependently typed host language. Using dependent types ought to allow precise reasoning about programs; however, the reasoning capabilities of
effects have been limited to simple state transitions which are known at compile-time. In this paper, I show how
effects can be extended to support reasoning in the presence of run-time state transitions, where the result may depend on run-time information about resource usage (e.g. whether opening a file succeeded). I show how this can be used to build expressive APIs, and to specify and verify the behaviour of interactive, stateful programs. I illustrate the technique using a file handling API, and an interactive game.
I’ve just submitted this, although constructive comments and suggestions are still of course very welcome!
To appear in the post-proceedings of IFL 2013, a paper by Simon Fowler and myself. Abstract:
Dependently-typed languages allow precise types to be used during development, facilitating reasoning about programs. However, stronger types bring a disadvantage that it becomes increasingly difficult to write programs that are accepted by a type checker and additional proofs may have to be specified by a programmer.
Embedded domain-specific languages (EDSLs) can help address this problem by introducing a layer of abstraction over more precise underlying types, allowing domain-specific code to be written in a high-level language which uses dependent types to enforce invariants without imposing additional proof obligations on an application programmer.
In this paper, we apply this technique to web programming. Using the dependently typed programming language Idris, we introduce an EDSL to facilitate the creation and handling of statically checked web forms, reducing the scope for programmer error and attacks such as SQL injection. We also show how to enforce resource usage protocols associated with common web operations such as CGI, database access and session handling.
You can find the accepted draft here. A revised version will appear later.
From Idris version 0.9.10 (and from now, if you’re tracking the git repository), the REPL provides various helpers for interactive editing. Agda users have known for a long time how useful this is, and I have become sufficiently jealous of it that I’ve decided it’s about time we had it too! I have implemented a short vim script to support interactive editing in vim, but since almost all of the work is done by the Idris REPL, it should be very easy to adapt to other editors. Here, I’ll briefly explain how to use it, then say a bit about how it works for anyone who might want to adapt it.
Read the rest of this entry »
We’ve just shipped the camera ready version of the following paper to PLMMS 2013:
Sequential decision problems, dependently typed solutions
Nicola Botta, Cezar Ionescu, Edwin Brady
We propose a dependently typed formalization for a simple class of sequential decision problems. For this class of problems, we implement a generic version of Bellman’s backwards induction algorithm and a machine checkable proof that the proposed implementation is correct. The formalization is generic. It is presented in Idris, but it can be easily translated to other dependently-typed programming languages. We conclude with an informal discussion of the problems we have faced in extending the formalization to generic monadic sequential decision problems.
You can find the full paper here.
I have just submitted a new paper to ICFP 2013:
Programming and Reasoning with Algebraic Effects and Dependent Types,
One often cited benefit of pure functional programming is that pure code is easier to test and reason about, both formally and informally. However, in order to be useful, programs must interact with the outside world. Haskell solves this problem using monads to capture details of possibly side effecting computations — it provides monads for capturing State, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects.
Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the Idris programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.
You can find the draft here. As usual, comments are very welcome.
This week I’ve been giving a course on Dependently Typed Functional Programming in Idris at IT University, Copenhagen. Various course materials are available:
- Lecture 1, Introduction, slides, video
- Lecture 2, Embedded DSLs, slides, video
- Lecture 3, Effect management, slides, video
- Lecture 4, Implementing Idris, slides, video
- Example code
- Idris web page