Категории типов. Итоги
Обзор, посвящённый применению элементов теории категорий в программировании, завершён. Настало время подвести его итоги.

От Lisp до Haskell
Обзор, посвящённый применению элементов теории категорий в программировании, завершён. Настало время подвести его итоги.

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

Как построить гибкий реактивный граф обработки данных, где узлы изолированы друг от друга, а связи между ними строятся автоматически на основе их возможностей? Рассказываю о разработке Transferum — легковесной TypeScript-библиотеки для реактивных потоков. Внутри: разбор системы вычислимых типов для проверки контрактов в compile-time, управление маршрутизацией данных в графе и примеры построения динамических пайплайнов для IoT-датчиков и панелей управления.
Императивные эффекты (direct-style effects), также известные как «алгебраические эффекты» и «обработчики эффектов», — это следующий шаг в развитии языков программирования. Сначала мы обсудим проблему и связанные с нею ограничения. Затем рассмотрим простую реализацию на Scala 3 и опишем языковую особенность, которая её обеспечивает — контекстные функции. Далее мы увидим некоторые недостатки этой реализации и посмотрим, как их можно решить с помощью двух языковых особенностей: одной хорошо известной (ограниченные продолжения) и одной, находящейся в разработке (нововведения в системе типов).

В мире разработки программного обеспечения редко можно увидеть, как зрелый, динамический язык добавляет мощную, статическую систему типов без ущерба для своей философии и существующего кода. 3 июня 2026 года команда Elixir сделала именно это, выпустив версию 1.20. Главное нововведение — постепенная типизация (gradual typing), которая обещает найти в вашем коде «верифицированные баги» (verified bugs — ошибки, гарантированно ведущие к падению в рантайме) без необходимости писать аннотации типов.
Но почему это должно волновать вас, если вы пишете на Python, Java или Go? Команда Elixir поставила перед собой цель, которую многие считают «святым граалем». На практике сочетание всех трёх свойств почти не встречается.
И я считаю, что это отличный повод присмотреться к Elixir, даже если вы никогда не писали на нём ни строчки. Зрелый и интересный язык, работающий на виртуальной машине Erlang (BEAM) и исповедующий функциональную парадигму. Он известен своей отказоустойчивостью и конкурентностью, но, увы, остается малоизвестным языком, и я надеюсь что эта статья заставит вас заинтересоваться Elixir.

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

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

Добрый день,Хаброжители! Сегодня мы подготовили для вас перевод статьи.
В статье рассматривается переход от взаимодействия человек-агент к полностью автономным системам. Авторы подчеркивают, что такие агенты представляют собой сложные распределенные системы, требующие надежного и отказоустойчивого дизайна.
Вдохновляясь принципами языка 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 сервиса авторизации, который (помимо прочего) должен регистрировать новых пользователей.
Для начала определим структуру данных для создания нового пользователя.