Викиучебник по теории типов посоветуйте, пожалуйста.

Только не такой "продвинутый" — https://en.wikibooks.org/wiki/Homotopy_Type_Theory_using_the_Agda_HoTT_library
а попроще, более "от печки".

Нужна схема, что в каком порядке изучать.

И список понятий, которые надо знать, например:
2000, Владимир Воеводский, Гомотопическая теория типов (HoTT), https://github.com/HoTT/book/wiki/Nightly-Builds
1991, Хенк Барендрегт, Лямбда-куб
1988, Стефано Берарди, Чистая система типов
1889, Джузеппе Пеано, арифметика Пеано, аксиомы Пеано
Трансфинитная индукция
Математическая индукция
1925, интерпретация Брауэра — Гейтинга — Колмогорова
Соответствие Карри — Ховарда

логика высказываний соответствует простому типизированному λ-исчислению
исчисление предикатов — λ-исчислению с зависимыми типами
логика высказываний второго порядка — полиморфному λ-исчислению

Ну и список литературы, отсортированый по годам.

Может форум какой для этого есть специальный?
Только не такой — https://www.reddit.com/r/ProgrammingLanguages/comments/b7qecp/domain_theory_and_type_theory/
а русскоязычный.

Открыл учебник
2022, Кудрявцева И. А. & Швецкий М. В., Программирование теория типов
на странице 24-25, там написано:
Typ — так будем записывать называние множества типов, а конструировать его будем из символов `0` и круглых скобок.
у меня сразу вопросы:
— есть соглашение по скобкам, ок. Но что если склеиваются два типа с уже по-разному расставленными скобками?
например
(0 0) (0 0), это ведь не то же самое, что ( ( (0 0 ) 0 ) 0 ), и не то же самое, что соглашению о правоассоциативности.
это важно, это неважно, зачем вообще конструировать это множество? Почему его конструировать именно так?

Здравствуйте, Эйнсток Файр, Вы писали:

ЭФ>Викиучебник по теории типов посоветуйте, пожалуйста.

Не уверен точно, правильно ли тебя понял. У меня вот это есть, весьма неплохая книжка, и не надо быть академиком, чтоб разобраться. Посмотри, там по ссылке оглавление есть.

https://market.yandex.ru/product--tipy-v-iazykakh-programmirovaniia/1781358443?sku=781953036&uniqueId=2570656&clid=703

ЭФ>логика высказываний соответствует простому типизированному λ-исчислению
ЭФ>исчисление предикатов — λ-исчислению с зависимыми типами
ЭФ>логика высказываний второго порядка — полиморфному λ-исчислению

Влез в топик не потому что много знаю, а потому что знакомую букву увидел.

После λ-исчисления часть народа двинулась изучать pi-исчисление (там добавились конкурентность и состояние). А на базе этого pi-исчисления Lucius Greg Meredith изобрёл rho-исчисление. Вот пока я был в его команде (писали интепретатор и прувер), и все вокруг с горящими глазами рассказывали как же всё круто интерпретируется и прувится, показалось, что это rho-исчисление штука мощная, но малоизвестная и недооценная. В базу закладывали конкурентность, независимость процессов, полиморфность + когда изобретали про прувер думали.

Здравствуйте, hi_octane, Вы писали:

_>А на базе этого pi-исчисления Lucius Greg Meredith изобрёл rho-исчисление

Что почитать об этом подробнее? Накидай ссылок, пожалуйста, про pi- и rho-исчисление

_>> А на базе этого pi-исчисления Lucius Greg Meredith изобрёл rho-исчисление
Б> Накидай ссылок

проклятые блокчейн-фальшивомонетчики:

https://www.google.com/search?q=Lucius+Greg+Meredith+ro+calculus

Б>Что почитать об этом подробнее? Накидай ссылок, пожалуйста, про pi- и rho-исчисление
Ткнулся туда-сюда по старым закладкам — не открывается нифига

Вот тут, несмотря на просроченные сертификаты, немного ссылок есть, ведущих на pdf-ки по теме. И там же по связанным авторам/заголовкам можно погулять:
https://rchain.coop/research.html

И ещё тут есть ссылки на pdf-ки, в разделе Rho-calculus:
https://rholang.github.io/docs/research/

Всё что по пути попадётся про консенсусы смартконтрактов на блокчейне — можно игнорировать.

Да, это хорошая книжка, прям как мне надо:

2010, Пирс Б., Типы в языках программирования
(есть целиком в Library Genesis и Annas Archive)
я выбрал от издательства "Лямбда", там ещё другое есть

Особенно мне в оглавлении понравился пункт
"Расширенный пример: Облегчённая Java"

Книжку ещё не прочитал, но мне непонятно, как описывать массивы.
Открываю предметный указатель на странице 642, хоп, а массивов нет!

ЭФ> список понятий, которые надо знать

1910, теория типов Рассела (Ramified Theory of Types) Уайтхеда и Рассела
1925, простая теория типов Рамсея
1940, простое типизированное лямбда-исчисление Чёрча
1973-1984, конструктивная теория типов Мартина-Лёфа
1988-1992, чистые системы типов Бенарди, Терлоу и Барендрегта (Berardi, Terlouw, Barendregt)

Кто из них умеет в массивы?

Static elimination of array-bounds checking is a long-standing goal for type system designers. In principle, the
necessary mechanisms (based on dependent types—see §30.5) are well understood, but packaging them in a form
that balances expressive power, predictability and tractability of typechecking, and complexity of program annotations
remains a significant challenge. Some recent advances in the area are described by Xi and Pfenning (1998, 1999).

Здравствуйте, Эйнсток Файр, Вы писали:

ЭФ>Открываю предметный указатель на странице 642, хоп, а массивов нет!
Там есть списки. Возможно, массивы рассматриваются как частный случай списка с доступом по индексу.