LINUX.ORG.RU
ФорумTalks

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

 , , ,


5

5

TaPL в процессе, есть что-нибудь ещё?
Желательно вместе с примерами на каком-нибудь Coq/Agda/etc
И ещё, что нужно вкуривать перед HoTT?

★★★★

Последнее исправление: Unununij (всего исправлений: 1)

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

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

IchBinFertig
()
Ответ на: комментарий от Unununij

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

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

IchBinFertig
()
Ответ на: комментарий от Deathstalker

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

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

IchBinFertig
()

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

AndreyKl ★★★★★
()
Ответ на: комментарий от AndreyKl

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

Unununij ★★★★
() автор топика

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 - не читал, я человек здоровый.

Begpoug
()

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

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

Siado ★★★★★
()
Ответ на: комментарий от Begpoug

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

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

mimimimi
()
Ответ на: комментарий от Siado

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

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

IchBinFertig
()

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

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

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

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

ymn ★★★★★
()
Ответ на: комментарий от e1nste1n

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

ymn ★★★★★
()
Ответ на: комментарий от IchBinFertig

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

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

ymn ★★★★★
()
Ответ на: комментарий от ymn

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

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, удобства во дворе)

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

IchBinFertig
()
Ответ на: комментарий от ymn

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

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

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

IchBinFertig
()
Ответ на: комментарий от Begpoug

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

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

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 3)
Ответ на: комментарий от AndreyKl

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

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

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

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

Begpoug
()
Ответ на: комментарий от Begpoug

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

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

AndreyKl ★★★★★
()
Ответ на: комментарий от Begpoug

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

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

AndreyKl ★★★★★
()
Ответ на: комментарий от AndreyKl

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

Begpoug
()
Ответ на: комментарий от Begpoug

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

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

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 1)
Ответ на: комментарий от Begpoug

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

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

ZERG ★★★★★
()
Ответ на: комментарий от Begpoug

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

ZERG ★★★★★
()
Ответ на: комментарий от ZERG

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

Begpoug
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.