A Framework for Resource Dependent EDSLs in a Dependently Typed Language

I am very pleased to announce that my paper describing a framework for constructing Resource Dependent EDSLs in a Dependently Typed Language was accepted to ECOOP 2020. Many of you may have seen this from the conference website itself, and I was waiting until the camera ready copy was produced to properly publicly announce. This was joint work with Wim Vanderbauwhede, and Edwin Brady.

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.

More details will follow around the time of the conference.