Homotopy type theory

что ты сделал с выходными днями, отдай назад 4 штуки

4 штуки

не льсти себе так :з

А можно вкратце, для неискушенного в теориях типов человека, что это, чем оно отличается от MLTT (в плане, что оно дает на практике по сравнению с зависимыми типами)?

не льсти себе так :з

Причем, не только по зарплате, но и по умственным возможностям.

А как таковой практики (если ты о программировании) пока не было, если я правильно понимаю. Пока это всего лишь «многообещающий» мат. аппарат, который находится, как они сами говорят, «в разработке».

Причем, не только по зарплате

тебе за чтение книжек по выходным платят зарплату? о_О

а читать я буду сразу тот самый раздел, где «веселые примеры в картинках для детей-имбецилов»

Теория топосов

а читать я буду сразу тот самый раздел, где «веселые примеры в картинках для детей-имбецилов»

В том то и дело, что это не «Хаскель для имбецилов за 24 часа», это чистая математика. Или опять будешь «тупо заучивать последовательность символов»? Ты же тупой.

А какие пререквизиты у этой книжки? Что нужно уже знать, чтобы успешно ее прочитать?

Пререквизиты:

1. быть достаточно сообразительным чтобы догадаться залезть в текст и прочитать про остальные пререквизиты

Для Ъ твой способ не подходит.

Тоже хочу прочитать эту книжку, типы это хорошо. А книжка сама хорошая?

P.S. Хипстеры такие тупые.

А можно вкратце, для неискушенного в теориях типов человека, что это, чем оно отличается от MLTT (в плане, что оно дает на практике по сравнению с зависимыми типами)?

Оно ничем не отличается от MLTT (intensional + idetity types) в плане того что одно — внутренний язык другого ((inf, 1)-топосов), если использовать терминологию категорных логик. То есть отличается не более чем теория (MLTT) и её модель (HOTT).

По сути, HOTT утилизирует MLTT как внутренний язык рассуждений для определённого рода топосов, а поинт в том, что такого рода топосы это, помимо прочего, предмет изучения homotopy theory — есть теоремы о том, что MLTT имеет правильную интерпретацию в любой Quillen model category и что эта интерпретация также полна. Так что реализации MLTT в виде Agda или Coq можно сразу использовать чтобы «писать» рассуждения в рамках homotopy theory (что можно видеть в разделе code на их сайте).

Это добавляет к Curry-Howard-Lambek correspondence ещё и

MLTT                                    Homotopy theory

Types                                   Spaces
Terms                                   Maps
a : A                                   Points (1 -> A)                         
p : a = b (for Type)                    Paths (a => b)
w : p = q (for Id)                      Homotopies ( p ==> q)
...
x : A |- B(x)                           Fibration (B -> A)
x, y : A |- x = y                       Path space (A' -> A * A)
...

Гиперссылкою — http://ncatlab.org/nlab/show/homotopy type theory.

the impression is that homotopy type theory thus should serve as a foundation for mathematics that is natively about homotopy theory/(∞,1)-category theory — in other words, a foundation in which homotopy types, rather than sets, are basic objects.

Теория топосов
Жанр: Теория категорий

лол, это теперь жанр такой. Пример текста в жанре «Теория категорий»: «берёшь пандорический захват, лифтишь в монаду... и т.д.»

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

Прочитал тред, ни слова не понял. Тут все мехмат чтоли заканчивали?

Мехмат - говно.

Тут все мехмат чтоли заканчивали?

А Вася из соседней общаги, напяливший мамин шарф и бабушкины очки — интеллигент из Оксфорда.

Прочитал тред, ни слова не понял.

А ты и не должен был. В этом и суть.

LISP, Haskell и теория категорий — явления одной природы. Их роднит не только то, что в Haskell используются некоторые категориальные понятия. И то, и другое, и третье — предельно абстрактные дисциплины, практически не имеющие приложений, но изобилующие специальной терминологией и имеющие чрезвычайно высокий порог вхождения.

Этим и объясняется нынешняя мода на LISP, Haskell и теоркат. Обсуждая их на форумах, можно создать впечатление, что занимаешься чем-то возвышенным, заоблачным и недоступным простому смертному. Хотя на самом деле это будет не более чем псевдоинтеллектуальное теоретизирование, не имеющее практического смысла.

LISP, Haskell и теория категорий — явления одной природы.

ну я листал книжки по лиспу и хаскеллу (одну по лиспу и одну по хаскеллу), там как раз понятно всё написано было, а тут судя по словам какой-то нириальни матан для посвящённых.

PS правда лисп и хаскелл я на практике применить не смог и забил =)

Ну, это закономерный процесс. Одно время лисп и хаскелл были таким вот «матаном для посвящённых», сокровенным знанием. Потом началась популяризация: на густой аромат нонконформизма слетелись тысячи желающих быть «не-такими-как-все». Текущая ситуация такова, что на ЛОРе уже каждый школьник знает, что монада - это всего-навсего моноид в категории эндофункторов, а Рич Хикки ни черта не смыслит в гигиенических макросах.

Таким образом, лисп и хаскелл утратили элитарность. Поэтому появилась потребность в чём-то, что могло бы снова занять нишу. Этим и объясняется растущая популярность теорката и сопутствующих языков: Coq, Agda, Epigram, Omega и прочих.

Некто Andrej Bauer закончил работу над сабжевой книгой.

The book is the result of an amazing collaboration between virtually everyone involved in the Univalent Foundations Program at the IAS last year.

https://github.com/HoTT/book/graphs/contributors

Поправьте, пожалуйста!

языков: Coq, Agda, Epigram, Omega

Не слышал даже названий таких, до сих пор на плюсах пишу, как лох =)

LISP, Haskell и теория категорий — явления одной природы... имеющие чрезвычайно высокий порог вхождения.

Lisp — высокий порог вхождения? То-то его студенты изучают курсе так на втором и в качестве скриптового в AutoCad запихнули. На фоне Java разе что. А если сравнить хоть с C++, хоть c Perl — порог вхождения практически такой же.

Таким образом, лисп и хаскелл утратили элитарность. Поэтому появилась потребность в чём-то, что могло бы снова занять нишу.

Лол, в точности, как с айфоном. Быдлан покупает его для того, чтобы выделиться из массы таких же быдланов, как он. А потом ВНЕЗАПНО оказывается, что айфон есть у каждого первого быдлана.

Так и с лиспом. Ботаешь ты, значит, Let Over Lambda, а тут тебе какой-то школьник хренак с вертушки в щщи анафорической лямбдой!

Lisp — высокий порог вхождения? То-то его студенты изучают курсе так на втором

Для того, чтобы написать «Hello, World!» или там курсовую - порог низкий. Для того, чтобы реализовать реальный проект, надо скурить тонну священных книг навроде SICP, Practical Common Lisp, On Lisp, Let Over Lambda и подобных. Или, может, их просто так написали?

в качестве скриптового в AutoCad запихнули

То, что запихнули в AutoCAD - жалкий огрызок, к лиспу имеющий отношение только скобками.

тонну священных книг навроде SICP, Practical Common Lisp, On Lisp, Let Over Lambda и подобных. Или, может, их просто так написали

Про C++ и Java написано на два порядка больше. И для реального проекта на них придётся читать гораздо больше (потому как тупого smart_ptr на все случаи жизни внезапно перестанет хватать).

CL в этом смысле гораздо проще. Разве что библиотек не всегда хватает, но через FFI достаточно просто использовать любую библиотеку.

на хабре выложили перевод статьи The HoTT book.