A Framework for Resource Dependent EDSLs in a Dependently Typed Language

The Glasgow site are very pleased to announce that their paper describing a framework for constructing Resource Dependent EDSLs in a Dependently Typed Language was accepted to ECOOP 2020. This was joint work with 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.