Inductive Graph Representations in Idris by Michael R. Bernstein.
An early exploration on Inductive Graphs and Functional Graph Algorithms by Martin Erwig.
Abstract (of Erwig’s paper):
We propose a new style of writing graph algorithms in functional languages which is based on an alternative view of graphs as inductively defined data types. We show how this graph model can be implemented efficiently and then we demonstrate how graph algorithms can be succinctly given by recursive function definitions based on the inductive graph view. We also regard this as a contribution to the teaching of algorithms and data structures in functional languages since we can use the functional-graph algorithms instead of the imperative algorithms that are dominant today.
You can follow Michael at: @mrb_bk or https://github.com/mrb or his blog: http://michaelrbernste.in/.
More details on Idris: A Language With Dependent Types.