akuklev: (ДР Цертуса 2011)
[personal profile] akuklev
Как до жирафа. Всего-то лет десять прошло. В общем я о том, что 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 из/в указанной границы. И всё работает.

Date: 2016-10-27 03:37 am (UTC)
From: [identity profile] sspr.livejournal.com
И всё работает.

Как у Вас это все легко связывается и развязывается в голове?

Date: 2016-10-27 03:42 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
В том-то и дело, что не легко. То есть сейчас уже довольно легко, потому что я эту мысль с перерывами больше десяти лет думаю.

Недавно по случаю упавшей полки в кабинете как раз видел бумажку с черновиком на эту тему 2004-го года. Я на тот момент вообще ничего не понимал про категорную семантику всех этих штук, а пытался понять исходя из того как “ООП в духе С++” по человечески могло бы быть применимо для кодирования алгебраических структур, таких как группа или эвклидова плоскость. Самый первый черновик на эту тему насколько я помню 2001 года, но он как мне кажется не сохранился, да и не интересно, там везде пишутся очевидные с сегодняшней позиции вещи.

Date: 2016-10-27 05:10 am (UTC)
From: [identity profile] juan-gandhi.livejournal.com
Не скажу, что точно все понял, но да, частично да, действительно. Хорошо б на это все посмотреть просто с точки зрения пределов (ну или копределов).

Date: 2016-10-27 10:22 am (UTC)
From: [identity profile] maxim.livejournal.com
Я у Гамбино и Ликаты видел про эти компоненты рекордов-контекстов, которые обладают абстрактными членами.
Эти члены не доживают до коде-экстракта, но вполне используются и имеют свои иденсы при тайпчекинге.
Для этих штук вводятся специальные кодировки (0-абстрактный, 1-конкретный) с арностью.

0, 1, Bool, Nat, U    (1)
List                  ((0, 1), 1)
+                     ((0, 1), (0, 1), 1)
Id                    ((0, 1), (0, 0), (0, 0), 1)
Π                     ((0, 1), (0, 0), (0, 0), 1) ((0, 1), (1, 1), 1)
Σ                     ((0, 1), (1, 1), 1)
T                     ((0, 0), 1)


Это из синтаксической интерпретации зависимой теории, вот тут нашел http://smc2014.univ-lyon1.fr/lib/exe/fetch.php?media=msc-hott1.pdf

Date: 2016-10-27 03:11 pm (UTC)
From: [identity profile] nponeccop.livejournal.com
Вселенные вроде из предикативности возникают, и предикативное исчисление без вселенных - оксюморон. Технически Вы можете разве что конечное количество вселенных изобразить, сделав некоторые квантификации ill-typed.

Date: 2016-10-28 12:28 am (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Я описал это так, потому что хотел определённый синтаксис. Известно что “предикативные варианты” разных расширений System F (где предикативность энфорсится именно так, как вы сказали, ограничением допустимых квантификаций) эквивалентны (если мы рассматриваем только импликативный сегмент, без Σ-типов и индуктивных семейств) MLTT с той или иной иерархией вселенных. Мне хотелось не смотря на эквивалентность работать в синтаксисе расширений System F, чтобы было явное различие между типами и термами, и чтобы синтаксически исключить большие Σ-типы.

Date: 2016-10-30 12:01 pm (UTC)
From: [identity profile] migmit.livejournal.com
> λωΠΣW

Неприличными словами не выражаться!
Page generated Jul. 20th, 2017 10:36 pm
Powered by Dreamwidth Studios