Категории типов. Часть 8.1. Вертикальная композиция эффектов

Одной из важнейших проблем в программировании с предсказуемым управлением эффектами является композиция монад. В этой статье мы рассмотрим наиболее общие подходы к решению этой задачи.

От Lisp до Haskell

Одной из важнейших проблем в программировании с предсказуемым управлением эффектами является композиция монад. В этой статье мы рассмотрим наиболее общие подходы к решению этой задачи.

Выбор языка программирования (ЯП) отражает стиль мышления разработчика. Однако если какой-то язык называют «популярным», это вовсе не значит, что он самый перспективный и единственно достойный глубокого изучения. Просто в данный момент он чаще на слуху по разным причинам. Это может быть следствием лёгкости освоения, востребованности в какой-то быстро растущей и специфической отрасли, ошибкой интерпретации статистических данных или просто хайпом. В этой статье вместе с разработчиками и исследователями компании «Криптонит» мы проследим динамику рейтингов ЯП, разберёмся, что скрывается за всплесками интереса к разным языкам, какие из них действительно востребованы и почему.
Для понимания общей картины рассмотрим подробнее, что говорят о популярности ЯП в источниках с разной методологией и оценим динамику.

Добрый день,Хаброжители! Сегодня мы подготовили для вас перевод статьи.
В статье рассматривается переход от взаимодействия человек-агент к полностью автономным системам. Авторы подчеркивают, что такие агенты представляют собой сложные распределенные системы, требующие надежного и отказоустойчивого дизайна.
Вдохновляясь принципами языка Erlang, они представляют библиотеку ramure, которая позволяет легко создавать и оркестровать надежные агентные процессы с прозрачным мониторингом и механизмами восстановления.

Несмотря на все усилия Бурбаки, Коши и Вейерштрасса, подлинно формальные доказательства всегда оставались предметом теории, а не практики. Некоторые математики теперь надеются, что компьютеры смогут это изменить.
Начиная с 1960-х годов исследователи разрабатывают компьютерные программы, называемые системами интерактивного доказательства. Используя такую систему, математик записывает каждую строку доказательства (включая каждое определение) на языке, понятном компьютеру, а затем система проверяет логику. Если хотя бы один шаг не вытекает из предыдущего — если не доказана каждая мелочь вплоть до того, что 1 + 1 = 2, — программа не примет доказательство.
Сейчас учёные надеются формализовать всю математику с помощью системы интерактивного доказательства под названием Lean. Уже создана библиотека, содержащая более 120 000 определений, и проверено четверть миллиона теорем. Несколько математиков поддерживают эту базу данных, обновляя её и проверяя новые данные. (Некоторые из них занимаются этой работой полный рабочий день.) Они уже получили более 10 миллионов долларов финансирования, в основном от миллиардера-финансиста Алекса Герко.

На машиностроительном заводе с цехом в несколько десятков единиц оборудования загрузка станков всю жизнь считалась «на глаз» — сменный мастер периодически обходил цех и делал отметки в бумажном журнале. Но сколько именно часов конкретный токарный станок фактически резал металл, а сколько просто стоял включенным вхолостую — без цифрового инструмента понять это было невозможно. В этой статье я разберу конкретное решение на базе беспроводной Zigbee-сети. Простой и дешевый мониторинг вместо кабелей и полностью открытый программный стек.

Недавно попалось на глаза одно очень интересное видео с динамическими шкалами по популярности разных языков программирования по годам (вроде как, начиная с 1980х). Удивительно, сколько всего и как много придумало человечество. И как быстро меняются тренды, а еще - сколько всего уникального уходит в тень истории. Вот был такой Лисп. Принято считать, что Лисп - это что-то из учебников по истории программирования. Где-то между перфокартами и первыми компиляторами. Условный артефакт. Язык, которым пользовались бородатые профессора, пока не пришел Python и не навел порядок.
Только вот Python тоже унаследовал из Лиспа некоторую часть. Но не все. Самое радикальное так и не забрал.

Здесь мы разбираем реализации основных возможностей расширений Кана и некоторые частные случаи. Большое внимание уделено устройству свободной монады, как монады коплотности различных забывающих функторов.

Здесь я (переводчик) собрал ссылки на все части цикла, написанного Скоттом Влащиным. И заодно перевёл предисловие, буквально, три абзаца.
Если вы захотите поделиться переводом, сбрасывайте ссылку именно на этот пост, потому что в нём есть все остальные ссылки.

Что ж, завершается цикл статей о проектировании, основанном на типах. Скотт показывает изначальный код (короткий) и сравнивает его с финальным кодом (длинным). И объясняет, почему размер — это хорошо.
Есть повод для размышлений!

Можно ли использовать размеченные объединения с одним вариантом (SCDU, Single Case Descriminated Unions) не только со строками, но и с другими типами? Можно ли накладывать бизнес-ограничения на такие штука, как количество позиций в заказе или дата рождения?
Скотт Влащин делится секретами разработки бизнес-логики на языке с алгебраическими типами. Подробности внутри.

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

В этот раз мы разберём, как пересвёртка рекурсивных структур данных помогает в решении задач динамического программирования.

Пятый пост Скотта Влащина посвящён конечным автоматам (они же машины состояний или даже стейт-машины). Функциональные языки хорошо подходят для реализации конечных автоматов, а конечные автоматы хорошо подходят для реализации бизнес-логики.
Попробуем?

Четвёртый пост из серии Скотта Влащина посвящена предметной области. Как с помощью типов описывать бизнес-правила? Как типы позволяют углубить понимание предметной области?
Узнаем прямо сейчас.

Привет, Хабр! Меня зовут Артём Корсаков. Я пишу на Scala и руковожу группой разработчиков в компании «Криптонит», а также веду Scalabook — русскоязычную базу знаний по Scala и функциональному программированию. В этой статье расскажу про обработку ошибок в библиотеке http4s на Scala 3. Мы разберём, как настроить декодирование запросов так, чтобы клиент получал не просто код “500” или “422” с общим сообщением, а сразу видел развёрнутый список всех проблем в запросе. Например, что логин уже занят, пароль содержит недопустимые символы, а капча не введена.
Пожалуй, самая раздражающая ошибка — это получение кода “500” в ответ на запрос, который ты десять раз перепроверил, сверился с документацией и уверен на все 100%, что запрос рабочий. Даже на 110%!
В такие моменты раздражённо думаешь: “Что же этому серверу надо? Я же чётко сформулировал запрос!
Ответить на этот вопрос порой сложно. Например, я хочу зарегистрироваться на сайте, ввожу логин/пароль и получаю сообщение "Internal Server Error". Первое желание – тут же покинуть сайт и поискать более дружелюбный.
Давайте подумаем, как можно сделать сообщение об ошибке более информативным. Для этого будем использовать Scala 3, уточняющие типы и http4s.
Представим, что мы создаём API сервиса авторизации, который (помимо прочего) должен регистрировать новых пользователей.
Для начала определим структуру данных для создания нового пользователя.

Новая глава из цикла Скотта Влащина. Обсуждаем, как сделать код надёжным с помощью развитых типов из F#.

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

Реализация ключевых конструкций лямбда‑исчисления на Python и объяснение их работы. Подойдёт даже тем, кто не очень знаком с Python.
Если хотите понять, как из одних лишь функций строятся булевы, списки и числа и, быть может, попробовать дойти до реализации некоторых алгоритмов самостоятельно — добро пожаловать под кат.
Я давно вынашивал желание написать эту статью. И, наверное, мне бы стоило потратить некоторое время на то, чтобы написать её чуть более структурно и продуманно, но, пожалуй, я её в таком случае вообще не напишу, так что - статья будет ad hock, прям from the top of my mind.
Начнём с того, что в обсуждениях объектного программирования бытуют несколько популярных мнений
Мотивацией для написания этого поста стали два года собеседований JS/TS-инженеров. Я интересуюсь языками и функциональным программированием, поэтому всегда «разбавлял» технические вопросы разговором о парадигмах. И заметил любопытную асимметрию.
Об ООП кандидаты рассуждали уверенно — но в основном на концептуальном уровне, не вдаваясь в то, как именно ООП реализовано в JavaScript. С FP картина была другой: уверенности меньше, зато критика — конкретная и повторяющаяся: «иммутабельность дорогая по памяти», «рекурсия небезопасна из-за стека». Что характерно — эти аргументы почти всегда были сформулированы через опыт работы с JS, а не с Haskell, Clojure или Scala.
Это важная деталь. Любая парадигма существует на двух уровнях: концептуальном (идеальная модель) и имплементационном (как конкретный язык эту модель выражает). Судить о FP по JS — примерно то же самое, что судить об ООП по bash-скриптам с глобальными переменными.
Параллельно я регулярно слышал, что JS — функциональный язык. Аргументы варьировались от «там есть .map()» до рассуждений о чистых функциях и каррировании. Именно это и стало поводом для поста: я хочу объяснить, что я считаю функциональным языком — и почему JS таковым не является. Не перечислить отсутствующие фичи, а показать, почему их нет и что это значит в реальном рантайме.