Matija Pretnar: Za algebrajske učinke in prestreznike ne potrebujemo omejitve na vrednosti

Datum objave: 11. 1. 2016
Seminar za temelje matematike in teoretično računalništvo
Torek, 12. 1. 2015, od 12h do 14h, Plemljev seminar, Jadranska 19
Za algebrajske učinke in prestreznike ne potrebujemo omejitve na vrednosti
Za algebrajske učinke in prestreznike bom predstavil enostaven sistem tipov s Hindley-Milnerjevim polimorfizmom, ki omogoča generalizacijo tipov poljubnih izračunov in ne zgolj vrednosti. Rezultat je presenetljiv, saj je znano, da je Hindley-Milnerjev polimorfizem v prisotnosti računskih učinkov potrebno omejiti, kljub temu pa lahko precej teh učinkov izrazimo s prestrezniki. V sodelovanju z Ohadom Kammarjem.

No value restriction is needed for algebraic effects and handlers
I will present a straightforward sound Hindley-Milner polymorphic type system for algebraic effects and handlers which allows type variable generalisation of arbitrary computations, and not just values. This result is surprising as the soundness of Hindley-Milner polymorphism is known to fail when not restricted in the presence of computational effects, but many of those effects may be expressed using handlers. Joint work with Ohad Kammar.