Maciej Piróg: Algebry szyte na miarę efektów
We wtorek 27 lutego o godzinie 12.30 odbędzie się seminarium wydziałowe (Instytut Informatyki, sala 119).
Prelegentem będzie Maciej Piróg, adiunkt w Instytucie Informatyki (absolwent naszych studiów informatycznych, doktorat na Oksfordzie, postdoc w KU Leuven), który prowadzi badania w obszarze semantyki formalnej języków programowania, wykorzystując metody algebry uniwersalnej w opisie tzw. efektów obliczeniowych.
Wygłosi od odczyt Algebry szyte na miarę efektów.
Przed wykładem, o godz. 12:00 Dziekan zaprasza na kawę i ciastka.
Dożyliśmy czasów programowania w chmurze, architektur heterogenicznych, systemów masywnie współbieżnych i rozproszenia na astronomiczną skalę. Opanowanie tej złożoności wymaga nowych pomysłów na sztukę tworzenia oprogramowania na poziomie wzorców, konwencji, języków programowania, bibliotek i systemów. Szczelne abstrakcje, które do niedawna były mrzonką bujających w obłokach idealistów, stają się codzienną koniecznością zwykłego programisty.
Popularność zyskują pomysły pochodzące ze świata programowania funkcyjnego, takie jak czystość czy bezstanowość. Podczas tej prezentacji zajmiemy się ich bardziej świadomym rozwinięciem: teorią efektów obliczeniowych, czyli tym, co, prócz przetworzenia danych wejściowych na dane wyjściowe, wolno danemu komponentowi: Czy wolno mu zgłosić wyjątek? A może wolno mu porozmawiać z bazą danych? Jednym z podejść do tematu są tzw. efekty algebraiczne, które powstały na przecięciu teorii języków programowania, algebry uniwersalnej i teorii kategorii. Rozwiązują one w elegancki sposób kilka znanych od dekad problemów związanych z efektami, np. problem definiowania nowych efektów przez użytkownika, składania efektów ze sobą, statycznych gwarancji bez konieczności uciekania się do nienaturalnego stylu programowania z monadami.
Punktem wyjścia będzie algebraiczność efektów, czyli odpowiedniość między efektami a odpowiednio rozumianymi teoriami algebraicznymi. Już najprostsze teorie odpowiadają podstawowym efektom: przemienne monoidy odpowiadają programom z niedeterminizmem, (uogólnione) pasy to czytanie ze środowiska, a moduły nad monoidami to zapisywanie. Można więc badać istniejące i definiować nowe efekty przez pryzmat algebry. Podczas prezentacji opowiem nie tylko o tych klasycznych konstrukcjach, ale także o nowszych wynikach, np. o tym, jak pewne pozornie niealgebraiczne konstrukcje można opisywać tzw. algebrami z zakresami [Piróg, Schrijvers, Wu, Jaskelioff, LICS 2018] czy o pierwszej równościowej teorii niedeterminizmu z globalnym stanem [Piróg, Polesiuk, Sieczkowski, FOSSACS 2019].
