Abstract data types are an essential tool in a programmer's toolkit, but finding a data structure to fit them can be challenging. This is especially so for graphs, which can have complex constraints that are difficult to encode using conventional data structures. Join me in the search for a functional, typesafe graph. We will explore different graph representations, and discover how types can help us encode constraints. Using dependent types, we will construct a graph that we can prove satisfies its abstract data type.
THIS TALK IN THREE WORDS
ADTs
Graphs
Dependent types
OBJECTIVES
By the end of this talk, the audience should:
- Understand the concept of an abstract data type vs a specific data structure
- Appreciate that there can be many different ways of modelling an abstract data type
- Understand that types can be used to constrain the structure of data
- Be inspired to experiment with Idris and dependent types
TARGET AUDIENCE
This talk would be best directed at people who use typed functional languages, but may not yet appreciate that type systems can be used to enforce constraints. They should be familiar with basic functional data structures, such as linked lists, but not need to know anything about graph encodings.
