?

Log in

No account? Create an account
"Зависимые" "типы" - Дважды мудак [entries|archive|friends|userinfo]
Декларативное рулит

Site Meter

[ website | Мой сайт ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

"Зависимые" "типы" [ноя. 21, 2017|01:32 am]
Andy Melnikov
[Tags|, ]

У хаскелистов есть локальный мем о том, что монады надо было назвать менее пугающе, какими-нибудь "теплыми и пушистыми штуками". Вот я думаю что с зависимыми типами та же история. И не только с типами, а вообще с функциональщиной.

Слово "типы" зашкварилось тогда, когда Рассел его забыл запатентовать, и его начали использовать для чего попало. Слово "лямбда" зашкварилось, когда Маккарти его украл у Чёрча, забывшего запатентовать. Даже слово "рекурсия" имхо зашкварено рекурсивными программами, т.к. Гёдель его забыл запатентовать. Более свежие зашквары - "нетотальность" зашкварена своим применением для обозначения чего попало. Слово "исчисление" законтачено интегральным исчислением, причём это редкий случай, когда в английском хуже, чем в русском.

Короче, туториалы по непонятным вещам ака НЁХ надо писать такими словами, чтобы не вызывать ложных аллюзий. Где-то видел пародийное объяснение устройства Saturn V словами, понятными ребёнку.

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

Далее, учебник по завтипам надо строить в обратную сторону - от верификации императивщины. Вообще, слово "программа" законтачено, по моему опыту в голове у людей под "программой" подразумевается одно из трёх:

- "семантический паскаль"
- "семантическая джава"
- "семантическая луа"

Надо сразу сказать, что луами занимаются структурные типы (см. тайпскрипт), джавами овнершип типы (см. rust), а мы начнём с того же с чего начали Ada Spark - с даже не семантического паскаля, а семантического ершова: с присваиванием, но без кучи, рекурсии и внешнего мира. Но дополненного эйфелеобразными контрактами - обычными ассертами и ассертами на пре- и постусловия.

Наша игра в подстановки - это не футбол, не дота и не шахматы, а скорее пасьянс, причём ближе к пауку с 4 мастями, которого почему-то все боятся. Программа на семантическом ершове играет роль колоды. Далее компьютер раскладывает эту колоду на игровом поле, а задача человека её сложить. Компьютер, как и в обычном пауке, следит за правилами и дает нам "читы" вроде возможности откатить и переиграть с любого места. Причём если получилось - то у нас не салют, а гарантия того, что в исходном ершове ни один ассерт не сработает. Это не так много, но считается, что этого достаточно, чтобы самолёты не убирали шасси стоя на земле и спутники не отворачивали антенны.

Педагогическая польза этой белиберды в том, что мы заявляем, что паук - это не язык программирования и не язык спецификаций, а некая логика/inference system. Что позволяет абстрагироваться от понятия компайл-рантайма, типов-значений, переменных, времени и т.п. и сосредоточиться на soundness. Т.е. сразу отметаются идеи "добавить в паук присваивание", т.к. любая модификация должна сохранять нашу гарантию.

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

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

И понятно, что формальная система паука не должна в общем случае походить на язык программирования - скажем, discharge of proof obligations by an smt solver or a non-constructive prover достаточно сильно не похоже на чисто функциональную трансляцию исходного ершова.

Далее, мы фокусируемся исключительно на статической семантике паука. И считаем, что у нас просто такое компайл-тайм перекладывание кусков текста программы на языке Ершова, т.е. у нас смешаны не типы и значения, а вспомогательные конструкции паука и фрагменты текста.

То есть к примеру, мы говорим студенту, что сигма-тип - это не тапл, тип второго элемента которого зависит от рантайм-значения содержащегося в первом элементе, а просто такая хитрая синтаксическая подстановка. Т.е. вот у нас есть (x: A) * B x и это просто 2 куска текста, в котором есть "локальный" кусок, обозначенный "буквой" x, который фигурирует (т.е. "подставлен") сразу во многих местах (подстановка B может быть "сколь угодно нелинейной"). И что эта конструкция нужна, чтобы "давать хинты" движку "пасьянса", какие синтаксические куски у нас "текстуально равны", чтобы ему было легче следить за правилами.

С пями та же самая история но в профиль, а лямбды \(x: A) -> ... - это просто способ изготавливать вторые компоненты-подстановки в сигмах (x: A) * B x и пях (x: A) -> B x

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

C индуктивными типами при таком педагогическом подходе тоже становится понятнее. Нам вообще плевать что у нас есть натуральные которые демонстрируют вычислительную мощь натуральных. Нам важно, что мы можем использовать мощь индукции при манипуляциях в пасьянсе. То есть, нам плевать на обычные элиминаторы, но критически важно (soundness all the way down!), чтобы были индуктивные элиминаторы, традиционно зашкваренно называемые "зависимыми". То есть, чтобы у нас была _доказательная_ мощь _аксиоматической теории_ натуральных, а на вычисление тотальных функций между натуральными нам по большому счёту плевать (и "в самолётах"/ершове натуральных всё равно нету, ибо анальное рабство хард реалтайма и всё преаллоцировано)
СсылкаОтветить

Comments:
[User Picture]From: thedeemon
2017-11-21 05:58 am
Up Goer Five - https://xkcd.com/1133/

Я с пасьянсами не знаком, про паука раньше вообще не слышал.

Пугливым студентам, мне кажется, можно давать книжку Type-Driven Development with Idris. Более мягкого, нежного, плавного (до занудности) введения сложно вообразить.
(Ответить) (Thread)
[User Picture]From: nponeccop
2017-11-21 07:23 am
Ну я как раз про идрис хотел написать - что для языка типа идрис подобный подход не сработает, потому что идрис изначально ЯП.

Я в принципе против любых аналогий, и цель поста не показать что придуманные мной аналогии как-то особенно хороши, а показать что текущие термины ужасны и педагогически вредны. А если человек пытается вникать в структуру слов, т.е. искать "зависимости", а не считать термины непрозрачными "сепульками" - то получается вообще жопа и misleading.

В этом плане никакой особой глубины аналогия с пасьянсом не несёт - паук просто один из нетривиальных пасьянсов, а идея пасьянса как игры в том, что это паззл для одного человека, т.е. нет противника. Можно заменить на судоку, например.
(Ответить) (Parent) (Thread)
From: (Anonymous)
2017-11-21 10:46 am
Просто освоение начинается с середины, отсюда все сложности. Если до хаскелей с идрисами почитать про TRS, полистать курс логики и нагуглить обзор методов, по которым работают (полу)автоматические пруверы, а заодно первые пару глав Барендрехта осилить, то волосы будут мягкими и шелковистыми. Хотя бы смутная картинка в голове сложится, и закидоны отдельных писателей не будут так сильно запутывать.
ИМХО никакие adhoc упрощения образования по теме не заменят. Всё равно всё сведётся к набиванию шишек граблями до просветления в каждом отдельном вопросе, а в сумме будет каша, так как эти прозрения в систему не выстроятся.
(Ответить) (Parent) (Thread)
[User Picture]From: phoonzang
2017-11-23 07:02 pm
вы бы заодно и накидали названий пары книжек для интересующихся
(Ответить) (Thread)
[User Picture]From: nponeccop
2017-11-23 09:38 pm
Я пока недостаточно разбираюсь в теме, чтобы что-то рекомендовать. Cам я читал талмуды вроде http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.6683
(Ответить) (Parent) (Thread)
[User Picture]From: phoonzang
2017-11-23 10:26 pm
спасибо за статью!
(Ответить) (Parent) (Thread)
[User Picture]From: wizzard0
2017-11-25 11:19 am
отлично! и да, пасьянсы общеизвестными не являются :)
(Ответить) (Thread)
[User Picture]From: nponeccop
2017-11-25 02:09 pm
А там и не предполагалось готового решения, лишь наброски принципов. Из которых основные "не врать" и "не вызывать паразитных ассоциаций". Но все решили что я вот прямо горжусь найденными метафорами.
(Ответить) (Parent) (Thread)