Спецификация системы типов

Этот документ определяет спецификацию системы типов языка программирования YaoXiang, включая базовые типы, составные типы, дженерики и trait.

Глава 0: Теоретические основы

0.1 Соответствие Карри-Ховарда

Соответствие Карри-Ховарда (Curry-Howard correspondence) является теоретической основой системы типов YaoXiang. Оно раскрывает глубокую связь между системой типов языка программирования и математической логикой:

Логика	Язык программирования
Пропозиция (P)	Тип `Type`
Доказательство (p: P)	Программа `x: T = ...`
Импликация (P \rightarrow Q)	Функциональный тип `(P) -> Q`
Конъюнкция (P \wedge Q)	Тип произведения `{ a: P, b: Q }`
Дизъюнкция (P \vee Q)	Тип суммы `{ a(P) \| b(Q) }`
Универсальная квантификация (\forall x:T. P(x))	Дженерики `(T: Type) -> ...`
Истина (\top)	`Void` (Unit, имеет значение по умолчанию)
Ложь (\bot)	`Never` (нулевой конструктор, не имеет обитателей)
Вселенная типов (Type_n : Type_{n+1})	Стратификация вселенных (защита от парадокса Рассела)
case-анализ	`match` на уровне типов

Примечание: match на уровне типов — это case-анализ, а не математическая индукция. Для индукции требуется рекурсивная функция на уровне типов + проверка завершимости компилятором.

0.2 Тип как пропозиция, программа как доказательство

В YaoXiang это соответствие является основополагающим принципом проектирования:

Завершающиеся вычисления на уровне типов соответствуют корректным конструктивным доказательствам. Семейства типов YaoXiang (такие как Add с case-анализом + рекурсивным вызовом на Nat) по сути являются типизированным кодированием математической индукции — при условии, что компилятор способен выполнить проверку завершимости.
Проверка типов — это проверка доказательства. Когда программа проходит проверку типов, это эквивалентно конструктивному доказательству логической пропозиции.

0.3 Влияние на проектирование языка

Конкретные проявления соответствия Карри-Ховарда в YaoXiang:

Стратификация вселенных (RFC-010): Type₀ : Type₁ : Type₂ … предотвращает логический парадокс (парадокс Жирара), возникающий при Type: Type.
Семейства типов (RFC-011): case-анализ + рекурсивный вызов на уровне типов для натурального числа Nat(Zero/Succ) соответствуют аксиомам Пеано — при условии, что компилятор выполняет проверку завершимости.
Условные типы (RFC-011): If: (C: Bool, T: Type, E: Type) -> Type соответствует case-дизъюнкции в логике.
Типы с зависимостью от значений (RFC-011): Array: (T: Type, N: Int) -> Type соответствует конечной квантификации «для каждого целого N существует тип».

Глава 1: Классификация типов

1.1 Выражения типов

TypeExpr    ::= PrimitiveType
              | RecordType
              | InterfaceType
              | TupleType
              | FnType
              | GenericType
              | TypeRef
              | TypeUnion
              | TypeIntersection

Пояснение к проектированию: хотя RFC-010 предлагает унифицированную модель «всё есть присваивание» (name: type = value), на синтаксическом уровне типы и значения всё же необходимо различать. В реализации компилятора Type и Expr — это два независимых перечисления AST (ast.rs:406 и ast.rs:25); TypeExpr служит BNF-заполнителем, соответствующим перечислению Type в реализации и означающим «в этой позиции ожидается тип».

Глава 2: Базовые типы

2.1 Примитивные типы

Тип	Логический аналог	Описание	Размер по умолчанию
`Type`	—	Метатип	0 байт
`Never`	⊥ (ложь/пустой тип)	Нулевой конструктор, без значений. Тип возврата при расходимости/panic. `Never <: T` выполняется для любого T.	0 байт
`Void`	⊤ (истина/Unit)	Имеет значение void по умолчанию, тип произведения с нулём полей. Допустимо `x: Void = <по умолчанию>`.	0 байт
`Bool`	—	Логическое значение: `true` / `false`	1 байт
`Int`	—	Целое со знаком	8 байт
`Uint`	—	Целое без знака	8 байт
`Float`	—	Число с плавающей точкой	8 байт
`String`	—	UTF-8 строка	Переменный
`Char`	—	Unicode-символ	4 байта
`Bytes`	—	Сырые байты	Переменный

Целые с заданной разрядностью: Int8, Int16, Int32, Int64, Int128. Числа с плавающей точкой с заданной разрядностью: Float32, Float64.

2.2 Never и Void: ⊥ и ⊤

Never и Void — логические примитивы системы типов, соответствующие лжи (⊥) и истине (⊤) соответственно.

Never (⊥, ложь/пустой тип) — три непреложных свойства:

Нулевой конструктор: ни один литерал или выражение не может породить значение типа Never. Для x: Never = ... нет правой части.
Принцип взрыва: Never <: T выполняется для любого типа T. assert(false) возвращает Never, после чего код может пройти проверку типов (хотя никогда не будет выполнен).
Маркер расходимости: f: (...) -> Never означает, что f гарантированно не вернётся. Компилятор использует это для анализа мёртвого кода и слияния ветвей match.

Never — встроенное имя типа (регистрируется тем же путём, что и Int/Bool), а не ключевое слово.

Void (⊤, истина/Unit) — ровно один обитатель (значение void по умолчанию). Void — единичный элемент для типа произведения с нулём полей. Допустимо x: Void = <по умолчанию>. Значение блока определяется хвостовым выражением (пустой блок {} имеет значение Void), подробности см. в RFC-010a.

Глава 3: Составные типы

3.1 Тип записи

Единый синтаксис: Name: Type = { field1: Type1, field2: Type2, ... }

RecordType  ::= '{' FieldList? '}'
FieldList   ::= Field (',' Field)* ','?
Field       ::= Identifier ':' TypeExpr
            |  Identifier                 // ограничение интерфейса

yaoxiang

// Простой тип записи
Point: Type = { x: Float, y: Float }

// Пустой тип записи
Empty: Type = {}

// Тип записи с дженериком
Pair: (T: Type) -> Type = { first: T, second: T }

// Тип записи, реализующий интерфейсы
Point: Type = {
    x: Float,
    y: Float,
    Drawable,
    Serializable
}

Правила:

Тип записи определяется с помощью фигурных скобок {}.
После имени поля сразу идут двоеточие и тип.
Имя интерфейса в теле типа означает его реализацию.

Принадлежность пространству имён: префикс Type.name (например, Point.draw) означает, что функция принадлежит пространству имён Point. Это не вызывает неявных привязок. Чтобы синтаксис вызова через . (например, p.draw()) работал, требуется явная привязка: Point.draw = draw[0]. Подробности см. в RFC-004 и RFC-010.

3.1.1 Значения полей по умолчанию

Поля типа могут иметь значения по умолчанию — при конструировании их можно не указывать:

yaoxiang

// Поля со значениями по умолчанию — необязательны при конструировании
Point: Type = {
    x: Float = 0,
    y: Float = 0
}

// Использование
Point()           // -> Point(x=0, y=0)
Point(x=1)       // -> Point(x=1, y=0)
Point(x=1, y=2) // -> Point(x=1, y=2)

// Поля без значений по умолчанию — обязательны при конструировании
Point2: Type = {
    x: Float,
    y: Float
}

// Использование
Point2(x=1, y=2) // корректно
Point2()          // ошибка

Правила:

field: Type = expression → значение по умолчанию задано, при конструировании необязательно.
field: Type → значения по умолчанию нет, при конструировании обязательно.

3.1.2 Встроенные привязки

В теле определения типа можно напрямую привязывать методы:

yaoxiang

// Способ 1: ссылка на внешнюю функцию
distance: (a: Point, b: Point) -> Float = { ... }
Point: Type = {
    x: Float = 0,
    y: Float = 0,
    distance = distance[0]    // привязка к позиции 0
}
// Вызов: p1.distance(p2) -> distance(p1, p2)

// Способ 2: анонимная функция + позиционная привязка
Point: Type = {
    x: Float = 0,
    y: Float = 0,
    distance: ((a: Point, b: Point) -> Float)[0] = ((a, b) => {
        dx = a.x - b.x
        dy = a.y - b.y
        return (dx * dx + dy * dy).sqrt()
    })
}
// Синтаксис: ((params) => body)[position]
// Вызов: p1.distance(p2) -> distance(p1, p2)

3.2 Тип интерфейса

InterfaceType ::= '{' FnField (',' FnField)* ','?
FnField       ::= Identifier ':' FnType
FnType        ::= '(' ParamTypes? ')' '->' TypeExpr

Синтаксис: интерфейс — это тип записи, все поля которого являются функциональными типами.

yaoxiang

// Определение интерфейса
Drawable: Type = {
    draw: (Surface) -> Void,
    bounding_box: () -> Rect
}

Serializable: Type = {
    serialize: () -> String
}

// Пустой интерфейс
EmptyInterface: Type = {}

Реализация интерфейса: тип реализует интерфейсы, перечисляя их имена в конце определения.

yaoxiang

// Тип, реализующий интерфейсы
Point: Type = {
    x: Float,
    y: Float,
    Drawable,        // реализация интерфейса Drawable
    Serializable     // реализация интерфейса Serializable
}

Прямое присваивание интерфейсу: конкретный тип можно напрямую присвоить переменной интерфейсного типа (структурная подтипизация).

yaoxiang

// Прямое присваивание (конкретный тип известен на этапе компиляции -> вызов без накладных расходов)
d: Drawable = Circle(1)
d.draw(screen)        // после компиляции: прямой вызов circle_draw, без vtable

// Возвращаемое значение из функции (конкретный тип неизвестен на этапе компиляции -> вызов через vtable)
d: Drawable = get_shape()
d.draw(screen)        // поиск метода через vtable

// Интерфейс как параметр функции
process: (d: Drawable) -> Void = d.draw(screen)

Стратегия оптимизации на этапе компиляции:

Сценарий	Результат вывода	Способ вызова
Прямое присваивание конкретного типа	Конкретный тип определим	Прямой вызов (без накладных расходов)
Возвращаемое значение из функции	Неизвестно	vtable
Гетерогенная коллекция	Несколько типов	vtable

Когерентность и сиротские правила (неприменимо, итоговое пояснение): интерфейсы в YaoXiang — структурные типы (интерфейс = запись, все поля которой — функциональные типы), а не номинальные trait. Здесь нет проблемы «кто и для кого реализует» между крейтами/модулями, поэтому когерентность и сиротские правила в стиле Rust не имеют объекта применения (см. протокол решения в RFC-011 §2.1). Соответствующей гарантией в структурном мире является отказ от дублирующих реализаций: повторное определение метода с той же сигнатурой в типе приводит к ошибке компиляции (RFC-011a §3, запрет переопределения; перегрузка допустима).

3.4 Кортежный тип

TupleType   ::= '(' TypeList? ')'
TypeList    ::= TypeExpr (',' TypeExpr)* ','?

3.5 Функциональный тип

FnType      ::= '(' ParamList? ')' '->' TypeExpr
ParamList   ::= TypeExpr (',' TypeExpr)*

Глава 4: Дженерики

4.1 Синтаксис параметров дженериков

Параметры дженериков являются частью функционального типа и используют единый синтаксис ():

GenericType     ::= Identifier '(' TypeArgList ')'
TypeArgList     ::= TypeExpr (',' TypeExpr)* ','?
TypeBound       ::= Identifier
                 |  Identifier '+' Identifier ('+' Identifier)*

В определении дженерик-типа (T: Type) — это сигнатура параметров конструктора типов, а -> Type обозначает возвращаемый тип:

yaoxiang

List: (T: Type) -> Type = { ... }
Map: (K: Type, V: Type) -> Type = { ... }

4.1.1 Типы-контейнеры

Типы-контейнеры — это конструкторы дженерик-типов, а не встроенные примитивы — они обрабатываются так же, как пользовательские дженерики, через единый путь инстанцирования. Принадлежность информации о длине — ключевое различие между тремя концепциями контейнеров:

Тип	Длина	Семантика	Базис
`Array(T, N)`	Тип	Массив фиксированной длины (const-дженерик N)	Базовый примитив (приоритет стека/инлайна)
`Vec(T)`	Значение времени выполнения	Сырой буфер с длиной, известной в рантайме, может расти	Базовый примитив (непрерывный буфер в куче)
`List(T)`	Значение времени выполнения	Стандартный тип библиотеки (растущий список)	Библиотека: `{ data: Vec(T), length: Int }`
`Dict(K, V)`	Значение времени выполнения	Отображение ключ-значение	`HeapValue::Dict`

List(T) — это тип стандартной библиотеки, а не примитив компилятора: он определён в самом YaoXiang в std.list и обрабатывается так же, как пользовательские дженерик-записи. Вся стратегия растущей семантики (когда расширяться, на сколько, возможно ли разделение) находится в библиотеке, компилятор в неё не вмешивается. Vec(T) — это минимальный фундаментальный примитив, от которого он зависит.
Set(T) удалён: нет литерала, нет представления в рантайме, нет std.set. При появлении потребности он будет добавлен по образцу Dict.

Ключевые правила:

Куда попадает литерал, определяется контекстом: голый литерал [...] и аннотация List(T) дают растущий список; аннотация Array(T, N), применённая непосредственно к литералу, даёт массив фиксированной длины. Проверка попадания: число элементов == N, тип элементов совместим с T; несоответствие — ошибка компиляции E1002; если N — символьная константа (const-параметр), проверка числа элементов откладывается до фазы уточнения типа.
Запрет неявного преобразования List→Array: фиксированность длины гарантируется на уровне типов — push принимает только receiver типа List(A).
Иерархия производительности: снизу вверх производительность убывает, гибкость растёт: Array > Vec > List.
Контракт ошибок индексации (ошибка времени выполнения — переходное состояние, целевое — покрытие на этапе компиляции через уточнение типов, см. §8.4):
- выход за границы (включая отрицательные индексы) → E6003
- отсутствующий ключ в Dict → E6008
Предикат принадлежности in: возвращает Bool и не сообщает об ошибке; правый операнд покрывает List/Array/Dict(ключ)/Tuple/String/Range. Это холловский предикат первого класса — основа для доказуемых на этапе компиляции утверждений через уточняющие типы.`

В дженерик-функциях параметры типов также объявляются в сигнатуре, компилятор автоматически выводит их из фактических аргументов:

yaoxiang

map: (T: Type, R: Type) -> ((list: List(T), f: (T) -> R) -> List(R)) = ...

4.2 Определение дженерик-типа

yaoxiang

// Базовый дженерик-тип
Option: (T: Type) -> Type = {
    some: (T) -> Option(T),
    none: () -> Option(T)
}

Result: (T: Type, E: Type) -> Type = {
    ok: (T) -> Result(T, E),
    err: (E) -> Result(T, E)
}

List: (T: Type) -> Type = {
    data: Array(T),
    length: Int,
    push: (self: List(T), item: T) -> Void,   // self — лишь соглашение об имени, не ключевое слово
    get: (self: List(T), index: Int) -> Option(T)
}

4.3 Вызов конструктора дженерика и вывод типов

Список полей определения дженерик-типа автоматически порождает конструктор: каждому полю соответствует параметр конструктора, имя поля — это имя параметра; поля со значениями по умолчанию могут быть опущены при конструировании, поля без значений по умолчанию обязательны. Поля функционального типа (методы) не порождают параметров конструктора.

yaoxiang

// Определение типа
Container: (T: Type) -> Type = {
    value: T,        // без значения по умолчанию → параметр конструктора обязателен
    extra: T,
}
// Автоматически развёрнутая полная форма (внутреннее представление компилятора; от пользователя не требуется):
// Container: (T: Type) -> (value: T, extra: T) -> Type = {
//     value: T = value,
//     extra: T = extra,
// }

// Вызов: вызов автоматически сгенерированного конструктора
c  = Container(42, 43)            // параметры конструктора по порядку полей; T автоматически распаковывается из элементов = Int
c2 = Container("a", "b")          // T = String
c3 = Container(Int)(42, 43)       // явный параметр типа + позиционные параметры конструктора
c4 = Container(Int)(extra=43, value=42)  // по именам полей, порядок произвольный
c5 = Container(Int)()             // пустой конструктор: поля получают значения по умолчанию/нулевые (данные присваиваются позже)

// Значения полей по умолчанию → параметры конструктора могут быть опущены
Point: (T: Type) -> Type = { x: T = 0, y: T = 0 }
p  = Point(1.5, 2.5)              // T = Float, x←1.5, y←2.5
p2 = Point(Int)()                 // x=0, y=0

Правила вызова (одни скобки, позиционное соответствие объявленным параметрам, слева направо):

Фактические аргументы по позиции пытаются соответствовать объявленным параметрам типа: позиция Type принимает фактические аргументы-типы, позиции параметров-значений времени компиляции (например, Int) принимают константы времени компиляции.
Если хотя бы одна позиция параметра-значения времени компиляции успешно сопоставлена (частичное соответствие), обработка идёт как конструирование типа: проверяются все позиции подряд; при ошибке первой сообщается первый несоответствующий/отсутствующий параметр в порядке объявления.
Если фактические аргументы полностью не соответствуют объявленным параметрам (всё — значения, ни одна позиция параметра-значения не сопоставима), обработка идёт как параметры конструктора: позиционное заполнение по порядку полей, параметры типа автоматически распаковываются из типов элементов.

yaoxiang

Matrix: (T: Type, Rows: Int, Cols: Int) -> Type = {
    _assert_rows: Assert(Rows > 0),
    data: Array(Array(T, Cols), Rows),
}

m: Matrix(Int, 3, 4)              // позиция типа: однослойное конструирование типа
m2 = Matrix(Int, 3, 4)(data=[[1,2,3,4],[5,6,7,8],[9,10,11,12]])  // двуслойное: тип + параметры конструктора
m3 = Matrix(Int, 3, 4)()          // пустой конструктор (модель RFC-011 §9.3, данные присваиваются позже)

Matrix(42)    // ❌ позиция 0: T←42 не соответствует (42 — не тип); позиция 1: Rows←42 соответствует;
              //    позиция 2: Cols отсутствует → сначала сообщается первая ошибка: ожидался Type, найдено 42
Container(42) // ❌ отсутствует параметр конструктора extra
Container(42, 43, 44)  // ❌ слишком много параметров конструктора

Вывод типов: параметры типа конструктора дженерик-типа автоматически распаковываются из типов элементов параметров конструктора (Container(42, 43) → T=Int); параметры типа дженерик-функции автоматически распаковываются из типов фактических аргументов (map(numbers, f) → T=Int, R=String, см. §4.1). Если распаковка невозможна, требуется явное указание.

Глава 5: Ограничения типов

5.1 Единичное ограничение

ConstrainedType ::= '(' Identifier ':' TypeBound ')' TypeExpr

yaoxiang

// Определение интерфейса (как ограничение)
Clone: Type = {
    clone: () -> Clone
}

// Использование ограничения
clone: (T: Clone)(value: T) -> T = value.clone()

5.2 Множественное ограничение

Источник разрешения ограничений (RFC-011b): разрешение имён ограничений операторов (Add / Subtract / Multiply / Divide / Modulo / Equal / Index) = обращение к реестру реализаций интерфейсов — T: Add ≜ в реестре зарегистрирована инстанциация Add(T, T, T); у Equal дополнительно работает структурный вывод (запись, все поля которой сравнимы, автоматически сравниваема). Имена Zero / One / PartialOrd пока не имеют источника определения и относятся к висящим именам ограничений.

yaoxiang

// Синтаксис множественных ограничений
combine: (T: Clone + Add)(a: T, b: T) -> T = {
    a.clone() + b
}

// Сортировка дженерик-контейнера
sort: (T: Clone + PartialOrd)(list: List(T)) -> List(T) = {
    result = list.clone()
    quicksort(&mut result)
    return result
}

5.3 Ограничения для функциональных типов

yaoxiang

// Ограничение на функцию высшего порядка
call_twice: (T: Type, F: () -> T)(f: F) -> (T, T) = (f(), f())

compose: (A: Type, B: Type, C: Type, F: (A) -> B, G: (B) -> C)(a: A, f: F, g: G) -> C = g(f(a))

Глава 6: Ассоциированные типы

6.1 Определение ассоциированного типа

AssociatedType ::= Identifier ':' TypeExpr

yaoxiang

// Iterator trait (используется синтаксис типа записи)
Iterator: (T: Type) -> Type = {
    Item: T,                    // ассоциированный тип
    next: () -> Option(T),
    has_next: () -> Bool
}

// Использование ассоциированного типа
collect: (T: Type, I: Iterator(T))(iter: I) -> List(T) = {
    result = List(T)()
    while iter.has_next() {
        if let Some(item) = iter.next() {
            result.push(item)
        }
    }
    return result
}

6.2 Дженерик-ассоциированные типы (GAT)

yaoxiang

// Более сложный ассоциированный тип
Container: (T: Type) -> Type = {
    Item: T,
    IteratorType: Iterator(T),  // ассоциированный тип тоже дженерик
    iter: () -> IteratorType
}

Глава 7: Дженерики времени компиляции

7.1 Параметры-значения времени компиляции

LiteralType   ::= Identifier ':' Int          // константа времени компиляции (кандидат)

Критерием служит использование в позиции типа, а не «аннотация конкретным типом»: в add: (a: Int, b: Int) -> Int = a + b параметры a/b — это параметры-значения времени выполнения (ни один из них не встречается в позиции типа).

Терминология: параметр дженерика, аннотированный конкретным типом, отличным от Type (например, Int), называется кандидатом в параметры-значения времени компиляции; становится ли он параметром-значением времени компиляции, определяется тем, используется ли его значение в позиции типа (зависимость от значений). Ключевое слово const не требуется (во внутренней реализации ранее использовался термин «const-дженерик», в документации унифицированно используется «параметр-значение времени компиляции»).

Правило определения (в два шага):

Грубая фильтрация по форме: параметр, аннотированный конкретным типом, отличным от Type (Int/Bool/Float) → кандидат.
Точная фильтрация по применению: имя кандидата встречается в позиции типа (тип поля в теле типа, тип параметра во вложенной Fn, предикат Assert, позиция фактического аргумента конструкции типа Array(T, N)) → истинный параметр-значение времени компиляции; иначе — параметр-значение времени выполнения.

Запись	Определение	Причина
`add: (a: Int, b: Int) -> Int = a + b`	a/b — параметры-значения времени выполнения	Только в позиции значения
`Array: (T: Type, N: Int) -> Type = { data: Array(T, N) }`	N — параметр-значение времени компиляции	N в позиции фактического аргумента конструкции типа
`factorial: (N: Int) -> (k: N) -> Int`	N — параметр-значение времени компиляции	N выступает как тип вложенного параметра k
`Foo: (T: Type, N: Int) -> Type = { x: T }`	N не сработал → параметр-значение времени выполнения	N не используется в теле типа

Ключевой замысел: параметр-значение времени компиляции (N: Int) + параметр-значение (k: N) различают константу времени компиляции и значение времени выполнения. Несработавший кандидат (форма подходит, но применение не сработало) деградирует до параметра-значения времени выполнения — и на уровне функции, и на уровне конструктора типа.

yaoxiang

// Параметр-значение времени компиляции: N используется в позиции типа (слот длины Array)
Measure: (T: Type, N: Int) -> Type = {
    data: Array(T, N),      // N в позиции фактического аргумента конструкции типа → параметр-значение времени компиляции
    length: N
}

// Использование: factorial(5) вычисляется в позиции типа (время компиляции), результат 120 встраивается в тип
arr: Measure(Int, factorial(5))  // компилятор вычисляет factorial(5) = 120 на этапе компиляции

// Зависимость от значения: N как тип внутреннего параметра k
// N — параметр-значение времени компиляции (используется в позиции типа (k: N));
// k — параметр-значение времени выполнения, его тип — литеральный тип N (однозначный тип).
factorial: (N: Int) -> (k: N) -> Int = {
    match k {
        0 => 1,
        _ => k * factorial(k - 1)
    }
}

7.2 Константные массивы времени компиляции

yaoxiang

// Использование матричного типа
Matrix: (T: Type, Rows: Int, Cols: Int) -> Type = {
    data: Array(Array(T, Cols), Rows)
}

// Проверка размерности на этапе компиляции
identity_matrix: (T: Add + Zero + One, N: Int)(size: N) -> Matrix(T, N, N) = {
    // ...
}

Глава 8: Условные типы

8.1 Условный тип If

IfType        ::= 'If' '(' BoolExpr ',' TypeExpr ',' TypeExpr ')'

yaoxiang

// If на уровне типов
If: (C: Bool, T: Type, E: Type) -> Type = match C {
    True => T,
    False => E
}

// Пример: ветвление времени компиляции
NonEmpty: (T: Type) -> Type = If(T != Void, T, Never)
// Мост IsTrue и уточняющий тип Assert (см. §8.3)
IsTrue: (b: Bool) -> Type = match b {
    true => Void,      // ⊤, программа продолжается
    false => Never,    // ⊥, расходимость/ошибка компиляции
}
Assert: (cond: Bool) -> Type = IsTrue(cond)

8.2 Семейства типов

yaoxiang

// Преобразование типа на этапе компиляции
AsString: (T: Type) -> Type = match T {
    Int => String,
    Float => String,
    Bool => String,
    _ => String
}

8.3 Уточняющий тип Assert и утверждение assert

assert и Assert — две стороны одного уточняющего примитива; выбор делается конвейером диспетчеризации автоматически по критерию «доступны ли свободные переменные предиката на этапе компиляции».

Базовая сигнатура: assert: (cond: Bool, ?msg: String | Error) -> Assert(IsTrue(cond))

Правило диспетчеризации:

Критерий	Режим	Поведение
Все свободные переменные известны на этапе компиляции (параметры дженерика, константы времени компиляции)	CompileTime	Вход в конвейер доказательств: true → стирается до Void, false → ошибка компиляции (Never не имеет обитателей)
Присутствуют свободные переменные времени выполнения (параметры функций, внешний ввод)	Runtime	Вставка проверки Bool во время выполнения, внедрение уточняющего факта в потоко-чувствительный набор предположений Γ

Потоко-чувствительный набор предположений Γ:

Компилятор поддерживает для каждой точки потока управления множество известных пропозиций:

yaoxiang

assert(x > 0)       // Γ = {x > 0}
y = x + 1           // Γ = {x > 0, y > 1}  ← распространение SP
mut x = x - 5       // Γ = {}  ← kill set mut: старые предположения более не действуют

После присваивания mut-переменной все предположения, относящиеся к этой переменной, удаляются (kill set). При слиянии ветвей Γ берётся как пересечение предположений ветвей.

8.4 Terminates: предикат меры завершимости

Terminates — это встроенный предикат, относящийся наряду с Int, Never к базовым примитивам (встроенное имя, не ключевое слово). Он привязывает меру к вычислению, утверждая завершимость этого вычисления и давая свидетельство завершимости.

Форма: одна и та же двухарная функция с одной и той же предикацией:

Форма	Точка привязки	Назначение
`Terminates(m)`	Имя текущей привязки	Форма по умолчанию — самовызывающие функции, циклы
`Terminates(FnType, m)`	Явный функциональный тип	Когда нужно явно указать принадлежность меры (мера определена в другом месте, одна мера обслуживает несколько вычислений)

yaoxiang

// Мера: обычная функция, тестируемая, переиспользуемая, не участвует в рантайме
gcd_measure: (a: Int, b: Int) -> Int = { b }

// Двухарная форма: мера определена в другом месте, явно указана принадлежность
gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

// Одноарная форма: точка привязки — имя привязки, мера — выражение в области видимости
loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n {
        i = i + 1
    }
    return acc
}

Семантика: уточнение Terminates(m) действует на тип значения того вычисления, к которому оно приписано в своей позиции типа. Обязательство ложится на это вычисление — для функции на каждую точку рекурсивного вызова, для цикла на обратную дугу — в обоих случаях «мера следующего состояния строго меньше меры текущего состояния», оцениваемое под охраной пути в этой точке.

Обязательство в точке вызова: m(callee_args) < m(caller_args); обязательство на обратной дуге: m(следующая итерация) < m(текущая итерация). Оба имеют одинаковую форму.

Почему покрываются и циклы: цикл — анонимная конструкция, его обычно невозможно обозначить. Имя привязки и есть имя — acc в acc: Terminates(n - i) = while ... даёт точку привязки, поэтому цикл можно обозначить. В этом причина, по которой одноарная форма Terminates применима к циклам.

Мера: возвращаемый тип не ограничен (не требуется натуральное число); «строгое убывание» на ней задаётся подходящим порядком, доступным для этого типа. Является ли мера вполне обоснованной (например, при возврате Int — >= 0) — это отдельное обязательство, проверяемое конвейером доказательств времени компиляции так же, как и обязательство убывания.

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

Приоритет автоматического поиска: компилятор сначала пытается автоматически подобрать меру (четыре шаблона: линейная ранг-функция, счётчик нарушений предиката, ограниченный рост/убывание, мультипликативное масштабирование); только если не удаётся, требуется явное Terminates.

Представление в рантайме: чисто компиляционная сущность, стирается вместе со свидетельством, не попадает в бинарник рантайма.

Полное проектирование см. в RFC-027 §6.9 (семантика) и RFC-027a (механизм реализации).

Глава 9: Объединение и пересечение типов

9.1 Объединение типов

TypeUnion     ::= TypeExpr '|' TypeExpr

9.2 Пересечение типов

TypeIntersection ::= TypeExpr '&' TypeExpr

Синтаксис: пересечение типов A & B обозначает тип, одновременно удовлетворяющий и A, и B.

yaoxiang

// Композиция интерфейсов = пересечение типов
DrawableSerializable: Type = Drawable & Serializable

// Использование пересечения типов
process: (T: Drawable & Serializable)(item: T, screen: Surface) -> String = {
    item.draw(screen)
    return item.serialize()
}

Глава 10: Перегрузка и специализация функций

10.1 Перегрузка функций

yaoxiang

// Базовая специализация: использование перегрузки функций (выбирается компилятором автоматически)
sum: (arr: Array(Int)) -> Int = {
    return native_sum_int(arr.data, arr.length)
}

sum: (arr: Array(Float)) -> Float = {
    return simd_sum_float(arr.data, arr.length)
}

// Универсальная реализация
sum: (T: Add)(arr: Array(T)) -> T = {
    result = Zero::zero()
    for item in arr {
        result = result + item
    }
    return result
}

10.2 Платформенная специализация

yaoxiang

// Перечисление платформенных типов (определение стандартной библиотеки)
Platform: Type = { X86_64: () -> Platform, AArch64: () -> Platform, RISC_V: () -> Platform, ARM: () -> Platform, X86: () -> Platform }

// P — предопределённое имя параметра дженерика, обозначающее текущую целевую платформу компиляции
sum: (P: X86_64)(arr: Array(Float)) -> Float = {
    return avx2_sum(arr.data, arr.length)
}

sum: (P: AArch64)(arr: Array(Float)) -> Float = {
    return neon_sum(arr.data, arr.length)
}

Глава 11: Атрибуты типов

В YaoXiang есть только один атрибут типа, который нужно различать: линейный vs. копируемый. Он выводится компилятором автоматически.

11.1 Move (передача владения по умолчанию)

Все типы по умолчанию следуют семантике Move. Присваивание, передача параметра, возврат = передача владения.

yaoxiang

p: Point = Point(1.0, 2.0)
q = p           // Move, p более не может быть прочитан

11.2 Dup (мелкое копирование: копия дескриптора, общие данные)

Атрибут Dup используется для типов-ссылок/токенов. Присваивание типа Dup = мелкое копирование — копируется дескриптор/токен, базовые данные являются общими. Несколько владельцев указывают на один и тот же блок данных.

Тип	Атрибут	Пояснение
`&T`	Dup	Токен чтения нулевого размера, копия токена = несколько точек зрения на одни и те же данные
`ref T`	Dup	Копия Rc/Arc = счётчик ссылок +1, общие данные в куче
`&mut T`	Linear	Токен записи нулевого размера, эксклюзивный, не может копироваться
Все остальные типы	Move	Передача владения по умолчанию

Примитивные типы значений (Int, Float, Bool, Char) — особый случай встроенной обработки компилятора: при присваивании автоматически выполняется копирование значения, два значения полностью независимы. Это встроенное поведение компилятора, не атрибут Dup.

yaoxiang

// &T: Dup, свободное алиасирование
view: &Point = &p
view2 = view     // Dup: копия токена, оба действительны
print(view.x)    // можно
print(view2.x)   // можно

// &mut T: Linear, копирование запрещено
mut_ref: &mut Point = &mut p
// r2 = mut_ref  // ❌ &mut T не является Dup, копирование невозможно

11.3 Clone (явное глубокое копирование) и его связь с Dup

Clone — интерфейс явного глубокого копирования. Любой тип может реализовать Clone, предоставляя метод .clone().

yaoxiang

// Определение интерфейса Clone (стандартная библиотека)
Clone: Type = {
    clone: () -> Clone
}

// Использование
p: Point = Point(1.0, 2.0)
backup = p.clone()    // глубокая копия, p по-прежнему доступен
p2 = p.clone()        // можно клонировать несколько раз

Различие между Dup и Clone:

	Dup	Clone
Семантика	Мелкое копирование: копия дескриптора/токена, общие базовые данные	Глубокое копирование: создаётся полная независимая копия
Способ вызова	Неявно (при присваивании/передаче параметра автоматически)	Явно (`.clone()`)
Влияние изменений	Взаимно (общие базовые данные)	Не влияют (независимые копии)
Применимые типы	Токены `&T`, `ref T`	Любой тип, реализующий интерфейс Clone
Стоимость	Нулевая (токен — тип нулевого размера)	Зависит от типа

Dup не влечёт Clone, Clone не влечёт Dup — это две ортогональные концепции:

yaoxiang

// Тип Dup: копия токена, общие базовые данные
view: &Point = &p
view2 = view        // Dup: копия токена, оба указывают на тот же p
print(view.x)       // можно
print(view2.x)      // можно, видят те же данные

// Примитивный тип значения: автоматическое копирование значения компилятором (не Dup)
x: Int = 42
y = x               // копирование значения, x и y полностью независимы
print(x)            // можно

// Clone: явное глубокое копирование, создаётся независимая копия
p: Point = Point(1.0, 2.0)
q = p.clone()       // Clone: глубокая копия, p по-прежнему доступен
r = p               // Move: передача владения, потому что Point не является Dup и не примитивным типом значения

Замысел проектирования:

Dup предназначен для токенов/ссылок, решая проблему «несколько точек зрения на одни и те же данные».
Clone предназначен для сценариев, где нужна независимая копия; явный вызов делает стоимость видимой.
Копирование примитивных типов значений (Int/Float/Bool/Char) — встроенное поведение компилятора, не относящееся к Dup.
Большинство пользовательских типов по умолчанию используют Move, обеспечивая высокую производительность без копирования.

Глава 12: Типы токенов заимствования

12.1 Основные понятия

&T и &mut T — это токены нулевого размера на этапе компиляции. Это не «ссылки», а «типовое доказательство права доступа».

&T      →  нулевой размер, замораживает исходные данные (запрещает получение WriteToken в это время),
          при гарантии заморозки множественные только-чтения безопасны → Dup (можно копировать)
&mut T  →  нулевой размер, эксклюзивные чтение и запись (запрещает любые другие токены),
          при эксклюзивном доступе копирование бессмысленно → Linear (не Dup)

Ключевые свойства:

Токен — обычный тип, подчиняющийся тем же правилам области видимости, что и все остальные типы.
Не требуется аннотация времени жизни 'a.
Не нужен специальный проверяющий заимствований — права доступа естественно выводятся из атрибутов типов (Dup/Linear).
Полностью исчезает после компиляции, нулевые накладные расходы в рантайме.

12.2 Базовое использование

yaoxiang

// Сторона метода: объявление типа параметра определяет требуемые права
Point.print: (self: &Point) -> Void = {
    print(self.x)               // токен &Point даёт право на чтение
    print(self.y)
}

Point.shift: (self: &mut Point, dx: Float, dy: Float) -> Void = {
    self.x = self.x + dx        // токен &mut Point даёт право на запись
    self.y = self.y + dy
}

// Сторона вызова: компилятор автоматически выбирает заимствование или Move
p = Point(1.0, 2.0)
p.print()                       // компилятор автоматически создаёт токен &Point
p.shift(1.0, 1.0)               // компилятор автоматически создаёт токен &mut Point
p.print()                       // OK, предыдущий токен освобождён по завершении shift

// Несколько токенов &T сосуществуют — тип Dup допускает свободное копирование
distance: (a: &Point, b: &Point) -> Float = {
    sqrt((a.x - b.x)**2 + (a.y - b.y)**2)
}
d = distance(p, p2)

12.3 Область видимости и распространение токенов

Токен — обычный тип, поэтому он поддерживает все операции обычных типов:

Возврат токена — токен распространяется вместе с возвращаемым значением:

yaoxiang

// ✅ Дочерний токен и родительский токен возвращаются вместе
Point.get_x: (self: &Point) -> (&Float, &Point) = {
    return (&self.x, self)
}

p = Point(1.0, 2.0)
(px_ref, p) = p.get_x()        // токен возвращается вызывающему
print(px_ref)                    // OK, токен всё ещё в области видимости

Хранение в структуре — структура может иметь поля-токены:

yaoxiang

// ✅ Структура несёт токен как поле
Window: Type = {
    target: Point,
    view: &Point,              // поле-токен — содержит представление target только для чтения
}

Замыкания не захватывают, контекст фиксируется в точке создания — замыкание принимает только свои параметры; если нужны внешние данные, они фиксируются в замыкании в точке создания через каррирование:

yaoxiang

// ✅ Контекст фиксируется через каррирование: threshold — параметр, gt_point(threshold) в точке создания фиксирует значение в замыкании
gt_point: (t: Float) -> (p: Point) -> Bool = (p) => p.x > t
filter_by_threshold: (items: List(Point), threshold: Float) -> List(Point) = {
    items.filter(gt_point(threshold))
}

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

12.4 Автоматический выбор заимствования

На стороне вызова компилятор автоматически выбирает по следующему приоритету:

1. Если фактический аргумент используется далее → предпочтительно создать токен (&T или &mut T, согласно сигнатуре метода)
2. Если фактический аргумент далее не используется → Move
3. Порядок предпочтения: &T < &mut T < Move

yaoxiang

p = Point(1.0, 2.0)
p.print()          // тип параметра print — &Point → компилятор создаёт токен &Point
p.shift(1.0, 1.0)  // тип параметра shift — &mut Point → компилятор создаёт токен &mut Point
p2 = p             // далее не используется → Move

Получатель метода следует семантике сигнатуры (аналогично соглашению о записи получателя в RFC-011a): получатель &T → токен неизменяемого заимствования; &mut T → токен изменяемого заимствования; по значению → Move (поглощение получателя). Токен заимствования, порождённый в точке вызова, освобождается по завершении вызова (transient, см. §12.5); получатель заимствования в интерфейсе явно объявляется автором интерфейса как &Self, сигнатура impl после замены Self ↦ тип impl должна полностью совпадать с интерфейсом (RFC-011a §3).

12.5 Обнаружение конфликтов токенов

Обнаружение конфликтов токенов — это холловская пропозиция заимствования (RFC-009a), а не отдельный потоко-чувствительный анализ. Компилятор автоматически генерирует пропозиции заимствования (borrow_conflict/use_after_move/use_after_drop/mut_violation) и отправляет их в конвейер доказательств; активность токена — это интервал [created_at, last_use] (см. RFC-009a § обратный BFS-анализ активности):

yaoxiang

// ❌ &mut и производный &T не могут быть активны одновременно
bad_alias: (p: &mut Point) -> Void = {
    p.x = 10.0                   // ✅ штатное использование WriteToken
    print(p.y)
}

// ✅ После завершения области видимости токен автоматически освобождается
good_seq: (p: &mut Point) -> Void = {
    {
        // Внутренняя область видимости
        print(p.x)               // использование &mut Point
    }
    // Конец внутренней области видимости
    p.x = 10.0                   // ✅ WriteToken по-прежнему доступен
}

// ❌ Один и тот же фактический аргумент не может одновременно породить токен &mut и другие токены
alias_bad: (a: &mut Point, b: &Point) -> Void = { ... }
p = Point(1.0, 2.0)
alias_bad(p, p)                  // ❌ p одновременно порождает &mut и & токены

12.6 Внутреннее устройство компилятора: механизм брендов

Пользователь никогда не работает с брендами напрямую. Компилятор внутри назначает каждому токену уникальный идентификатор на этапе компиляции:

Видимое пользователю       Внутреннее представление компилятора
────────────────────────────────────────
&Point         →  ReadToken(Point, #N)    // #N — уникальное целое на этапе компиляции
&mut Point     →  WriteToken(Point, #M)   // #M — уникальное целое на этапе компиляции

Назначение брендов:

Защита от подделки: токен может быть получен только из капсулы владельца, не может быть сконструирован из ничего.
Отслеживание связей: производный &Float от доступа к полю несёт производный бренд (#N.field_x), компилятор может проследить до родительского токена.
Обнаружение конфликтов: одноимённый WriteToken и производный ReadToken не могут быть активны одновременно.

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

12.7 Сумма токенов

&BorrowToken ::= &T          // ReadToken (замораживает исходные данные → Dup безопасно)
               | &mut T      // WriteToken (эксклюзивные чтение/запись → Linear)

12.8 Токен заимствования vs `ref`

	`&T` / `&mut T`	`ref`
Что делает	Посмотреть / изменить на месте	Разделяемое владение
Область	Соответствует области видимости значения токена	Между областями видимости
Стоимость	Нулевая (тип нулевого размера, исчезает после компиляции)	Rc или Arc (выбирает компилятор)
Побег	Допустим (токен распространяется через возвращаемое значение/структуру)	Для этого и предназначен
Между задачами	Недопустим (передача токенов между задачами не реализована)	Допустимо (компилятор автоматически выбирает Arc)
Обнаружение циклов	Не задействовано	Внутри задачи — тихо, между задачами — lint

Примечание (не определено): как читать содержимое после создания ref (разыменование/метод/автоматически) пока не определено в спецификации, текущая реализация *a сообщает E1052. После определения будет добавлено в этот раздел.

Приложение: Краткий справочник по определениям типов

A.1 Определения типов

// === Тип записи (фигурные скобки) ===

// Тип записи
Point: Type = { x: Float, y: Float }

// Тип записи с вариантами (с использованием функциональных полей)
Result: (T: Type, E: Type) -> Type = { ok: (T) -> Result(T, E), err: (E) -> Result(T, E) }

// === Тип интерфейса (фигурные скобки, все поля — функции) ===

// Определение интерфейса
Serializable: Type = { serialize: () -> String }

// Тип, реализующий интерфейс
Point: Type = {
    x: Float,
    y: Float,
    Serializable    // реализация интерфейса Serializable
}

// === Функциональный тип ===

Adder: Type = (Int, Int) -> Int

// === Мера завершимости (встроенный предикат, см. §8.4) ===

// Одноарная: точка привязки — имя привязки (самовызывающие функции, циклы)
loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n { i = i + 1 }
    return acc
}

// Двухарная: явное указание принадлежности меры (мера определена в другом месте)
gcd_measure: (a: Int, b: Int) -> Int = { b }
gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

A.2 Синтаксис дженериков

// Дженерик-тип
List: (T: Type) -> Type = { data: Array(T), length: Int }
Result: (T: Type, E: Type) -> Type = { ok: (T) -> Result(T, E), err: (E) -> Result(T, E) }

// Дженерик-функция
map: (T: Type, R: Type)(list: List(T), f: (T) -> R) -> List(R) = { ... }

// Ограничение типа
clone: (T: Clone)(value: T) -> T = value.clone()
combine: (T: Clone + Add)(a: T, b: T) -> T = body

// Ассоциированный тип
Iterator: (T: Type) -> Type = { Item: T, next: () -> Option(T) }

// Дженерик времени компиляции: N используется в позиции типа (k: N) → параметр-значение времени компиляции
factorial: (N: Int)(k: N) -> Int = { ... }
Measure: (T: Type, N: Int) -> Type = { data: Array(T, N), length: N }

// Условный тип
If: (C: Bool, T: Type, E: Type) -> Type = match C { True => T, False => E }

// Специализация функции
sum: (arr: Array(Int)) -> Int = { ... }
sum: (arr: Array(Float)) -> Float = { ... }

A.3 Краткий справочник по атрибутам типов

// === Move (по умолчанию) ===
// Все типы по умолчанию Move. Присваивание, передача параметра, возврат = передача владения

// === Примитивные типы значений (встроены в компилятор) ===
Int, Float,     // при присваивании автоматически копируется значение, два значения полностью независимы
Bool, Char      // это не Dup, а встроенная обработка примитивов компилятором

// === Dup (мелкое копирование: копия дескриптора, общие базовые данные) ===
&T              // токен чтения нулевого размера, копия токена = несколько точек зрения на одни и те же данные
ref T           // копия Rc/Arc = счётчик ссылок +1, общие данные в куче

// === Linear ===
&mut T          // токен записи нулевого размера, Linear (эксклюзивный, не копируется)

// === Clone (явное глубокое копирование) ===
value.clone()   // создаётся независимая копия, изменения не влияют на оригинал

A.4 Краткий справочник по токенам заимствования

// === Токены заимствования ===
&T              // токен чтения нулевого размера на этапе компиляции, замораживает исходные данные → Dup (можно копировать)
&mut T          // токен записи нулевого размера на этапе компиляции, эксклюзивные чтение/запись → Linear (нельзя копировать)

// Автоматический выбор на стороне вызова
// 1. Фактический аргумент далее используется → создать токен
// 2. Фактический аргумент далее не используется → Move
// 3. Порядок предпочтения: &T < &mut T < Move

// Распространение токенов
// ✅ можно вернуть, можно хранить в структуре, можно захватить замыканием
// ❌ нельзя передавать между задачами (передача токенов между задачами не реализована)

Спецификация системы типов ​

Глава 0: Теоретические основы ​

0.1 Соответствие Карри-Ховарда ​

0.2 Тип как пропозиция, программа как доказательство ​

0.3 Влияние на проектирование языка ​

Глава 1: Классификация типов ​

1.1 Выражения типов ​

Глава 2: Базовые типы ​

2.1 Примитивные типы ​

2.2 Never и Void: ⊥ и ⊤ ​

Глава 3: Составные типы ​

3.1 Тип записи ​

3.1.1 Значения полей по умолчанию ​

3.1.2 Встроенные привязки ​

3.2 Тип интерфейса ​

3.4 Кортежный тип ​

3.5 Функциональный тип ​

Глава 4: Дженерики ​

4.1 Синтаксис параметров дженериков ​

4.1.1 Типы-контейнеры ​

4.2 Определение дженерик-типа ​

4.3 Вызов конструктора дженерика и вывод типов ​

Глава 5: Ограничения типов ​

5.1 Единичное ограничение ​

5.2 Множественное ограничение ​

5.3 Ограничения для функциональных типов ​

Глава 6: Ассоциированные типы ​

6.1 Определение ассоциированного типа ​

6.2 Дженерик-ассоциированные типы (GAT) ​

Глава 7: Дженерики времени компиляции ​

7.1 Параметры-значения времени компиляции ​

7.2 Константные массивы времени компиляции ​

Глава 8: Условные типы ​

8.1 Условный тип If ​

8.2 Семейства типов ​

8.3 Уточняющий тип Assert и утверждение assert ​

8.4 Terminates: предикат меры завершимости ​

Глава 9: Объединение и пересечение типов ​

9.1 Объединение типов ​

9.2 Пересечение типов ​

Глава 10: Перегрузка и специализация функций ​

10.1 Перегрузка функций ​

10.2 Платформенная специализация ​

Глава 11: Атрибуты типов ​

11.1 Move (передача владения по умолчанию) ​

11.2 Dup (мелкое копирование: копия дескриптора, общие данные) ​

11.3 Clone (явное глубокое копирование) и его связь с Dup ​

Глава 12: Типы токенов заимствования ​

12.1 Основные понятия ​

12.2 Базовое использование ​

12.3 Область видимости и распространение токенов ​

12.4 Автоматический выбор заимствования ​

12.5 Обнаружение конфликтов токенов ​

12.6 Внутреннее устройство компилятора: механизм брендов ​

12.7 Сумма токенов ​

12.8 Токен заимствования vs ref ​

Приложение: Краткий справочник по определениям типов ​

A.1 Определения типов ​

A.2 Синтаксис дженериков ​

A.3 Краткий справочник по атрибутам типов ​

A.4 Краткий справочник по токенам заимствования ​

Спецификация системы типов

Глава 0: Теоретические основы

0.1 Соответствие Карри-Ховарда

0.2 Тип как пропозиция, программа как доказательство

0.3 Влияние на проектирование языка

Глава 1: Классификация типов

1.1 Выражения типов

Глава 2: Базовые типы

2.1 Примитивные типы

2.2 Never и Void: ⊥ и ⊤

Глава 3: Составные типы

3.1 Тип записи

3.1.1 Значения полей по умолчанию

3.1.2 Встроенные привязки

3.2 Тип интерфейса

3.4 Кортежный тип

3.5 Функциональный тип

Глава 4: Дженерики

4.1 Синтаксис параметров дженериков

4.1.1 Типы-контейнеры

4.2 Определение дженерик-типа

4.3 Вызов конструктора дженерика и вывод типов

Глава 5: Ограничения типов

5.1 Единичное ограничение

5.2 Множественное ограничение

5.3 Ограничения для функциональных типов

Глава 6: Ассоциированные типы

6.1 Определение ассоциированного типа

6.2 Дженерик-ассоциированные типы (GAT)

Глава 7: Дженерики времени компиляции

7.1 Параметры-значения времени компиляции

7.2 Константные массивы времени компиляции

Глава 8: Условные типы

8.1 Условный тип If

8.2 Семейства типов

8.3 Уточняющий тип Assert и утверждение assert

8.4 Terminates: предикат меры завершимости

Глава 9: Объединение и пересечение типов

9.1 Объединение типов

9.2 Пересечение типов

Глава 10: Перегрузка и специализация функций

10.1 Перегрузка функций

10.2 Платформенная специализация

Глава 11: Атрибуты типов

11.1 Move (передача владения по умолчанию)

11.2 Dup (мелкое копирование: копия дескриптора, общие данные)

11.3 Clone (явное глубокое копирование) и его связь с Dup

Глава 12: Типы токенов заимствования

12.1 Основные понятия

12.2 Базовое использование

12.3 Область видимости и распространение токенов

12.4 Автоматический выбор заимствования

12.5 Обнаружение конфликтов токенов

12.6 Внутреннее устройство компилятора: механизм брендов

12.7 Сумма токенов

12.8 Токен заимствования vs `ref`

Приложение: Краткий справочник по определениям типов

A.1 Определения типов

A.2 Синтаксис дженериков

A.3 Краткий справочник по атрибутам типов

A.4 Краткий справочник по токенам заимствования