A Framework for Resource Dependent EDSLs in a Dependently Typed Language

The Glasgow site are very pleased to announce that their ECOOP 2020 paper & conference video describing a framework for constructing Resource Dependent EDSLs in a Dependently Typed Language is now live. This is 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.

The paper and video can be found online on the conference website.

Apologies in advance for the quiet audio!