Oct. 21st, 2016

akuklev: (ДР Цертуса 2011)
Добавление к заданной в стиле 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.

Как это правильно понимать?...
Page generated Sep. 19th, 2017 06:49 pm
Powered by Dreamwidth Studios