Document Open Access Logo

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

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

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.6.2.2.pdf
  • Filesize: 426 kB
  • 3 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

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

Funding

This work was funded by EPSRC projects: Border Patrol: Improving Smart Device Security through Type-Aware Systems Design (http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N028201/1); and Type-Driven Verification of Communicating Systems - http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N024222/1.

Artifact

  MD5 Sum: 9a75e4a5804bee0be7edfcf152ad8f4c (Get MD5 Sum)

Related Article

  • Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede, "A Framework for Resource Dependent EDSLs in a Dependently Typed Language", in 34th European Conference on Object-Oriented Programming (ECOOP 2020), LIPIcs, Vol. 166, pp. 20:1 - 20:31, 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.20

References

  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
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact