A Framework for Resource Dependent EDSLs in a Dependently Typed Language

My ECOOP2020 video & paper detailing how one can create Resource-Dependent EDSLs in Idris are out!

They can be found online on the conference website. Apologies in advance for the quiet audio!

Idris’ Effects library demonstrates how to embed resource dependent algebraic effect handlers into a dependently typed host language, providing run-time and compile-time based reasoning on type-level resources. Building upon this work, RESOURCES is a framework for realising Embedded Domain Specific Languages (EDSLs) with type systems that contain domain specific substructural properties. Differing from Effects, RESOURCES allows a language’s substructural properties to be encoded within type-level resources that are associated with language variables. Such an association allows for multiple effect instances to be reasoned about autonomically and without explicit type-level declaration. Type-level predicates are used as proof that the language’s substructural properties hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types provide correctness-by-construction guarantees that substructural properties of written programs hold.

This is joint work with Wim Vanderbauwhede & Edwin Brady.