2016-02-18 - Lambda Days 2016

Zaczniemy od propagandy, czyli - ludzie, płaćcie składki JUGa, bo można wygrać wejściówki na konferencje :)

Wejściówkę wygrałem i pojechałem na Lambda Days do Krakowa, 18-19 lutego 2016 r. Prelekcje odbywały się równolegle w 3 salach Auditorium Maximum UJ.

Na początek...

...muszę wspomnieć o niemym bohaterze tego wydarzenia, czyli aplikacji do głosowania. Prosta, ładna - jeden ekran, trzy emotki (yay, meh, ney), które wdzięcznie pulsują pod palcami kolejnych uczestników. Po zakończeniu każdej prelekcji przed przed drzwiami czekał człowiek z obsługi z tabletem w ręku. Wyniki nie były jawne, ale widać było, że dużo osób oddaje głosy i kosztuje ich to minimum wysiłku.

Pakiet startowy, oprócz identyfikatora, obejmował płócienną torbę w logiem, stos ulotek, cukierki z masy cukrowej z małą lambdą oraz ołówek. O papierowy program trzeba było poprosić w rejestracji, naraz tylko na jeden dzień. I od razu nieaktualny, ale to uroki druku.

Przybyłem na miejsce kilka minut po otwarciu rejestracji, więc było mi dane zobaczyć jak ktoś na szybko prasuje narzutę na stoisku sponsorskim, a korytarze powoli zapełniają się uczestnikami.

Wszystkie prelekcje były nagrywane, a plotka głosi, że powinny pojawić się w ciągu miesiąca. Zobaczymy! Pierwsze zaczęły się już pokazywać na YouTube, więc polecam odwiedzić stronę konferencji, a potem wyszukać tytułami prelekcje.

Aktualizacja: filmy pojawiają się na stronie konferencji! Wystarczy wejść w profil prelegenta, by zobaczyć udostępnione materiały.

Pierwszy dzień...

...rozpoczął się krótkim wstępem, opóźnionym o 20 minut, ale i tak zdążyli przejść przez wszystkie slajdy powitalne.

Wstępniak płynnie przeszedł w pierwszy keynote - Propositions as Types. Philip Wadler, po wstępie historycznym opowiadał o paralelach między logiką a programowaniem (a dokładniej prosto typowanym rachunkiem lambda), które zostawili nam po sobie Haskell Curry i William Howard - w skrócie - program jest tezą, a jego wykonanie dowodem. Jednym z wniosków wykładu było to, że są języki programowania, które ktoś odkrył czy tez zbudował wokół odkrycia (matematycznego), a są też takie, które ktoś wyssał z palca, jak Java czy C++. Te pierwsze są lepsze. Nazwiska do zapamiętania (i prace do do przeczytania): Hilbert (Entscheidungsproblem), Gödel (Incompleteness, Recursive functions), Church (Lambda calculus), Turing (Turing Machines). Na zakończenie dowiedzieliśmy się, że najnowszym problemem, nad którym pracuje też sam Wadler, są typy sesyjne, opisane po raz pierwszy przez Kohei Hondę w 1993, a wywiedzione z logiki linowej (Jean-Yves Girard, 1987). Jest już nagranie!

A brief history of history of programming languages: sprawdźcie kto stworzył ALGOLa, a następnie przeczytajcie przynajmniej po jednej publikacji każdego z autorów. Jeszcze tego nie zrobiłem, ale najwyraźniej warto!

The mysteries of Dropbox: testowanie synchronizacji plików jest trudne - autor QuickChecka, John Hughes, zrobił to z kolegami za pomocą laptopa, kilku maszyn wirtualnych i QuickChecka dla Erlanga. Nie było to robione na zlecenie Dropboksa! Polecam przeczytać opis metodologii, bo omawia, jak przetestować złożony system za pomocą losowych danych. Tak, znaleźli kilka przypadków brzegowych i zgłosili je Dropboksowi.

Zaliczyłem dwie sesje o Data Science, które pokazały jak powinno się promować DS - za pomocą ciekawych pytań! Pierwsza z nich zaraz po lunchu: A board game night with geeks i pytanie: czy można zremisować w Quarto? Quarto to gra planszowa, w której trzeba na planszy 4x4 ułożyć w rzędzie, kolumnie lub kwadracie zestaw klocków, które mają wspólną cechę. Jeśli użyjecie SAT solvera, to dowiecie się, że owszem, można w tej grze zremisować. Kod i prezentacja są dostępne na GitHubie. Tych samych metod używa się, m. in., przy planowaniu rozkładów, testowaniu i sekwencjonowaniu DNA.

W następnej prelekcji - Teaching functional programming to n00bs in mobs - Rob Martin przekonywał, że powinniśmy uczyć wszystkich juniorów programować funkcyjnie! Dlaczego? Bo nauczyć ich funkcyjnego myślenia jest prościej niż seniorów, trudno jest zatrudnić dobrego seniora, a ci seniorzy, których już masz, będą się lepiej rozwijać, jeśli będą mogli kogoś uczyć. Do tego dwie lektury podane przez prelegenta: Why Functional Programming Matters i Why "Why Functional Programming Matters" Matters. Druga część prelekcji była pochwałą dla “mob programming”. Programowanie grupowe - 4-15 osób siedzi nad jednym problemem, tylko jedna klawiatura i myszka, jeden (duży) monitor. W takim środowisku powstaje lepszy kod (prezentacja z perspektywy roku) i sprzyja ono równomiernemu rozwijaniu kompetencji - w grupie większość stanowią juniorzy. I jeśli chcecie rozumieć funkcyjne koncepcje lepiej, to uczcie się Haskella ;)

Byłem na dwóch “małych” prelekcjach. Pierwsza, Elixir and Elm - the perfect couple, wychwalała duet Elm + Elixir, zaznaczając jednocześnie, by starać się wybierać narzędzie (język, framework itd.) do potrzeb, zamiast używać zawsze złotego młotka. Druga, Embracing change - how to introduce Clojure into your company technology stack seamlessly, traktowała o tym, jak wprowadzić Clojure, albo jak twierdził autor - dowolną nową technologię, do swojej organizacji. Krok pierwszy: zdobądź pierwszych wyznawców, krok drugi: wybierz mały, niekrytyczny projekt, krok trzeci: ???, krok czwarty: profit, nowa technologia została wprowadzona. Prelegentowi się udało, a prostym projektem był serwis do healthchecku, który odpowiadał tylko “żyję!”, jeśli serwer działał.

Na koniec pierwszego dnia odbyło się 5 lightning talków, które niestety przegapiłem, bo dołączyłem do grupy dopytującej Roba Martina, jak np. mierzyć wydajność pojedynczych pracowników w takim programistycznym tłumie. Po pierwsze: nie rób tego, używaj retrospektyw żeby dawać sobie wzajemną informację zwrotną, przy czym jeśli jesteś zwierzchnikiem, to najlepiej nic nie mów, żeby niechcący nie uciszyć jakiejś inicjatywy (prowadzącemu się to raz zdarzyło). Po drugie: jeśli masz nóż na gardle, to zrób 360 Review.

Afterparty było w The Legend Music Club.

Drugi dzień...

...otworzył moim zdaniem najsłabszy z 3 keynote’ów - Things that Matter autora Siedem języków w siedem tygodni. W skrócie: języki, których autorom przyświecała jakaś idea i którzy pozostali jej wierni są fajne (i o nich poczytacie w książce, jest Haskell!), a Java jest zmyślona.

Pierwsza zwykła prezentacja, na którą trafiłem to The Zen of Akka prowadzona przez Konrada Malawskiego z Typesafe’a (teraz Lightbend). Zen Akki składa się z 13 punktów, których jednak nie pokuszę się o szczegółowe omówienie i będziecie musieli wyciągnąć je z nagrania, kiedy się ukaże. Kilka przykładów to:

• Używajcie niemodyfikowalnych wartości i unikajcie jak ognia modyfikowalnych zmiennych; 
• Unikajcie javowej binarnej serializacji - użyjcie Kryo, Thrifta, ProtoBufa albo czegokolwiek innego, co nie jest domyślnym mechanizmem; 
• Akka to nie framework - to zestaw narzędzi - można z niego wybrać swoje ulubione części i nie wkładać do projektu całości. 

Do poczytania - rozproszone strumienie dla Akki, o których prowadzący wspomniał w odpowiedzi na jedno z pytań po prezentacji: Intel Gear Pump.

Druga prezentacja tego dnia to druga sesja z Data Science: The F#orce awakens, czyli kto jest najważniejszą postacią w Star Wars i dlaczego epizody I-III mają kiepskie oceny? Trzeba dokonać analizy grafu stworzonego ze sparsowanych scenariuszy Gwiezdnych Wojen. W samej analizie pomaga nam język R. W epizodach I-VI najważniejszy jest Obi-Wan, a jeśli dołożymy VII, to jest to C3-PO! Ale to tylko wierzchołek góry lodowej, dużo więcej znajdziecie na blogu autorki: The Star Wars social network, Star Wars social networks: The Force Awakens. W prawdziwym życiu tych samych technik używa się do analizy rozmów online przez czaty, e-maile, przy pracy z siatkami zaopatrzenia czy też do analizy sieci biologicznych.

Następna prezentacja, Getting started with Frege [czyt. frige], zachęcała do zapoznania się z implementacją składni Haskella dla JVM. Za przykład posłużyła prosta aplikacja do walidacji JSONa. Język kompiluje się do Javy, nie do bytecode’u. Chciałbym coś więcej o tym powiedzieć, ale sama implementacja jeszcze nie jest w pełni kompatybilna, więc niestety nie będzie mi dane wprowadzić jutro Haskella do projektu niskim kosztem ;) Można oczywiście obserwować projekt na GitHubie.

Kolejną była prezentacja dwóch ludzi z TomToma, którą mogliście zobaczyć już na spotkaniu JUGa - Practical demystifcation of CRDT. CRDT to Conflict-free Replicated Data Type. Tło prezentacji to usługa synchronizacji dla danych z nawigacji (np. ulubionych miejsc, zapisanych tras). Magia tych typów polega na tym, że obsługują przemienną i przechodnią operację łączenia, dzięki czemu nie ma znaczenia w jakiej kolejności nakładane są zmiany - wynik będzie zawsze taki sam. Omówili typy danych, których używają, dochodząc do tego, że musieli wymyślić własny, bazujący na OR-Set (Observed/Removed Set), OUR-Set (OR-Set + Updated). Taki zbiór trzyma w sobie listy utworzony, zaktualizowanych i usuniętych obiektów. Jednym z problemów przy używaniu CRDT jest brak niezawodnego zegara, więc kompromisem jest taka priorytetyzacja dostępnych czasów: zegar GPS > czas serwera > czas lokalny+1 > czas lokalny. Prelegenci powiedzieli, że byli na prezentacji Johna Hughesa, więc dowiedzieli się też o nowych sposobach, w jaki mogą ten system przetestować. Post, który zainspirował prelegentów do zgłębienia tematu: CRDTs for fun and eventual profit.

Ostatnia zwykła prelekcja to Purely Functional Web Apps, która opowiadała historię aplikacji internetowej napisanej w Haskellu i Elmie. Potrzebowali aplikacji, która na podstawie historii pull requestów z ich GitLaba ekstrapolowała potencjalną długość trwania review w zależności od ilości kodu. Do części serwerowej użyty został zestaw narzędzi Haskell Servant. Po stronie Elma za to pomocny okazał się jego Time Traveling Debugger, który używanie wygląda jak pokaz magiczny. Padło też zdanie, że powinniśmy nauczyć się Haskella, bo dzięki temu staniemy się lepszymi programistami.

Ostatni keynote - The Truth about Types Bartosza Milewskiego - mówił o teorii kategorii. Kategoria to byt matematyczny, który składa się z obiektów, przekształceń między nimi (strzałek) i operacji łączenia ze sobą strzałek. Dowiedzieliśmy się, że tak jak istnieją paralela między logiką i rachunkiem lambda, tak można wykazać paralelę między nimi i teorią kategorii. Prezentacja była mocno abstrakcyjna. Przeszliśmy przez Kategorię Zbiorów (Set Category), intuicjonistyczną logikę, kontynuacje, a zakończyliśmy stwierdzeniem, że skoro istnieją analogie między tymi trzeba dziedzinami (logika, rachunek lambda, teoria kategorii), to może istnieje jakaś większa abstrakcja, która obejmie je wszystkie? Tym właśnie zajmują się teraz badacze. Niestety nam, zwykłym zjadaczom chleba, pozostaje czekać.

Koniec!

Wyjazd uznaję za udany, konferencja bardzo mi się podobała. Mam nadzieję, że będę mógł pojechać na nią również w przyszłym roku :)