2026-07-22T11:40:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13177 2024-03-06T10:49:55Z ddc:004 open_access

A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Pearl) de Muijnck-Hughes, Jan Brady, Edwin Vanderbauwhede, Wim Dependent Types Algebraic Effect Handlers Domain-Specific Languages Embedded Domain Specific Languages Idris Substructural Type-Systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan de Muijnck-Hughes and Edwin Brady and Wim Vanderbauwhede 2020 Is Part Of LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2020.20 urn:nbn:de:0030-drops-131773 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.20 eng https://creativecommons.org/licenses/by/3.0/legalcode