DEV Community: Amedov Bekmukhamed

О теории типов

Amedov Bekmukhamed — Sat, 05 Sep 2026 04:52:58 +0000

Известный "кризис оснований математики", который произошел в начале XX века. Возник он из-за (или благодаря, тут трудно сказать) "Наивной теории множеств" Георга Кантора, которая на первый взгляд должна была стать точкой сбора всех математиков. Все мы, особенно разработчики, интуитивно понимаем теорию множеств. Например, вот множество натуральных чисел {1,2,3...}, а вот множество целых чисел {..., -1, 0, 1...}. Можно заметить, что множество целых чисел включает в себя множество натуральных чисел. Так что разность этих множеств (Z \ N) будет множество всех отрицательных целых чисел и нуля: {..., -1, 0}. Теория множеств является основой для реляционной алгебры, а значит он будет знаком каждому, кто работал с SQL. Но в наивной теории множеств были серьезные белые пятна, которые приводили к нарастающим год за год парадоксам. Самые известные - парадоксы Рассела, и одна из них сформулирована в виде парадокса брадобрея:
Пусть в некой деревне живёт брадобрей, который бреет всех жителей деревни, которые не бреются сами, и только их. Бреет ли брадобрей сам себя?
Bertrand Russel
Вместо множеств, которые могли включать в себя любые объекты, в том числе и себя, английский философ и логик Бертран Рассел предложил делить их по типам. Типы находились на разных уровнях и тип большего порядка включал в себя только типы меньшего порядка, поэтому это решило парадоксы. Но как я уже писал в предыдущем посте, работы Рассела оказались слишком непрактичными и не получили поддержки математического сообщества.

В 30-х годах XX века американский математик Алонзо Черч (учитель Алана Тьюринга) придумал очень мощную формальную систему под названием "Лямбда-исчисление" (Lambda calculus). Что такое "лямбда-исчисление" мы будем исследовать отдельно, потому что тема невероятно интересная и обширная. Но для понимания, та система, которую придумал Черч была бестиповой. Это сново привело к различным парадоксам в духе парадоксов Рассела (парадокс Клини-Россера). Чтобы спасти свое детище, Черч тоже обратился к типам и придумал "Просто типизированное лямбда-исчисление" (STLC). Почему "Просто типизированное"? Ну, чтобы никто не испугался из-за ассоциаций с теорией типов Рассела. Именно связка типов с лямбда-исчислением поспособствовала к дальнейшему развитию теории типов.
Название "Теория типов" очень обманчивое, потому что оно подразумевает, что это одна общая теория. На самом деле нет единой теории типов, есть множество теорий и два я уже упомянул (разветвленная теория типов Рассела и просто типизированное лямбда-исчисление Черча). Также может показаться, что теория типов изучает типы. Но, к удивлению, не существует общего определения понятия "тип". Долгое время математики понимали его интуитивно, как мы программисты, когда говорим, что тип - это "множество значений и операций над этими значениями". По предыдущим историям можно проследить, что математики изначально вводили типы как защиту от логических ошибок в формальных системах. Но дальнейшее изучение типов дало понять, что логика и типы имеют более глубокую связь.

В тех же 30-х годах американец Хаскелл Карри (в честь которого назван язык программирования Haskell и термин "каррирование") обнаружил удивительное сходство между логикой и типизированной комбинаторной логикой, о чем он решил рассказать только через 20 лет спустя. Тогда мало кто обратил внимание на это совпадение, пока другой американский математик Уильям Ховард не доказал изоморфизм между упомянутым "Просто типизированным лямбда исчислением"(STLC) и интуиционистский логикой. Изоморфизм означает, что структурные элементы этих систем равнозначны:

Это означает, что любая типизированная вычислительная система эквивалентна логической системе и они работают одинаково. Тут внесу ясность, что логическая система используется для доказательств. Отсюда делаем вывод, что любое вычисление в типизированной системе то же самое, что и доказательство какой-либо теоремы. Ну и подставьте сюда вместо страшного слова "Типизированная вычислительная система" какой-нибудь язык программирования - смысл от этого не поменяется.
То что я описал выше известно как Соответствие Карри-Ховарда. И выводы из него повлияли и на математику (появились новые теории типов, т.к. теория типов Мартина-Лефа), и на программирование. Программисты поняли, что типы - это не просто способ разделять данные, но и способ целиком описать систему в терминах логики. По другому - создать спецификацию программы. Данная программа не будет содержать логических ошибок и противоречий, если она скомпилировалась. На этом принципе построены все современные системы автоматического доказательства, такие как Rocq, Agda и Lean.

Чтобы это все работало в языке программирования, нам нужно иметь язык с мощной системой типов. А, к сожалению, таких ЯП среди мейнстрима исторически было мало. Дело в том, что типы в языках программирования появились естественным образом. Вспомните, сперва были типы на аппаратном уровне (integers and floating-point numbers), потом появились простые системы типов как в языке Fortran или С. Все, что мы обсуждали развивалось за стенами университетов, а затем перекочевало в академические языки типа Haskell. Но в последнее десятилетие происходит явный тренд на идеи из Теории типов в мейнстриме. Начали появляться популярные языки с интересной системой типов как TypeScript, Kotlin и Rust (который основан на линейной и аффинной логике Жан-Ив Жирара). Но интереснее поговорить про то, что классические языки как Java, Python, C# тоже начали адаптировать идеи как из функционального программирования, так и из теории типов. Рассмотрим этот феномен в контексте Java, в современных версиях языка мы уже видим реализации этих концепций.
Вывод типов. Это когда нам компилятор разрешает не указывать тип каждого объекта, а использовать var. Но в Java реализован только локальный вывод типов. Самым продвинутым способом вывода типов является алгоритм Хиндли-Милнера и его мы можем видеть, например, в OCaml.
Алгебраические типы данных (ADT). Реализуется через структуры Record и sealed interface. Позволяет нам выполнять алгебру типов (как я уже говорил, как в логике), создавая более сложные типы.
Сопоставление с шаблоном (Pattern matching). Напрямую связан с ADT, так как позволяет выразить все состояния типа. Это помогает нам обработать все возможные сценарии через оператор switch. Данный принцип можно описать как "Make illegal states unrepresentable".
Очевидно, что Java заимствует все последние фичи от своих собратьев по JVM, таких как Scala и Kotlin, потому что их делали дядьки с более сильной академической базой. Но мне как человеку, которому интересна теория типов, неважно откуда они взялись в моем языке программирования, главное что мне это дает. А дает то, что обсуждали выше - систему, которую я могу описать через выразительную систему типов. Практически, язык с мощными типами позволит писать бизнес-логику через них, а также проверить ее корректность на этапе компиляции.

P.S. Теория типов зашагала далеко вперед практики, поэтому многие вещи нам еще предстоит увидеть в своих языках программирования. Одна из таких интересных идей - зависимые типы.
Они позволяют связывать типы со значениями. Например, сделать тип «массив фиксированной длины» или «число строго больше нуля», причем проверку компилятор выполнит статически. Немного такой магии уже можно видеть в TypeScript.

Большой миф разработки

Amedov Bekmukhamed — Thu, 02 Oct 2025 06:11:38 +0000

TL;DR

Введение

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

Сегодня мы будем обсуждать REST и самое мистическое понятие в разработке - RESTful API. Многие не поймут в чем подвох и вроде бы все понимают, что это значит. Но! Как часто вы задумывались, что вообще значит REST? Как вы измеряете насколько ваши API являются RESTful? Почему по этой теме столько противоречивой информации и почему у каждого серьезного разработчика свое представление по правильному дизайну реста? Почему по нему нет никакой стандартизации, спецификации или документации?

Надеюсь, поразмыслив над этими вопросами у вас появится хоть тенечек сомнения по этой теме. Также как они появились и у меня полтора года назад, когда я читал документацию популярного Django REST Framework. Несмотря на кричащее название, документ использует слово REST очень осторожно и предпочитает заменять его на Web API или просто API. А еще откровенно пишет, что название подобрали чисто из-за маркетинговых целей.

First off, the disclaimer. The name "Django REST framework" was decided back in early 2011 and was chosen simply to ensure the project would be easily found by developers. Throughout the documentation we try to use the more simple and technically correct terminology of "Web APIs".
В целом кажется именно маркетинг является главной причиной почему понятие RESTful API возникло и существует по сей день.

Мотивация

Не так давно у Кирилла Мокевнина в его канале "Организованное программирование" вышел эпизод посвященный проектированию API. Я советую всем посмотреть полный эпизод, потому что там разбирают много недооцененных подходов и инструментов для современной разработки. Но где-то в середине начали обсуждаться вещи о которых я слышал очень отдаленно. Речь зашла про диссертацию некоего Роя Филдинга, концепцию HATEOAS и о книге Сергея Константинова - "API", который я тоже советую всем прочитать (или хотя бы эту статью от автора). После прослушивания я сразу же начал гуглить и разбирать эти темы, и поверьте - все что меня волновало долгие годы вдруг встало на свое место. У меня будто открылся третий глаз на лбу и с того момента любые дискуссии насчет REST перестали иметь для меня смысл. Здесь я попытаюсь ассемблировать все что было нарыто мной по этой теме, чтобы вы тоже могли взглянуть на это с совершенно другого угла.

Было

Словом REST нас в первый раз знакомит Рой Филдинг в своем phd "Architectural Styles and the Design of Network-based Software Architectures" начала этого тысячелетия. Вся диссертация посвящена теме, как строить системы в условиях только набирающего обороты веба. Рой примечателен тем, что стоит за спецификацией протокола HTTP и когда-то самого популярного веб-сервера Апачи. Так что же пишет отец REST-а:

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

Конечно, неподготовленный мало что поймет из такого определения. Но тут есть важная деталь, REST - это не про построение API. Это самый большой миф, в который верят разработчики. На протяжении всей диссертации Филдинга ни слово говорится о мифическом REST API. В его работе, REST - это классное решение для построения систем взаимодействующих по сети (сам он это разделяет от понятия "распределенные системы"). Прилагательное RESTful уместно было бы употреблять к приложениям или сервисам, но его начали массово применять к API. Тут большую роль, как по мне, сыграл маркетинг и хайп вокруг понятия REST, но про это поговорим чуть позже.

В оригинальном тексте автор знакомит нас с зоопарком архитектурных стилей. И в итоге рождает новый стиль, который именует REpresentation State Transfer и складывается он из следующих принципов:

Client-Server. Здесь все понятно.
Layered System. Здесь я тоже не хочу надолго задерживаться. Автор говорит, что системы REST могут быть многослойными. В нашу эпоху 99.99% продакшн систем являются таковыми.
COD (Code on Demand). Автор допускает, что клиент может запросить исполняемые коды с сервера. Если вы занимались фронтендом и загружали тонну джаваскрипта на ваш сайт, то знайте, что не отходите от принципов REST. Кстати, этот пункт является немного спорным, потому что если подумать, то кажется он противоречит следующему принципу.
Stateless. Прямое продолжение первого принципа. Если мы разделяем сущности клиент-сервер, то мы должны сделать все так, чтобы серверу было без разницы с какого клиента к нему обращаются и то же самое наоборот. Единственное, клиент должен предоставить в запросе все необходимое (то что в работе называется REpresentation) для успешной обработки сервером. Разные виды авторизаций (session cookies, authorization token) не нарушают принципы REST, так как клиент сам предоставляет состояние клиента в запросе[1]. Так чем же этот пункт входит в противоречие с предыдущим? А тем, что если сервер не хранит состояние клиента, то как он может отдавать код на исполнение, который написан на конкретном языке и который клиент должен понимать? А что вы думаете по этому поводу?
Cache. Данный принцип говорит о том, что клиент может закэшировать данные у себя и делать это он должен явно. В эпоху когда автор писал диссертацию, сетевые обращения были дороже, поэтому данный пункт был принципиальным для производительности систем. Про серверные кэши Рой тоже говорит, но меньше. В нынешнее время кэши используются повсеместно на всех уровнях: на клиентских приложениях, кэширующих прокси и на самих application серверах. Изменилось одно, сейчас увидеть чтобы клиент явно указывал кэшируемые ресурсы - редкость.
Uniform Interface. Принцип говорит о том, что клиент всегда должен знать как взаимодействовать с сервером через единообразный интерфейс. Это главный пункт, который отличает REST от других архитектур по Филдингу и который вообще дал повод существованию понятия REST API. Uniform Interface складывается из четырех других принципов: идентификация ресурсов, изменение ресурсов через представления, самоописываемые сообщения и использование гипермедиа, как движка состояния приложения. Коллективный разум разработчиков решил, что те API, которые формально соответствуют этим четырем принципам могут называться RESTful. Далее известные компании начали публиковать свои открытые API в интернете и (ИМХО) в маркетинговых целях стали называть их REST/RESTful. И все было прекрасно, а этой статьи просто бы не существовало в природе. Но заметили ли вы один непримечательный принцип, когда я перечислял требования к интерфейсу рестовых систем? Если нет, то я говорю про принцип hypermedia as the engine of application state или просто - HATEOAS.

Вероятно некоторые из вас подумали, что это очередной абстрактный и клишированный принцип, название которого знать не обязательно. Но именно оно стало яблоком раздора между автором и сообществом, а также сделало понятие RESTful API очень и ОЧЕНЬ спорным.

Стало

Жили разработчики, не тужили, создавали ресты и радовались жизни. Слово REST уже тогда потерял исконный смысл, ну и хрен бы с ним. Но в 2008 году Рой снова пишет про REST. Статью он начинает без прелюдий:

I am getting frustrated by the number of people calling any HTTP-based interface a REST API. Today’s example is the SocialSite REST API. That is RPC. It screams RPC. There is so much coupling on display that it should be given an X rating.

Далее он пишет свою главную мысль:

What needs to be done to make the REST architectural style clear on the notion that hypertext is a constraint? In other words, if the engine of application state (and hence the API) is not being driven by hypertext, then it cannot be RESTful and cannot be a REST API. Period. Is there some broken manual somewhere that needs to be fixed?

В общем. Рой Филдинг, который долго терпел как айти сообщество все эти годы издевалось над его термином, решил дать ответку довольно в жесткой форме. В своем обращении он заявляет, что без принципа HATEOAS никакой REST не REST. И делайте с этим, что хотите. Только перестаньте называть это REST API.

Внимательно ознакомившись с этим принципом я пришел к немного шизанутому выводу, что единственной системой успешной реализующей REST API по Филдингу - это... сама Всемирная паутина. Я не зря упомянул про бэкграунд Роя, ведь он стоял у истоков веба и надеюсь теперь у вас тоже все встало на свои места - диссертация была про сам WWW.

Принцип HATEOAS говорит о том, что клиент получив доступ к серверу через одну точку входа, должен далее выстроить все взаимодействие с API с помощью гипермедиа. Клиент абсолютно ничего не должен знать про сервер и должен двигаться по API Божьей помощью, ой, то есть через текущее состояние в которой клиент оказался (Application State) и через связанные с этим состоянием ссылками (hyperlinks). Если клиент не понимает как дальше работать с API, то он может запросить код для дальнейшего действия, подчиняясь принципу COD. Это удивительно похоже на то как вы пользуетесь браузером. Вы серфите по интернету и выходите на одни сайты через другие. Отсюда вывод, что у рестового API должен быть не менее рестовый клиент, работа которого будет схожа на работу веб-браузера. Есть имплементации таких клиентов, допустим Ketting. Часто для взаимодействия клиент-сервера используется формат HAL.

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

{
  "_links": {
    "author-collection": { "href": "/authors", "title": "List of authors" },
    "article-collection": { "href": "/articles", "title": "List of articles" },
    "help": { "href": "mailto:support@api.example" }
  },
  "motd": "Welcome to the blogging server!"
}

Провалившись в список статьей получаем:

{
  "_links": {
    "item": [
      { "href": "/articles/1" },
      { "href": "/articles/2" },
      { "href": "/articles/3" }
    ],
    "next": { "href": "/articles?page=2" }
  },
  "total": 25
}

А здесь как выглядел бы клиент такого API.

const client = new Client('https://api.example/');
const home = client.go();
const articleCollection = await home.follow('article-collection');
const articleResources = await articleCollection.followAll('item');

for(const resource of articleResources) {
  const state = await resource.get();
  console.log(state.data);
}

Если хотите спроектировать трушный REST API, то первым делом я бы советовал удалить весь Swagger, если он имеется. Потому что настоящий рест по Филдингу не хранит фиксированный интерфейс и создание документации для таких API просто бессмысленное занятие. Но я почему то сильно сомневаюсь, что кто-то из читающих будет разрабатывать подобные API.

Итого

Лично для себя я решил вывести из своего вокабуляра словосочетание REST API и заменять его на HTTP API, Web API или просто API. Причина проста, для уменьшения путаницы и в качестве символического уважения к автору. Так допустим делают Сергей Константинов, разработчики DRF и некоторые разработчики Яндекса. Понятное дело таких людей немного, потому что мало кто действительно углублялось в историю этого термина.

Но я ни в ком случае не собираюсь осуждать людей, которые продолжают использовать это слово (даже зная контекст). Тот же Кирилл Мокевнин в эпизоде которого я про все эти вещи впервые услышал, не перестает употреблять его в своих материалах. На самом деле в айти хватает других мифов и базвордов, которые тоже возникли из-за их некорректного применения, те же Agile, ACID и т.д. и т.п. С исторической точки зрения, хоть понятие RESTful API слишком абстрактное и часто покрыто откровенной отсебятиной, но оно действительно помогло создать хорошие практики для многого поколения разработчиков. Правильная утилизация статус кодов и HTTP-методов, подбор хорошего нейминга для путей в URI, выбор JSON в качестве формата данных, все это имеет ничего общего с понятием REST, но это очень хорошие и правильные советы для разработки API. А как вы упакуете и назовете его, это уже дело десятое.

Links:
https://www.baeldung.com/cs/rest-sessions
https://www.django-rest-framework.org/topics/rest-hypermedia-hateoas/
https://www.youtube.com/watch?v=W9sYAdiLnt8&t=3675s
https://twirl.github.io/The-API-Book/API.en.html
https://twirl.medium.com/the-mythology-of-rest-695eb00ba8c0
https://ics.uci.edu/~fielding/pubs/dissertation/fielding_dissertation.pdf
https://roy.gbiv.com/untangled/2008/rest-apis-must-be-hypertext-driven