Gdzie w programach sens, gdzie logika
Prowadzący: Michał Horodecki
Po co w programach są typy i z czym się to je
Disclaimer: Zdaję sobie sprawę że zadań kwalifikacyjnych jest trochę i mogą nie być najłatwiejsze - dlatego nie trzeba robić wszystkich - zrobienie połowy, w tym nadesłanie częściowych rozwiązań i pomysłów jest ok i z dużym prawdopodobieństwem wystarczy do kwalifikacji.
Opis
Kto pisał w jakimś języku programowania ten niemal na pewno spotkał się z pojęciem typów, chociażby w postaci błędów kompilacji lub w runtimie:
>>> 2 + "pomidor"
Traceback (most recent call last):
File "<python-input-0>", line 1, in <module>
2 + "pomidor"
~~^~~~~~~~~~~
TypeError: unsupported operand type(s) for +: 'int' and 'str'O ile w Pythonie lub C++ sprawa jest względnie prosta - podajemy typy/wartości explicite i jak coś się nie zgadza to rzucamy błędem - to okazuje się że istnieje cały świat rożnorakich pomysłów w Teorii typów które rozważają takie pomysły jak:
- Automatyczne wnioskowanie typów (jak w Haskellu) - zamiast podawać typy argumentów jak C++ zmuszamy kompilator do zrobienia tego za nas
- Zastosowanie typów do dowodzenia twierdzeń (jak w Leanie lub Rocqu (Coqu)) - typ reprezentuje twierdzenie matematyczne, a kompilujący się program jest dowodem jego prawdziwości
- Path Dependent Types w Scali - gdzie typ obiektu zależy od tego kto go stworzył, dzięki czemu nie da się pomieszać obiektów stworzonych w różny sposób
- Gradual typing - gdzie celujemy w coś pomiędzy C++ a Pythonem - z jednej strony niektóre typy chcemy żeby sprawdzał kompilator, z drugiej strony niektóre chcemy zostawić dynamicznymi
- aż po takie dziwactwa jak Homotopy type theory która robi jakąś gęstą matematykę homotopii na typach w programowaniu??? Nie wiem, nie pytajcie mnie, tym się na szczęście nie będziemy zajmować
- I wiele wiele innych, dość ciekawych zagadnień (w tym moja praca magisterska, którą obecnie piszę)
Na warsztatach zajrzymy w głąb króliczej nory i zapoznamy się z podstawami tej cudownej dziedziny na granicy teorii i praktyki informatyki.
Plan jest taki:
- Zaczynamy od czegoś prostego, czyli jak w ogóle opisujemy świat z perspektywy typów, i jak wygląda system od którego wszyscy wychodzą
- Przejdziemy sobie przez kilka różnych ciekawych, w miarę niezależnych od siebie aspektów, które moim zdaniem warto zobaczyć
- Spróbujemy się pobawić, dopisując własny system typów do zabawkowego języka programowania (może przydać się laptop) Z braku chętnych którzy rozwiązali zadania nie jest to planowane. Zamiast tego chętnie opowiem o swojej pracy magisterskiej (która właśnie jest w teorii typów) - jak i co w niej jest ciekawego.
Kontakt
W razie jakichkolwiek wątpliwości lub pytań w sprawie warsztatów i zadań kwalifikacyjnych, zachęcam do kontaktu :) (tylko nie per "Pan" bo poczuję się staro :P)
discord: noobexception#5365 (Michał Horodecki na discordzie www)