Накидайте книжек по теории типов

И ещё, что нужно вкуривать перед HoTT?

Топология, теория гомотопий и алгебраическая топология же. Странный вопрос.

«Конкретная математика» очень неплоха.

Я про pre requirements в области теорию типов спрашиваю, MLTT?

Я про pre requirements в области теорию типов спрашиваю, MLTT?

Конечно же да.

«Конкретная математика. Основание информатики» — книга Дональда Кнута, Роналда Грэхема и Орена Паташника по математике, рассматривающая математические основы информатики, особенно анализа алгоритмов.

Это же не про теорию типов, не?

Всё равно не помешает.

Перепишись с бейсика на что-нибудь поадекватнее.

если судить по TaPL, то тебе может быть интересно так же software foundations, особенно вероятно том2. Но там все 3 тома с примерами на Коке https://softwarefoundations.cis.upenn.edu/, но это конечно больше по программированию. Что нужно перех HoTT я не знаю совсем.

Про SF я знаю, меня пока более математический смысл интересует.

TaPL

Гонимая книга, как по мне. Автор - конченый теоретик, уже забыл, как словами изъясняться. Такое впечатление, книга на агде написана вместо английского: «Теорема 28.3.1: Γ |-> T <: T is provable for every Γ and T. Доказательство: очевидно. Теорема 28.3.2: If Γ |-> S <: Q and Γ |-> Q <: T, then Γ |-> S <: T. Доказательство: очевидно.» И так целыми страницами. В печь идёт.

Лично мне TTFP куда лучше зашло. Тоже не идеал, но мотивация-интуиция более человечьим языком изложена. Остальное - пока хватает бэкграунда, чтобы излагаемую тарабарщину мысленно переводить на человеческий язык, типа Rust/OCaml/Haskell/Idris - норм идёт. Как только бэкграуд заканчивается - книга превращается в тыкву. Поэтому читал параллельно с «Type-driven Development with Idris». В таком сочетании норм. HoTT - не читал, я человек здоровый.

книжек по теории типов

Это еще что за диковина и когда на свет уродиться успела?

Лично мне TTFP куда лучше зашло.

Тоже читаю, хорошо идет.

Это еще что за диковина и когда на свет уродиться успела?

Это такая уличная магия, чтобы пугать динамических петушков.

https://www.cs.cmu.edu/~rwh/courses/hott/

Хм, спасибо

TaPL в процессе, есть что-нибудь ещё?

Надо брать сразу HoTT.

И ещё, что нужно вкуривать перед HoTT?

Зависит от целей. Если хочется просто потыкать палочкой, то берешь и читаешь первую часть, запиливая все примеры и задачи на cubicaltt.

Мне тоже понравились эти лекции. Присоединяюсь к рекомендации.

cubicaltt

Не слишком ли больно на таком писать? В Agda 2.6.0, говорят, cubical‐режим завезли.

Не очень больно, если есть некоторый опыт. Агда дофига сложная, а cubicaltt простой, как бревно. Да, «стандартная библиотека» практически отсутствует, нет никакой мебели а-ля экстракции как в Coq, удобства во дворе)

Но в качестве учебного языка лично мне вкатило.

Я просто пытался писать на кубике, и уже необходимость явной передачи всех аргументов огорчила: получалось что‐то вроде:

module comp_assoc where

fcomp (A B C : U) (g : B -> C) (f : A -> B) : (A -> C) = \(x : A) -> g (f x)

Path (A : U) (a b : A) : U = PathP (<_> A) a b
refl (A : U) (a : A) : Path A a a = <i> a

comp_assoc (A B C D : U) (f : A -> B) (g : B -> C) (h : C -> D) : (x : A) -> Path D ((fcomp A C D h (fcomp A B C g f)) x) ((fcomp A B D (fcomp B C D h g) f) x) =
  \(x : A) -> refl D (h (g (f x)))

Бесконечные «A», «B», «C» огорчают.

Ещё огорчили совсем короткие ошибки: просто «syntax error» или «type», например, без указания конкретного места и других подробностей.

Может я что‐то делаю не так? Я бы не против писать на гомотопическом с самых начал языке.

А так да: кубик очень простой.

Да, «стандартная библиотека» практически отсутствует, нет никакой мебели а-ля экстракции как в Coq, удобства во дворе)

Для доказательства теорем это же не так страшно.

Тут недавно Мортберг сотоварищи выкатили yacctt (код тут), который не так многословен (посмотри вот тут http://www.cs.cmu.edu/~amoertbe/slides/Mortberg-MURI18.pdf примеры).

Тут недавно Мортберг сотоварищи выкатили yacctt…

Ага, видел. Но там же вроде тоже надо все аргументы явно тащить, не?

Кстати, тот пример для кубика выше, в yacctt запустился без всяких изменений.

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

Ну вернее как непонятным... это было доказательсво алгоритма хиндли-милнера. В барендрегте сказано «смотри там то» и ссылка на оригинальную статью. Я пошёл, но я ж не математик, не продрался. Взял тапл, прочитал главу в котрой док-во, пришлось посидеть, но в целом всё вроде было понятно.

пришлось посидеть

Ну и нафиг такие книги, над которыми надо сидеть и расшифровывать? Жизнь девать некуда?

Вот как должна выглядеть хорошая книга: http://adit.io/posts/2013-04-17-functors,_applicatives,_and_monads_in_picture...

У автора ещё блог есть с побными постами и целая книжка по алгоритмам в таком стиле.

Просто сложные вещи сложны и описывать на 10 страниц то что пишется на одну страницу можно себе позволить только в исключительных случаях (а именно в книжках и статьях «для новичков»). Иначе книжки станут в тыщи страниц и остануться такими же непроходимыми, потому что когда уже научился читать, читать такую нудятину невозможно.

Правда, случаи разные. Но и книжки разные. Рад что ты для себя нашёл то что тебе по уровню подходит.

Нет никаких сложных вещей, есть неумение объяснять.

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

ну или да, никто объяснять не умеет в мире, один ты хренов гений, но скрываешь свои сверхспособности. Позвони в лигу супергероев... или нет, погоди, тебя не возьмут, твои способности слишком велики.

Как мне противно ставло от твоих реплик, сразу повеяло запахом водовки, картофанчика и 100500 однотипных интегралов с Демидовича...

ну да, матан ведь учат только на зашквареных совком просторах нашей бывшей необъятной. поди на бездуховном западе, как теперь и у нас, по модному молодёжному, вместо этого учат псалмы чтобы ракеты в космос пускать.

ты молодец, чё. блещешь мыслью.

100500 однотипных интегралов с Демидовича

Как будто что-то плохое. Ты, как я понимаю, европейских студентов не видел и пороху не нюхал.

Лол, но я и есть европейский студент.

Так тебе тогда и сравнивать нечего: ты же понятия не имеешь, какова водовка с картофанчиком на вкус. Да и запах Демидовича 80-х годов тебе тоже незнаком.

Да лол, закончил универ в России, а потом магистратуру здесь. Как земля и небо же.