Today, I gave an extended talk about Resource Dependent EDSLs in a Dependently Typed Language at the MSP101 Seminar Series of the MSP Group at the University of Strathclyde. This was joint work with Wim Vanderbauwhede, and Edwin Brady.
While many people use dependent types for theorem proving some of us like to use dependent types for building, and running, safer programs.
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 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. We use type-level predicates as proof that a language’s substructural properties hold.
Using Resources we have shown how to provide correctness-by-construction guarantees that substructural properties of written programs hold when working with =Files=, specifying Domain Specific =BiGraphs=, and Global Session Descriptions—=Sessions=. With this talk I want to discuss the how and why of Resources, and show how we can use the framework to build EDSLs with interesting type-systems.
This talk is part practise talk for ECOOP 2020, part tutorial on an important idiom for practical dependently-typed programming, and part chance to highlight more how dependent-types are useful when programming in the real world.