A framework for resource dependent EDSLs in a dependently typed language (Artifact)

Muijnck-Hughes, Jan de and Brady, Edwin C. and Vanderbauwhede, Wim (2020) A framework for resource dependent EDSLs in a dependently typed language (Artifact). Dagstuhl Artifacts Ser., 6 (2). 02:1-02:3. (https://doi.org/10.4230/DARTS.6.2.2)

[thumbnail of Muijnck-Hughes-etal-DAS2020-A-framework-resource-dependent-EDSLs-dependently-typed-language-Artifact]
Preview
 Text. Filename: Muijnck_Hughes_etal_DAS2020_A_framework_resource_dependent_EDSLs_dependently_typed_language_Artifact.pdf
Final Published Version
License: Creative Commons Attribution 3.0 logo
Download (436kB)| Preview

Abstract

dris' 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.

CORE (COnnecting REpositories)