Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

Как же до меня медленно доходит!

Как до жирафа. Всего-то лет десять прошло. В общем я о том, что translucent modules это “виртуальный” uncurrying тайпклассов.

Давайте работать в терминах предикативного λωΠΣW-исчисления, без каких либо предположений о существовании вселенных. Т.е. у нас как термы, так и типы могут быть зависимы как от термов, так и от типов, однако мы не смешиваем термы и типы, как это принято в традиции MLTT, благодаря тому что там подразумевается, что вселенные у нас есть.

Если у нас есть обыкновенный зависимый тип навроде Fin[n : Nat], то функцию f типа
Π(n : Nat).Π(m : Fin[m]).R никто не мешает оформить как f : Π(x : BoundedNat).R, где BoundedNat := Σ(bound : Nat).Fin[bound].

Вот и когда у нас есть зависимый от типов тип навроде Order[T] и полиморфная функция f : ∀(T).Π(o : Order[T]).R, мы хотим иметь возможность эквивалентно написать f : Π(x : Ordered).R, где Ordered что-то вроде Σ(T).Order[T], при в терминах Σ-типов мы это выразить не можем, T не терм, а тип. В MLTT мы можем аппроксимировать этот тип через U-Ordered := Σ(T : U).Order[T], где U — какая-нибудь вселенная, однако в этом случае мы фиксируем вселенную перед определением функции, и таким образом теряем требование, чтобы функция была параметрически полиморфна по T.

Отметим, что в MLTT сигнатура Π(T : U).Π(o : Order[T]).R гарантирует параметрическую полиморфность благодаря тому, что т.е. вселенные в MLTT не имеют элиминаторов и синтаксически невозможно написать неполиморфную функцию такой сигнатуры; однако двойственная ей через uncurrying сигнатура Π(x : U-Ordered).R уже ничего такого не гарантирует.

Так вот translucent modules, они же “records with abstract type members” это такой синтаксический сахар, который позволяет нам жить и писать так, как будто бы uncurrying для ∀(X).Y[X] существовал, получается такой специальный “рекорд” (X : ∗, y : Y[X]), в котором поле X такое специальное, что честной проекции на него не существует, но мы тщательно делаем вид, что она существует при помощи path dependent types (т.е. записей вида o.X), только ведёт себя не как все нормальные отображения, а как-то особенно хитро, на самом деле в точности так, чтобы "λo : (X : ∗, y : Y[X]). blablabla o.X blablabla" всегда можно было desugar'нуть в “Λ(X : ∗).λ(y : Y[X]). blablabla X blablabla”.

Семантически транслюсцентный модуль (рекорд с одним или несколькими абстрактными полями) следует понимать как типозависимый тип (тайпкласс) R[T1 T2 .. Tn : ∗], просто представленный синтаксически нетривиальным образом. В языках с развитой системой модулей, абстрактные поля могут иметь не только тип Type, но и тип иного транслюсцентного модуля, скажем M := (O : Ordered, x : X[O.Carrier],..), всё спокойно это дешугарится в вышеописанную схему, просто M[T : ∗] := (order : Order[T], x : X[T],..), в процессе, правда, возникнут higher kinded parameters, если тип абстрактного поля сам был параметризован. Функции, возвращающие translucent module после дешугаринга возвращают просто параметризованный одним или несколькими типами рекорд, т.е. f : X -> (∀(T).M[T]), функции, принимающие translucent module дешугарятся в полиморфные: f : (l : List) -> List.Item превращается в f : ∀(T). List[T] -> T. После такого дешугаринга можно заменить все ∀(T) на Π(T : U) без потери строгости, вот и всё. (Насколько я понимаю, higher kinded ∀'s тоже заменяются на Π's без потери строгости, хотя это совсем не элементарный результат.) Вот и ответ на мой вопрос про семантику сложных структур из прошлого поста.

А, да, про системы модулей в языках с отношением subtyping'а: указание верхних и нижних границ можно рассматривать на уровне семантики как дополнительные поля рекорда, обеспечивающие конверсию в/из абстрактного параметра 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.
  • 7 comments