(no subject)

Самый лёгкий в мире велосипед, как известно, весит 2.7кг (там из фич, правда, только тормоза и переключение скоростей, но это не помешало владельцу отъездить на нём тысячи километров), и сделан ещё лет пять назад, с тех пор никто не переплюнул.

Так вот вопрос: а почему компоненты из углеволокнистого пластика столько стоят? Что там именно дорогое? Сырьё копеечное, технология уж точно проще чем сталь варить...

Я тут почитал про успехи в области композитных материалов с использованием углеродных и борнитридных нанотрубок. Сегодня-завтра будет технически возможно изготовить велосипед весом 1.5кг (или 2-3кг без ущерба для комфорта), спортивный (т.е. пригодный для скооостей до 300км/ч) мотоцикл весом в 25кг или комфортный автомобиль весом в 150кг + батарея (она пока весит тонну с гаком, но придет тот день, когда она будет весить не намного больше полного бензобака, в пределах 100кг).
Но если углеволокно, которому уже 40 лет, стоит столько, то сколько же это стоить будет?

Вычислительная модель унивалентности

Скорее всего к вечеру в репозитории https://github.com/mortberg/cubicaltt/tree/equiv будет оконченное доказательство унивалентности (upd: сделали). Первая часть квеста, кажется, закончена: создано вычислительное обобщение MLTT, содержащее высшие индуктивные типы и доказывающее унивалетность, с разрешимым тайпчекингом, тотальным эвалюатором термов и каноничностью. Скорее всего скоро ещё доказуемость theorems for free повалит (т.е. внутренняя доказуемость параметричности полиморфизма). Будем знать, что любой терм t(T : Type, x : T) : T равен id_T и т.д.

Цена вопроса: правило J перестало быть верным по определению. Но судя по всему, делу можно помочь в очень широком классе случаев при помощи ручного тьюнинга в духе Observational Type Theory.
* * *
Чтобы два раза не вставать: ещё 10 лет назад некто Алексей Копылов написал диссертацию о представлении в рамках Extensional Type Theory структур данных, классов и объектов: http://files.metaprl.org/papers/thesis-kopylov.pdf

Это блестящая работа не только с точки зрения содержания, но и с точки зрения обозначений, вот так работать с теорией типов _удобно_, занимаясь программированием или математикой at large. Обязательно intersection types, обязательно ∈ вместо двоеточий и множественная принадлежность (имплицитные конверсии) термов, чтобы можно было писать про один и тот же икс что x ∈ Real и x ∈ Interval(2, 5), а также l ∈ List(Int) и l ∈ Vec(Int, some-length).

Язык программирования Scala сейчас скатился в не буду говорить что во многом* из-за того, что в нём понадобилось гибко работать тайпклассами, а сам язык такой функциональности не даёт, пришлось делать Shapeless, изобретая велосипед вручную. Тамошний HList это новый обрезаный class, только такой, что с ним можно работать нормально статически. А шейплесс это охрененно долбанутый на всю голову хак. А вот работа Копылова как раз показывает, как надо делать правильный ab initio Shapeless, чтобы обычные скальные определения классов и объектов дешугарились в него.

(* А в остальном он туда скатился, потому что стандартные библиотеки переползли на тайпклассы ровно одной ногой, не вытаскивая вторую из болота обратной совместимости с джавой, и потому что разработчики перестали чинить архитектурные баги, упёршись рогом в добавление фич.)

Впрочем, подход Копылова не позволяет, насколько я понимаю, сделать совсем Dotty. А вот подход Hickey с использованием Very Dependent Types как раз позволяет. Интересно есть ли Very Dependent Types в кубической теории типов? Ведь тогда туда и OOP мапится, и категории функторов можно строить для конкретных категорий, и, о счастье, повторить подход The Gentle Art of Levitation: сделать полноценную модель (рефлексию термов и типов) со вторичным использованием ambient type-checker'а.