Перейти к содержанию

Дырки

Начиная с версии 0.9.0

Дырка — это часть терма, которая оставлена ненаписанной. Дырки служат для постепенной разработки доказательства. Мы оставляем ? там, где должен стоять подтерм, спрашиваем у Rzk, что там ожидается, и заполняем её, когда знаем, что нужно написать. Это аналог интерактивной разработки «через дырки» из Agda в режиме термов.

Дырка записывается как знак вопроса. Например, тело следующего определения — это одна дырка:

#define swap
  : (A : U) -> (B : U) -> (Σ (_ : A) , B) -> Σ (_ : B) , A
  := \ A B p -> ?

Дырке можно дать имя, добавив идентификатор после знака вопроса. Это удобно, когда в терме их несколько:

#define swap
  : (A : U) -> (B : U) -> (Σ (_ : A) , B) -> Σ (_ : B) , A
  := \ A B p -> (?b , ?a)

Где допустимы дырки

Дырка допустима только там, где её тип уже известен, то есть в позиции проверки, где Rzk проверяет терм относительно ожидаемого типа. Тело #define с аннотацией типа — такая позиция. Таковы же каждая компонента пары, каждая ветвь recOR и тому подобное.

Дырка в позиции вывода, где Rzk пришлось бы угадывать её тип, отвергается. Например, у дырки, использованной как функция, нет известного типа:

-- ошибка: невозможно вывести тип дырки
#define bad
  : (A : U) -> A -> A
  := \ A x -> ? x

Rzk не вводит метапеременные и поэтому никогда не угадывает тип дырки. Это делает смысл частичного терма предсказуемым. Дырка обозначает терм ровно ожидаемого типа и ничего больше.

По умолчанию дырки — это ошибки

По умолчанию rzk typecheck сообщает о каждой дырке как об ошибке. Завершённая работа не должна содержать дырок. Именно такое поведение нужно для готовой формализации и для непрерывной интеграции, где файл с незаполненной дыркой не должен проходить проверку.

$ rzk typecheck swap.rzk
...
found an unsolved hole
expected type (goal):
  Σ (x₁ : B), A

Просмотр дырки

Чтобы работать с дырками, мы передаём --allow-holes. В этом режиме Rzk принимает дырки и печатает для каждой из них её ожидаемый тип (цель) вместе с локальным контекстом:

$ rzk typecheck --allow-holes swap.rzk
Hole ?b at swap.rzk:2
  goal:
    B
  context:
    p : Σ (x₁ : A), B
    B : U
    A : U
Hole ?a at swap.rzk:2
  goal:
    A
  context:
    p : Σ (x₁ : A), B
    B : U
    A : U
Everything is ok! (2 hole(s))

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

  • context перечисляет локальные переменные-термы и их типы;
  • cube variables перечисляет локальные переменные, пробегающие по кубам (например, t : 2);
  • tope context перечисляет топовые предположения, действующие в месте дырки.

Показываются только локальные гипотезы. Глобальное окружение, то есть все предыдущие определения, намеренно исключается, чтобы цель оставалась читаемой даже внутри большой разработки.

Цель сохраняется в символьном виде. Составные определения показываются как написаны, без раскрытия. Для типа расширения цель несёт свою границу, так что видны условия, которым должен удовлетворять терм.

Когда в связывании используется образец-пара, например \ (t , s) -> ..., гипотеза показывается своим образцом, как (t, s) : ..., а не через проекции. Тем самым написанные нами имена компонент сохраняются в цели и контексте.

Любопытный факт

До появления дырок распространённой уловкой, чтобы увидеть ожидаемый тип, было поставить U на месте недостающего терма и прочитать ошибку типизации. Поскольку U редко имеет ожидаемый тип, Rzk сообщал тип, который он там ожидал, и это служило подобием цели.

JSON-диагностика

Для инструментов, не привязанных к конкретному редактору, и для непрерывной интеграции rzk typecheck --json выдаёт каждую диагностику, как ошибки типов, так и дырки, в виде JSON-массива в stdout. Сообщения о ходе работы идут в stderr. Команда завершается с ненулевым кодом только при наличии диагностики уровня ошибки. Дырка имеет уровень "warning", поэтому при --json файл с дырками всё равно завершается с нулевым кодом.

Каждая диагностика несёт уровень серьёзности, стабильный "code", исходную "location" и отрендеренное "message". Дырка дополнительно несёт свою структурированную цель и контекст в "hole":

{
  "code": "hole",
  "severity": "warning",
  "location": { "file": "swap.rzk", "line": 2 },
  "message": "Hole ?b at swap.rzk:2\n  goal:\n    B\n  ...",
  "hole": {
    "name": "b",
    "goal": "B",
    "termVars": [ { "name": "p", "type": "Σ (x₁ : A), B" }, ... ],
    "cubeVars": [],
    "topes": [],
    "shape": null
  }
}

Интеграция с инструментами

Та же информация о цели и контексте доступна инструментам как структурированные данные, а не только как текст. Поэтому редакторы и Rzk Playground могут показывать цель и контекст в месте дырки и обновлять их по мере редактирования терма. Языковой сервер сообщает о каждой дырке как о предупреждении, несущем её цель и контекст, следуя жёлтой подсветке «unsolved» из Agda.

Ограничения

  • Дырка принимает ожидаемый от неё тип. Её пока нельзя уточнить, написав внутри частичный терм, как это позволяет {! ... !} в Agda. Мы планируем это добавить.