Implementing functional graph algorithms in a dependently typed language
Assigned to Pavel Karasik.
In functional languages, such as Haskell, we find existing libraries for working with graphs. These libraries contain the definitions of the necessary datatypes and the functions working on them. Examples of such libraries (in Haskell) are the FGL library by Martin Erwig and the Data.Graph module in the containers package.
In a dependently typed language we are able to express more expressive properties in the type signatures. The principal goal of this thesis is to develop a graph library in the dependently typed language Idris. This library should make use of dependent types in order to guarantee more invariants at compile time.
Functions which respect the invariants of the types require the construction of additional proof terms. A further goal of this thesis is to evaluate the mechanisms that Idris provides to erase these additional terms. The compiled functions should be no less efficient than an implementation which does not use dependent types.
Further Information
- Martin Erwig, Inductive Graphs and Functional Graph Algorithms.Link
- Andrey Mokhov, Algebraic Graphs with Class (Functional Pearl) Link
- Blogpost Link
- The Idris Programming Language Link