A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact)

Authors Jan de Muijnck-Hughes , Edwin Brady , Wim Vanderbauwhede

Thumbnail PDF

Artifact Description

  • Filesize: 426 kB
  • 3 pages

Document Identifiers

Author Details

Jan de Muijnck-Hughes
  • University of Glasgow, United Kingdom
Edwin Brady
  • University of St Andrews, United Kingdom
Wim Vanderbauwhede
  • University of Glasgow, United Kingdom

Cite AsGet 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)



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
  • Dependent Types
  • Algebraic Effect Handlers
  • Domain-Specific Languages
  • Embedded Domain Specific Languages
  • Idris
  • Substructural Type-Systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. 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.
  2. 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.
  3. 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.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail