Combining effects with dependent types
Thesis title in Czech: | Combining effects with dependent types |
---|---|
Thesis title in English: | Combining effects with dependent types |
Key words: | dependent types|effect handlers|type systems |
English key words: | dependent types|effect handlers|type systems |
Academic year of topic announcement: | 2023/2024 |
Thesis type: | Bachelor's thesis |
Thesis language: | |
Department: | Department of Distributed and Dependable Systems (32-KDSS) |
Supervisor: | Mgr. Tomáš Petříček, Ph.D. |
Author: | hidden - assigned and confirmed by the Study Dept. |
Date of registration: | 26.03.2024 |
Date of assignment: | 26.03.2024 |
Confirmed by Study dept. on: | 04.04.2024 |
Date of electronic submission: | 08.05.2024 |
Opponents: | Mgr. Vít Šefl |
Guidelines |
There are multiple directions in the development of advanced and more expressive type systems for programming languages. On the one hand, algebraic effect handlers [6] are used to control how programs affect the world. On the other hand, dependent types [4, 7] make it possible to express richer properties using types. There is some work on combining those [8], but the design space for programming languages that combine multiple advanced type system features remains largely unexplored.
The aim of this thesis is to design a programming language that combines multiple of the recent research directions on advanced type system. The developed programming language may support a form of effect system inspired by Koka, Eff or Effekt [1, 2, 3] alongside with a form of dependent types [4] and may utilize bidirectional type checking [5] in the implementation. The thesis will focus on formally specifying the type system of the dependently typed core language with an extension for tracking effects. |
References |
[1] Brachthäuser, J. I., Schuster, P., & Ostermann, K. (2020). Effekt: Lightweight effect polymorphism for handlers. Technical Report. University of Tübingen, Germany.
[2] Leijen, D. (2014). Koka: Programming with row polymorphic effect types. arXiv preprint arXiv:1406.2061. [3] Bauer, A., & Pretnar, M. (2014). An effect system for algebraic effects and handlers. Logical methods in computer science, 10. [4] Löh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae, 102(2), 177-207. [5] Christiansen, D. R. (2013). Bidirectional typing rules: A tutorial. Available at: https://davidchristiansen.dk/tutorials/bidirectional.pdf [6] Plotkin, G., & Pretnar, M. (2009). Handlers of algebraic effects. In European Symposium on Programming (pp. 80-94). Berlin, Heidelberg: Springer Berlin Heidelberg. [7] Bove, A., Dybjer, P., & Norell, U. (2009). A brief overview of Agda–a functional language with dependent types. In Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings 22 (pp. 73-78). Springer Berlin Heidelberg. [8] Brady, E. (2013). Programming and reasoning with algebraic effects and dependent types. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (pp. 133-144). |