Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Что мне на самом деле пока непонятно про сабтайпинг

Добавление к заданной в стиле bi-directional type-checking системе типов subtyping judgement — сущий пустяк, привносящий минимум сложности и не вызывающий неинтуитивного/нежелательного поведения языка. Однако этот пустяк значительно повышает удобство языка при работе с орнаментированными индуктивными типами (v : Vec[T, n] можно совать туда где требуется l : List[T]) и коиндуктивными типами (f : Int -> T) можно пихать туда, где требуется (f : Nat -> T).

Это дополнение перестаёт быть тривиальным в тот момент, когда мы начинаем позволять абстрактные параметры с upper/lower bounds. Как только мы допустили такие абстрактные параметры, у нас появляются модули (рекорды, содержащие opaque = abstract type members) и path dependent types. Это во-первых означает, что на уровне правил вывода необходимо гарантировать предикативность, в противном случае typechecking станет неразрешим (см. 1ML, Andreas Rossberg, страница 5), а во-вторых из-за path dependent types, type preservation перестаёт вообще говоря работать в непустом контексте (см. Dependent Object Types, Nada Amin).

Но оно того стоит!
* * *

Для индуктивных типов очень просто понять, что должно выражать subtyping-отношение. Давайте на примере Nat.

A :> Nat означает, что тип A снабжен морфизмами zero : Unit -> A и succ : A -> A, другими словами A снабжен структурой Nat-алгебры, например тип Ordinal конструктивных ординалов или тип Int целых чисел
E <: Nat означает, что к (n : E) можно применять элиминатор Nat.elim, т.е. что E снабжен структурой расслоения над типом Nat (инициальной Nat-алгеброй), например тип List

Когда мы определяем операцию сложения натуральных чисел стандартным образом, мы на самом деле не нуждаемся в том, чтобы оба аргумента были типа Nat, нам нужно чтобы один из них был надтипом Nat, а другой подтипом Nat:
add [A <: Nat <: B](a : A, b : B): a.elim
  zero: b
  succ: add(a, succ b)

В этом примере очень хорошо видно, как что система типов допускающая типовые параметры с верхними и нижными границами более выразительна существенным образом. И даёт нам возможность один раз написать функцию add, а затем использовать её для сложения иных сущностей очень общего вида. Ещё отметим, что часто тип можно множеством неэквивалентных способов снабдить структурой той или иной алгебры или расслоения, так что сабтайпинг обязан быть номинальным, чтобы быть удобным и понятным (т.е. например то, что тип Ordinal снабжен структурой Nat-алгебры должно вытекать из того, что конструкторы succ и zero в нём называются точно как в типе Nat и это сделано автором определения Ordinal нарочно, для чего автор должен указать в определении @import Nat или в явном виде писать в определении Nat.succ и Nat.zero).

Какую же семантику должно иметь отношение сабтайпинга для коиндуктивных типов? В одну сторону это очевидно:
E :> T должно означать, что к (e : E) можно применять все те же элиминаторы, что к (t : T), т.е. E является T-коалгеброй.

А вот
A <: T должно как-то означать, что элементы A должны быть задаваемы продуктивной T-корекурсией, что должно быть как-то эквивалентно тому, что A является корасслоением над T.

Как это правильно понимать?...
Subscribe

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 8 comments