Функциональные языки. Интро

Слайды про Ur/Web

https://github.com/grwlf/urweb-homepage/blob/master/tut/Slides-Minsk-2014.pdf?raw=true

Вопросы можно задавать на [email protected]

Спасибо за встречу! Особенно понравились доклады про F# и про Fixed-point. Можно ли получить слайды второго? Хочу и в самом деле погонять эту штуку под отладчиком. Про мой собственный доклад об Ur/Web я думаю, что он вышел корявенько. Буду учиться подавать информацию качественнее.

Это не совсем те dependent types, которые в Агде. В своей статье (в слайдах была ссылка) автор Ur/Web описывает разницу. Насколько я понял, дело там в том, что в агде пространство типов бесконечно (есть типы типов, и типы типов типов, и типы типов ... типов), а в Ur/Web оставлено только 2 уровня: типы и типы типов (кайнды). Сделано это сознательно, для упрощения программ. Получилось или нет - спорно, так как сигнатуры функций там бывают зубодробительные, см. файл top.ur из стандартной бибилиотеки. Хотя знатокам Агды, возможно, они не покажутся чем-то сильно сложным.

Именованые поля в кортежах - отдельное нововведение, не связанное с количеством этажей типизации. Такое решение было выбрано автором для "покорения" предметной области - запросов SQL.

Понравились только доклады о F# (первый раз вообще вижу его, всё ясно, понятно) и Why Y. Ну и про эрланг нейтрально, у Макса Лапшина на почти аналогичном митапе в Москве как-то полнее вышло. Опущена вся магия паттерн-матчинга, сообщений, receive-цикла, генериков (хотя это уже весь ЯП, ок). Но если цель была именно просто рассказать о свойствах языка, то ок.

Про Scala непонятно абсолютно ничего. Я даже было стал сомневаться, что знаю как работают тайпклассы. Поэтому я не хочу писать на Scala. Уровень синтаксического шума зашкаливает и в него не вьехать быстро. Хотя это так, мои личные проблемы и субъективность.

Type Providers штука интересная с точки зрения практики, много возможностей самых разных по интеграциям и всему такому.

Но это должно делаться исключительно в компайлтайме и никоим образом не в рантайме, ибо это полностью лишено смысла и лишь бессмысленно уменьшает производительность.

Тайпчекинг придуман не для «точечки в IDE», а чтобы не допускать ошибок рантайма в компайлтайме. Тем более если это изи-пизи реализовать и просто была допущена ошибка.

Доклад про Clojure&ClojureScript был полной противоположностью https://www.youtube.com/watch?v=SyWFvn0I6m8 (советую посмотреть весь полностью, а не нарезку, за час «вдуплился», что такой за FRP).

Ur / Web это не так плохо, как могло бы показаться. Вот та «новинка» которую привнёс разработчик, создав кортежи с именоваными полями (в Haskell'е, они, кстати, тоже есть, только кривые и являются просто функциями, которые достают с нужного места значение из АТД (хотя и есть синтаксис {a = "some", b = [1, 2, 3])) и возможности достать какой-то элемент элемент произвольного кортежа при условии, что мы знаем тип этого нечта на самом деле затрагивает ту область, в которую я сейчас копаю (я бы сказал, которой упарываюсь/болен).

Это зависимые типы. Единственное, наверное, что меня в данный момент интересует и о чём я действительно хотел бы говорить с людьми. Я бы мог написать пост о них, но у меня таких уже не менее двух (более или менее читабельный — https://medium.com/p/49554136ebca ).

Есть Idris'ы всякие, Agda'ы, Coq, в которых они уже есть и на них даже что-то пишется (видел формально верифицированные компиляторы Си, движок браузера).

Но лично я считаю, что у них недостаточно абстрактности и можно полностью отделить формальную спецификацию (описание типа) от её реализации и вообще предоставить выбор реализации компилятору (представьте, что в Java у вас есть лишь интерфейс List, у которого есть разные конструкторы, а конкретный выбирается в зависимости от того, как компилятор оценил вашу задачу/сравнил производительности текущих решений (есть общий репозиторий всех решений), выбрал наиболее подходящее (решения конкурируют между собой за производительность и каждая компиляция может ускорить весь проект в разы)).

А, лол, отвлёкся. В них можно описать, например, кортеж как тип, параметризированный списком типов. Затем не составляет труда для любого произвольного кортежа получить любой порядковый элемент, предоставив доказательство, что на соответствующем месте этого списка типов стоит тип, который мы ожидаем получить.

В общем, неплохое событие. Я сам не минский, поэтому если они сильно часто будут, не смогу посещать все, ибо работу из-за своей лени и лени я так и не нашёл :).

Слайды с доклада "F# for Data*" http://www.slideshare.net/sergeytihon/f-for-data

Есть будут еще какие-то вопросы - пишите в твиттер @sergey_tihon (всем отвечу).

Продолжение следует: более подробный рассказ на следующей встрече http://www.meetup.com/fsharpminsk/events/214812192/