Show simple item record

dc.contributor.advisorPlotkin, Gordon
dc.contributor.advisorStark, Ian
dc.contributor.authorAhman, Danel
dc.date.accessioned2018-03-13T11:37:40Z
dc.date.available2018-03-13T11:37:40Z
dc.date.issued2017-11-30
dc.identifier.urihttp://hdl.handle.net/1842/28788
dc.description.abstractWe study the interplay between dependent types and computational effects, two important areas of modern programming language research. On the one hand, dependent types underlie proof assistants such as Coq and functional programming languages such as Agda, Idris, and F*, providing programmers a means for encoding detailed specifications of program behaviour using types. On the other hand, computational effects, such as exceptions, nondeterminism, state, I/O, probability, etc., are integral to all widely-used programming languages, ranging from imperative languages, such as C, to functional languages, such as ML and Haskell. Separately, dependent types and computational effects both come with rigorous mathematical foundations, dependent types in the effect-free setting and computational effects in the simply typed setting. Their combination, however, has received much less attention and no similarly exhaustive theory has been developed. In this thesis we address this shortcoming by providing a comprehensive treatment of the combination of these two fields, and demonstrating that they admit a mathematically elegant and natural combination. Specifically, we develop a core effectful dependently typed language, eMLTT, based on Martin-L¨of’s intensional type theory and a clear separation between (effect-free) values and (possibly effectful) computations familiar from simply typed languages such as Levy’s Call-By-Push-Value and Egger et al.’s Enriched Effect Calculus. A novel feature of our language is the computational S-type, which we use to give a uniform treatment of type-dependency in sequential composition. In addition, we define and study a class of category-theoretic models, called fibred adjunction models, that are suitable for defining a sound and complete interpretation of eMLTT. Specifically, fibred adjunction models naturally combine standard category-theoretic models of dependent types (split closed comprehension categories) with those of computational effects (adjunctions). We discuss and study various examples of these models, including a domain-theoretic model so as to extend eMLTT with general recursion. We also investigate a dependently typed generalisation of the algebraic treatment of computational effects by showing how to extend eMLTT with fibred algebraic effects and their handlers. In particular, we specify fibred algebraic effects using a dependently typed generalisation of Plotkin and Pretnar’s effect theories, enabling us to capture precise notions of computation such as state with location-dependent store types and dependently typed update monads. For handlers, we observe that their conventional term-level definition leads to unsound program equivalences becoming derivable in languages that include a notion of homomorphism, such as eMLTT. To solve this problem, we propose a novel type-based treatment of handlers via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a family of value terms (the operations). This type internalises Plotkin and Pretnar’s insight that handlers denote algebras for a given equational theory of computational effects. We demonstrate the generality of our type-based treatment of handlers by showing that their conventional term-level presentation can be routinely derived, and this treatment provides a useful mechanism for reasoning about effectful computations. Finally, we show that these extensions of eMLTT can be soundly interpreted in a fibred adjunction model based on the families of sets fibration and models of Lawvere theories.en
dc.contributor.sponsorotheren
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionD. Ahman, J. Chapman, and T. Uustalu. When is a container a comonad? Logical Methods in Computer Science, 10(3), 2014.en
dc.relation.hasversionD. Ahman, N. Ghani, and G. D. Plotkin. Dependent types and fibred computational effects. In B. Jacobs and C. L¨oding, editors, Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016, volume 9634 of LNCS, pages 1–19. Springer, 2016.en
dc.relation.hasversionD. Ahman, C. Hrit¸cu, K. Maillard, G. Mart´ınez, G. Plotkin, J. Protzenko, A. Rastogi, and N. Swamy. Dijkstra monads for free. In A. D. Gordon, editor, Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL 2017, pages 515–529. ACM, 2017.en
dc.relation.hasversionD. Ahman and G. D. Plotkin. Refinement types for algebraic effects (extended abstract). In T. Uustalu, editor, Book of abstracts of the 21th Meeting ”Types for Proofs and Programs”, TYPES 2015, pages 10–11. Inst. of Cybernetics at TUT, 2015.en
dc.relation.hasversionD. Ahman and S. Staton. Normalization by evaluation and algebraic effects. In D. Kozen and M. Mislove, editors, Proc. of 29th Conf. on the Mathematical Foundations of Programming Semantics, MFPS XXIX, volume 298 of ENTCS, pages 51–69. Elsevier, 2013.en
dc.relation.hasversionD. Ahman and T. Uustalu. Update monads: Cointerpreting directed containers. In R. Matthes and A. Schubert, editors, Post-proc. of the 19th Meeting “Types for Proofs and Programs”, TYPES 2013, volume 26 of LIPIcs, pages 1–23. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, Dagstuhl Publishing, 2014.en
dc.subjectdependent typesen
dc.subjectcomputational effectsen
dc.subjectdependently typed programming languagesen
dc.titleFibred computational effectsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record