?

Log in

No account? Create an account
Previous Entry Share Next Entry
2016-01

Type system for numerics

Перечитал спеку Julia. Всё красиво-красиво. Некоторые вещи еще хорошо заходят, после K. Пошел читать ишшуи. "Пятачок, неси ружье!" Сколько corner cases, пиздец.

Вот интересно, можно ли вообще построить type lattice для сколько-нибудь нетривиального количества перпендикулярных свойств типов? (тип элемента матрицы, размерность матрицы, способ хранения матрицы например)

(Там обсуждают Кронекера, Иверсона и как уменьшить количество special кейсов для штук вроде Inf * Complex(0,0))

И типа что делать с генериками если оно взрывается когда матрицу населили какими-нибудь типами без обратного элемента..

Патамушо design space у меня в голове ж теперь еще шире после того как в K я могу написать "ABCD"="A" и получить (1;0;0;0)

akuklev подскажи, что почитать?

И интересно, можно ли программировать на языке у которого будет explicitly partial type system? Т.е. некоторые relations будут фэйлиться, в духе "is_subtype_of(A,B) = NaN", не тру, не фолс, а именно NaN? диспатч конечно будет безумный

This entry was originally posted at http://wizzard.dreamwidth.org/478559.html. It has comment count unavailable comments. Please comment there using OpenID.

  • 1
justy_tylor November 20th, 2016
У них перетаскивание в рантайм-диспатч и систему типов всего того бардака оптимизации, который решается адским говнокодищем в компиляторах и СУБД. Натягивают на единую specificity, что-то работает, а потом corner cases лезут. Я это упоминал в http://justy-tylor.livejournal.com/241882.html

И ещё тот момент, что numerics плохо вписываются в иерархии типов, сделать автоприведение из uint8 в uint32 это ок, а вот назначить один подтипом другого уже некорректно.

wizzard0 November 21st, 2016
Ну да, именно что в иерархии. Там остаются только relations, и то не факт. Надо попробовать осилить Ludics, но я пока не осилил.

akuklev January 13th, 3:20
Алсо, если удастся осилить Ludics, сообщайте. По-моему, это нечто инопланетное, и понять его нормально предстоит лет через 30, не раньше.

akuklev January 13th, 2:48
Про explicitly partial type system читать http://tyconmismatch.com/bh_talk.pdf и https://repository.upenn.edu/cgi/viewcontent.cgi?article=2031&context=cis_reports (“Combining Proofs and Programs in a Dependently Typed Language” by Stephanie Weirich, Vilhelm Sjoberg and Chris Casinghino). Type lattices для нетривиального количества ортогональных аспектов прямо и не знаю, что почитать, но вообще работы по неиерархичному сабтайпингу позволяют всерьёз предположить, что такую систему изготовить можно, хоть и сложно.

По крайней мере разнесение аспекта “матричности”, типа элементов в её ячейках, размерности и конкретной имплементации выглядят совершенно возможными. Для этого нам потребуется два разных вида сабтайпинга — refinement subtyping и ornamental subtyping. Для этого нам понадобится
система типов с зависимыми высшими индексированными индуктивными и коиндуктивными типами данных, счётная иерархия унивалентных вселенных, наличие полиморфизма по вселенным, параметрических кванторов, непредикативной вселенной утверждений и туча релевантного для имплицитного сабтайпинга синтаксического сахара, реализующего рекорды (синтаксический сахар над коиндуктивными типами данных), модули (синтаксический сахар над рекордами и параметрическими кванторами) и орнаментацию, а также ручное управление имплицитным приведением между равными типами (в частности приведение между разными имплементациями матриц, например более или менее эффективными для разряженных матриц).

Edited at 2018-01-13 03:16 am (UTC)

wizzard0 January 14th, 0:09
Ух :) Ладно, я надеюсь, что как-нибудь в итоге разберусь)))

wizzard0 January 19th, 13:51
Почитал про орнаменты и partial types. Очень любопытно.

Хотя не выходит из головы мысль, что и то и другое продолжает путать типы и семантику, даже после того как в Transporting Functions across Ornaments ( https://arxiv.org/pdf/1201.4801.pdf ) отмечают, что это проблема -- но продолжают пытаться решить ее by construction, что является обратной задачей к очень банальному вопросу "подходит ли эта структура данных в данном месте?"

akuklev January 19th, 16:27
Мне кажется, “не типы и семантику”, а “реализацию и назначение”. Штука именно в том, что у двух вещей может быть по случайности совершенно одинаковая семантика, и в этом случае _вредно_ их идентифицировать.

Классический пример № 1:
Пусть CList — тип циклических списков, т.е. конечных списков по модулю группы сдвигов. В рамках этого типа CList(1, 2, 3, 4) = CList(4, 1, 2, 3) = CList(3, 4, 1, 2) = CList(2, 3, 4, 1).
Пусть тип Collection — тип конечных мультимножеств, т.е. конечных списков по модулю группы перестановок. Collection(1, 2, 3) = Collection(1, 3, 2) = Collection(2, 1, 3) = Collection(2, 3, 1) = Collection(3, 2, 1) = Collection(3, 1, 2).

В случае длины 2 типы CList и Collection совпадают — то и другое даёт неупорядоченную пару. И формально, и семантически. Но если какой-то язык программирования начнёт имплицитно конвертировать одно в другое, то надо дизайнеру этого языка за это сковородой по башке давать. Потому что идеологически типы разные, а их изоморфизм — артефакт малых размерностей.

Классический пример № 2:
Кстати, возникающий постоянно на практике — это типы s.Point и g.Point для разных, но изоморфных пространств s и g. В программировании это возникает при программировании GUI, там s и g разные холсты. В физике — это разные реально пространства могут быть.

Ещё это очень часто бывает с тайпклассами — один и тот же объект о запросто может быть группой или даже кольцом одновременно несколькими способами. Скажем, натуральные числа это одновременно полукольцо по сложению и умножению, и полукольцо по сложению и взятию максимума.

И чтобы с этим работать нам существенно нужна номинальность — имплицитные приведения в целом и сабтайпинг вообще должны быть не структурными, а номинальными, т.е. типы конвертируются только если при их определении программист в явном виде (при помощи имён, как правило, откуда и возникает термин “номинальность”) указывает, что _подразумевается_, что всякий x : A автоматически является x : B. Единственный случай, когда структурный сабтайпинг возможен — это сабтайпинг вдоль “забывания дополнительной структуры”. Т.е. сабтайпинг, что “чётное целое” это тоже "целое", "кольцо с делением" это тоже "кольцо", а "функция на целых числах" это в том числе и "функция на натуральных числах".

Иными словами, refinement subtyping may be structural, but ornamental subtyping MUST be nominal.
Так вот, наивный подход к орнаментам (в частности проступающий в приведённой статье) этого не учитывает, и горе ему в этом месте. К счастью, отец родной орнаментов, Конор, наш дорогой, МакБрайд, всё это понимает. Есть где-то даже видеозапись его клёвой лекции, где он предостерегает от наивного подхода к орнаментированию, при котором возникают ситуации, что “электрочайник надо понимать как разновидность кочерги”.

wizzard0 January 19th, 17:05
> Так вот, наивный подход к орнаментам (в частности проступающий в приведённой статье) этого не учитывает, и горе ему в этом месте. К счастью, отец родной орнаментов, Конор, наш дорогой, МакБрайд, всё это понимает.

О, круто, я рад что мне не показалось и что мы on the same page (и что что-то понял в этом всем, гг).

Мне вот кажется, что если мы констрейним (индексируем в этой терминологии?) CList и CCollection, то (явный, наверное) каст между ними, когда они имеют длину ровно 2 как раз имеет смысл. Partial equality / conditional equality, хз.

Ну т.е. мы говорим что если List[T][len:N] = (N=0): Pair[T] (T, null) | (N>0): Pair[T](T, List[N-1]), то от этого List[1] не перестает каститься в Pair, и Pair (иммутабельную) всегда можно скастить в List[1]

Причем, возможно, List может быть определен двумя способами, и ту же пару можно скастить, например, в List[2] (если мы говорим, что List[0] это Pair[Sentinel,Sentinel], List[1] это Pair[T1,Sentinel] то у нас список из нулла и T, очевидно, имеет длину два), и вот в этом месте начинается номинальность и это надо ресолвить примерно как ambiguous overloads.

А распространять это неограниченно/автомагично пытаться выгребать все возможные интерпретации, конечно, приведет к кочерге и/или кочерге, которая состоит из чайников.

Edited at 2018-01-19 05:07 pm (UTC)

akuklev January 19th, 17:16
Явный каст конечно ОК. А вот именно за неявный — кочергой по чайнику. ;-)

wizzard0 January 19th, 17:16
О, я понял, чего тут не хватает.

У нас есть как минимум четыре домена, не два. С терминологией очень сложно, попробую попроще изложить.

1. Энкодинг номинальных типов в структурные. Хотя бы в битовые вектора. Vector <-> Theorem (интерпретация вектора). Tagless, т.е. "какой энкодер выбрать - задаем извне".
2. Номинальный энкодинг функций на теоремах (Theorem, Theorem, ...) -> Semantic(Semantic(...)), т.е. Proofs из Combining Proofs and Programs
2.1. Составленная из них, собственно, полезная программа.
3. Множество структурных семантик на битовых векторах, аксиоматическое (ну процессор у нас такой, говоришь ему Функция 5 от 001 и 010 - будет 111, и он не знает что это в семантике юзерской)
4. Набор конкретных реализаций Programs для структурных (!) типов, где тайпчек - это процесс выбора тех, что подходят под Proofs, и тайпчек и позволяет размапить энкодинг на вот эту базовую конкретную семантику. Тут можно пытаться их генерить, будет кодоген.

Итого получается в одном флаконе и компилятор/интерпретатор, и тайпчекер. А если рассматривать по отдельности - то как-то оно, ммм, выглядит бессистемным.

UPD: proofs and programs подходит к этому достаточно близко, и в общем тут наверное полезно определять три уровня, пруфы, абстрактная реализация, и конкретная реализация, в том смысле что абстрактная реализация это Program из P&P, а конкретная - уже machine code для Program-ов, скомбинированных так, что пруфы сходятся.

Edited at 2018-01-19 05:20 pm (UTC)

akuklev January 19th, 17:21
Вечная проблема высокосогласованных систем — на куски толком не разделишь, так чтобы можно было эти куски отдельно рассматривать, а вся система целиком настолько сложна, что чтобы суметь её прожевать и проглотить целиком, не разделяя на куски, нужна масса мотивации и многие месяцы работы (которым должны предшествовать годы тренировки мозга, чтобы в него вообще влезали абстракции такого размера). :-(

wizzard0 January 19th, 13:58
То есть, глубокий лифтинг это замечательный инструмент, но это скорее обобщение генериков (параметрического полиморфизма), потому что вот у нас например есть перемножение скаляров, и оно коммутативно, и есть перемножение матриц, оно не коммутативно.

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

Пример второго места, где происходит смешение семантики и типов -- если либа дефайнит умножение как repeated addition, и не требует от базового типа умножения вообще -- то она в матрицы лифтанется, но снова неправильно.


Edited at 2018-01-19 02:02 pm (UTC)

akuklev January 19th, 16:34
Дадада! Вот я в комменте выше именно про это.

Глубокий лифтинг (много лет назад это называлось транссемантическим переносом или гиперсемантическим программированием) должен оставаться инструментом ручным, а не автоматическим. Во-первых при переносе на новую структуру может понадобиться ручная доводка (добавление “аспектов” (в смысле аспектного программирования) поверх базового лифтнутого кода), во-вторых во многих случаях вообще фигня получается (точнее, не фигня, а “то что было сложением превращается в сопряжение схем и должно быть соответствующим образом переименовано и документированно”).

wizzard0 January 19th, 14:09
О, я понял, чем мне так не понравились орнаменты. Пример с lookup > опирается, вообще-то, не на магическую изоморфность между списками и числами, а на то, что у нас Nat в арифметике Пеано построен как List of Unit, и *число* - это cardinality множества (пространства?) значений List of Unit. Но что если мы захотели, ммм, оптимизации! и строим числа как binary tree of unit? (и нас интересует cardinality деревьев, количество листьев листья, количество листьев и узлов (оно не равно cardinality всего пространства), или вообще не дерево взяли а pairing function?, не важно). Как тогда доказать, что вот такой список длины N у нас все еще подходит в либу, которая хочет список длины N?


Edited at 2018-01-19 02:15 pm (UTC)

akuklev January 19th, 16:50
С этим как раз проблемы не будет. Перенос между разными имплементациями Nat (и вообще разными имплементациями любого типа или любой структуры) происходит в гомотопических теориях типов вдоль заданного пользователем в качестве доказательства равенства изоморфизма (и не может происходить иначе — не тайпчекнится оно), так что тут всё будет корректно.

wizzard0 January 19th, 16:55
А, понял идею. То есть у нас есть номинальное равенство (не обязательно reflexive, кстати, мне кажется что для partial type systems важны и просто односторонние импликации), и если по решетке равенств оно сходится, или есть путь по графу рефлексивных равенств, то считаем, что тайпчекнулось.

Edited at 2018-01-19 04:56 pm (UTC)

akuklev January 19th, 17:01
Да.

  • 1