Idris is a functional programming language developed at the University of St Andrews (and elsewhere). It has similarities with Haskell (taught as part of CS2006) but additionally has a more expressive type system which allows programmers to state properties of programs which are checkable at compile time, such as assumptions about sizes of data structures, or checking that a resource or communication protocol is followed correctly.
As a new language, there is still limited library support, and plenty of scope for experimenting with ways to use the type system to build safer software. This project is to provide library support for one of the following, and investigate how the type system can be used to our advantage:
- Graphical or textual user interfaces
- Parsing common document formats, e.g. XML, JSON
- Graphics via SDL/OpenGL
- Concurrent and Parallel programming
In most cases, this will involve finding the relevant C libraries, creating bindings, then building expressively typed Idris bindings on top.
- Low level bindings to the relevant C library
- A high level type safe interface to the library
- A suite of demonstration programs