Žiga Lukšič: Types with local algebraic theories

Date of publication: 27. 11. 2018
Mathematics and theoretical computing seminar
Četrtek, 29. 11. 2018, od 11h do 13h, učilnica 3.07, Jadranska 21
Abstract: In this talk I will present a type system with equations, aimed at languages which include algebraic effects and handlers. In the original paper of Plotkin and Pretnar, heavy restrictions were imposed on handlers in order for them to be deemed correct. However those restrictions were removed to allow for a greater variety of handlers, but in the process sacrificing a great deal of reasoning and safety. With the new type system, we aim to reclaim easier reasoning, improved safety, and hopefully even opening ways for future compiler optimisations. In cases where the code is obscure or unobtainable, the new type system also offers partial insight into the behaviour of handlers, making handlers seem less mysterious and intimidating.