DARTS.6.2.2.pdf
- Filesize: 426 kB
- 3 pages
Document
A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact)
Authors
Jan de Muijnck-Hughes 
,
Edwin Brady ,
Wim Vanderbauwhede
-
Part of:
Issue:
Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Volume: DARTS, Volume 6 (ECOOP 2020)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-11-06
Artifact Description
Document Identifiers
Author Details
Cite As Get BibTex
Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede. A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/DARTS.6.2.2
Artifact
DARTS-6-2-2-artifact-9a75e4a5804bee0be7edfcf152ad8f4c.tar.gz
(Filesize: 218.22 MB)
MD5 Sum:
9a75e4a5804bee0be7edfcf152ad8f4c
(Get MD5 Sum)
Abstract
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.
Subject Classification
ACM Subject Classification
- Software and its engineering → General programming languages
- Software and its engineering → Language features
- Software and its engineering → Domain specific languages
- Software and its engineering → System modeling languages
Keywords
- Dependent Types
- Algebraic Effect Handlers
- Domain-Specific Languages
- Embedded Domain Specific Languages
- Idris
- Substructural Type-Systems
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
- Edwin Brady. Programming and reasoning with algebraic effects and dependent types. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 133-144. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500581.
- Edwin Brady. Resource-dependent algebraic effects. In Jurriaan Hage and Jay McCarthy, editors, Trends in Functional Programming - 15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers, volume 8843 of Lecture Notes in Computer Science, pages 18-33. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-14675-1_2.