Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Category:

"Зависимые" "типы"

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

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

Короче, туториалы по непонятным вещам ака НЁХ надо писать такими словами, чтобы не вызывать ложных аллюзий. Где-то видел пародийное объяснение устройства 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!), чтобы были индуктивные элиминаторы, традиционно зашкваренно называемые "зависимыми". То есть, чтобы у нас была _доказательная_ мощь _аксиоматической теории_ натуральных, а на вычисление тотальных функций между натуральными нам по большому счёту плевать (и "в самолётах"/ершове натуральных всё равно нету, ибо анальное рабство хард реалтайма и всё преаллоцировано)
Tags: fp, programming
Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 8 comments