Теория языков программирования

Линейные и аффинные типы

Use-after-free, double-free, data races - три класса багов, уничтожившие репутацию C и C++. Mozilla подсчитала: 70% CVE в браузерах Chrome и Firefox - это memory safety баги. Rust решил их не через GC, не через runtime checks, а через систему типов. В основе - линейная логика 1987 года. Теория наконец встретила индустрию.

**Rust в Linux kernel (2022):** первый язык после C, принятый в ядро. Borrow checker - главная причина выбора.
**Android (Google):** новый код на Rust. Memory safety баги упали с 76% до 24% среди security уязвимостей за 3 года.
**Haskell LinearTypes (GHC 9.0+):** безопасная работа с файлами, сетью, CUDA без утечек ресурсов

Линейная логика Жирара

В классической логике если у нас есть доказательство P, его можно использовать сколько угодно раз: и дублировать, и выбрасывать. **Линейная логика**, предложенная Жан-Ивом Жираром в 1987 году, убирает это допущение: каждый ресурс должен быть использован *ровно один раз*.

Линейная логика моделирует **ресурсы**: деньги, файловые дескрипторы, токены доступа, память. В отличие от классической логики, здесь «использовать» значит «потребить». Это даёт фундамент для систем типов, отслеживающих жизненный цикл ресурсов.

**Аффинные типы** - ослабление линейных: ресурс можно использовать *не более одного* раза (то есть можно и выбросить, но нельзя дублировать). Rust использует именно аффинные типы через систему владения.

В линейной логике что означает оператор ⊸ (линейная импликация, A ⊸ B)?

Управление ресурсами через типы

Файловый дескриптор - классический пример ресурса с lifecycle: открыть, использовать, закрыть ровно один раз. Забыть закрыть - утечка. Закрыть дважды - undefined behavior. Линейные типы кодируют этот protocol в системе типов: компилятор отслеживает использование.

Ключевое: компилятор статически гарантирует, что каждый `Handle` будет закрыт *ровно раз* - без runtime-проверок, без GC finalizers, без надежды на дисциплину разработчика. Это **protocol compliance через типы**.

Что произойдёт в системе с линейными типами, если файловый handle не закрыт перед выходом из функции?

Borrow Checker Rust как линейные типы

Rust не называет свою систему «линейными типами», но её семантика - прямое воплощение аффинных типов. Каждое значение имеет ровно одного **владельца** (owner). Когда владелец выходит из scope, значение уничтожается. Передача значения = **move**: оригинал больше недоступен.

Правило «либо N shared, либо 1 exclusive» - это ограничение **aliasing**: не может быть двух mutable ссылок на одно значение. Именно aliasing является причиной большинства data races и use-after-free багов. Borrow checker исключает их статически.

**Lifetimes в Rust** - ещё один слой: компилятор отслеживает, что ссылка не переживает объект, на который ссылается. `'a` в `&'a str` - это аннотация времени жизни, позволяющая компилятору доказать отсутствие dangling references.

Почему Rust разрешает множество `&T` одновременно, но только один `&mut T`?

Uniqueness Types в Clean и Idris

**Uniqueness types** - двойник линейных типов, разработанный для функциональных языков. Идея: тип помечается как *уникальный*, если гарантировано, что на него нет других ссылок в данный момент. Уникальный объект можно безопасно мутировать - как в imperative языках, но со статической гарантией.

Uniqueness types и линейные типы решают одну задачу с разных сторон. Линейные: «значение должно быть использовано ровно раз» (взгляд со стороны потребителя). Uniqueness: «на это значение нет других ссылок» (взгляд со стороны владельца). В Clean uniqueness позволяет делать destructive update массивов с O(1) вместо O(n) - без нарушения чистоты.

**Linearity в Haskell GHC 9.0+:** расширение `LinearTypes` добавляет `%1 ->` синтаксис. Это не полноценные линейные типы, но позволяет писать протоколы safe resource handling в обычном Haskell коде.

Линейные типы и uniqueness types - это одно и то же, просто разные названия

Они двойственны (dual), но не идентичны. Линейные типы ограничивают потребителя: «используй ровно раз». Uniqueness типы ограничивают поставщика: «нет других ссылок». В теории Girard эти системы связаны через логическую двойственность, но на практике дают разные паттерны программирования.

В Clean uniqueness дают O(1) мутацию в функциональном языке. В линейных типах акцент - на lifecycle ресурсов. Rust сочетает оба: ownership (uniqueness) + borrows (временное ослабление уникальности).

Почему uniqueness types позволяют делать destructive update массива в чисто функциональном языке (Clean)?