State, interaction and side-effecting programs in Idris
Description changed:
Idris (http://idris-lang.org) is a general-purpose purely functional
programming language with dependent types. In a talk at EdLambda last
year, I gave an introduction to the language showing how to implement
small functions, prove their correctness, and gave a larger example of
a well-typed interpreter for the lambda calculus.
In this talk, I will present some recent work on Idris which gives a
more practical example of these techniques. I will show how we can use
dependent types to implement and reason about side-effecting programs,
with a clear and usable API, illustrated using a "Space Invaders"
style game.
