Зависимые типы и мутабельность

Для начала, давай определимся о каком языке идет речь?

А есть живые языки с зависимыми типами и мутабельными структурами данных?

с зависимыми типами и мутабельными структурами данных?

Я намекал, что не плохо бы строже оформить свои желания. Какой-нибудь псевдокод что-ли. Нихрена не понятно же, что есть зависимый тип, по-твоему?

Под зависимыми типами я имею в виду общепризнанный термин. Тип, зависимый от значений.

Кто-нибудь использовал Xanadu?

Хороший вопрос. Я таких систем не знаю, но, думаю, это возможно. Есть системы, в которых мутабельность видна на уровне типов — скажем, capability calculus. Вероятно, можно адаптировать это дело и под зависимые типы.

увеличить, например, число элементов в списке

Тогда тип этого объекта не «список из 5 целых», а просто «список целых».

А если у тебя зафиксировано количество элементов, то получишь ошибку типа на операцию добавления элемента.

Да, косвенные ссылки могут быть только у совместимых типов. В смысле Rest(List-5-Ints) вернет не просто список целых, а List-4-Ints.

P.S. Практическое применение есть в Typed Racket. Только там типы не выводятся, а только проверяются.

Тогда тип этого объекта не «список из 5 целых», а просто «список целых».

Т.е. мутабельный тип в принципе не может быть зависимым? Okay.

Xanadu, кстати, не смотрел?

Т.е. мутабельный тип в принципе не может быть зависимым

Ну почему? У указанного списка могут меняться элементы. Значит он мутабельный.

А ещё можно сконструировать тип «Список не более 10 целых».

Xanadu, кстати, не смотрел?

Практически нет

Про ATS уже сказали?

Для мутабельности в чистом (и, возможно, тотальном) языке «с типами» всегда достаточно монады IO и ссылок. В агде, например, это будет такой интерфейс:

IO : Set → Set
return : {A : Set} → A → IO A
bind : {A B : Set} → IO A → (A → IO B) → IO B
...

Ref : Set → Set
new : {A : Set} → A → IO (Ref A)
write : {A : Set} → Ref A → A → IO T
read : {A : Set} → Ref A → IO A
...

для него даже не нужно зависимых типов — достаточно обычного полиморфизма (по Set). И обратно — такая мутабельность не может ничего сломать в зависимых типах, если они есть, так же как она ничего не ломает в хаскеле.

Такой интерфейс суть теория (явного) IO и (явно) мутабельных (явных) ссылок (для более продвинутой теории нужно ещё навешать разных утверждений о том как все эти вещи ведут себя вместе). В качестве моделей могут выступать — 1) RTS-магия, в агде (MAlonzo) можно эти сигнатуры сделать примитивами (postulate) и перепоручить прагмами GHC (а сам хаскель делает точно так же, то есть в языке предоставляет IO и Ref-ы как абстрактные типы, оставляя всю работу RTS), вот запускаемый пример — Вышел пятый выпуск Haskell Platform (комментарий); 2) чисто языковые вещи — IDE для Haskell - когда появится? (комментарий).

Про ссылки есть глава в TAPL.

Ещё на тему семантики IO, памяти, ссылок и т.п. именно в языках с зависимыми типами — http://www.staff.science.uu.nl/~swier004/publications.html, точнее — http://www.staff.science.uu.nl/~swier004/Publications/Thesis.pdf, http://www.staff.science.uu.nl/~swier004/Publications/DepTypesForDistrArrays.pdf, http://www.staff.science.uu.nl/~swier004/Publications/MoreDepTypesForDistrArr..., http://www.staff.science.uu.nl/~swier004/Publications/HoareLogicStateMonad.pdf.

Ох. Спасибо=)

ИО для мутабельности совершенно излишне. Что за привычка совать монады повсюду, даже если они к теме никоим боком не относятся?

повсюду

Не повсюду а

в чистом (и, возможно, тотальном) языке «с типами»

А чистым и тотальным ему нужно быть затем, чтобы функции были функциями в математическом смысле и equational reasoning теории работал, как я понимаю. Либо никакого изоморфизма Карри-Говарда.

Либо никакого изоморфизма Карри-Говарда.

Ну и ладно. Зачем он нужен?

equational reasoning теории работал

Прекрасно, пусть работает. С чистотой и тотальностью это никак не связано, достаточно, чтобы для языка была определена операционная семантика.

Но даже если принять подобные возражения - все равно при чем тут монады? Это просто эталонный пример, когда монадический интерфейс пытаются сунуть туда, где он и близко не нужен с точки зрения семантики.

2) чисто языковые вещи — IDE для Haskell - когда появится? (комментарий).

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

Зачем он нужен?

Это одно из направлений развития статических систем типов и соответствующих языков — тупая недо-логическая система синтаксических рассуждений о корректности программ и данных, скажем так, превращается в достаточно выразительную _логическую_ систему (так что понятия непротиворечивости, правильности и т.п. становятся строгими).

Про CH применительно к ФП — http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf, http://www.cs.cmu.edu/~rwh/plbook/book.pdf (XI), ATTAPL тот же.

И если делать язык на основе какой-то теории типов (с CH и непротиворечивостью) какой-то типизированной лямбды с консервативными расширениями, то для сохранения всех ништяков IO, event-loop-ы и т.п. вещи за пределами тотальной вычислимости должны реализовываться, по сути, левыми библиотечными средствами как монады (или как-то ещё, но не важно — если это «как-то ещё» достаточно выразительно, то оно эквивалентно монадическому интерфейсу, то есть либо в него оборачивается, либо делается над ним). Можно это считать минусом, или нет.

С чистотой и тотальностью это никак не связано, достаточно, чтобы для языка была определена операционная семантика.

Если функции в языке это чистые математические функции, то сразу работает не какой-то там, а именно обычный математический (логический, алгебраический и т.п.) ER. А вот если эффекты не выделены в отдельный слой, то элементарное x : A; y : A; x-equal-y : Id A x y теряет смысл — непонятно, как доказывать равенство, если x и y это на самом деле не термы A, а effectful вычисления (если термы IO A — никаких проблем).

То есть чистота необходима для нормального ER, тотальность полезна для него, а достаточно выразительная теория типов с CH предполагает нормальный ER, но трудно себе представить непротиворечивую теорию типов с CH в грязном языке.

при чем тут монады?

Речь про чистые языки?

Тогда io monad — http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf, state monad, free monad над императивным языком, просто абстрактный тип.

В Haskell, Agda, Coq (Ynot) как-то ничего лучше не придумали.

Partiality monad — та же история.

Там ниже упрощённая версия на хаскеле. По сути free monad над императивным языком — умеет последовательное выполнение и прикидывается как будто умеет работать с памятью, которая моделируется как функция. То есть эквивалентно чистому State — State становится «настоящим» IO когда ему RealWorld подсовывают, а эта штука станет «настоящей» если ей дать настоящую (volatile) память.

Это одно из направлений развития статических систем типов и соответствующих языков

Но есть ведь и другие?

тупая недо-логическая система синтаксических рассуждений о корректности программ и данных

Почему же недо? Вполне формальная и логическая.

И если делать язык на основе какой-то теории типов (с CH и непротиворечивостью) какой-то типизированной лямбды с консервативными расширениями, то для сохранения всех ништяков IO, event-loop-ы и т.п. вещи за пределами тотальной вычислимости должны реализовываться, по сути, левыми библиотечными средствами как монады

То есть все интересное из рассмотрения выкидывается, а все тривиальное и неинтересное - остается. Ну это как заниматься изучением теории групп, оставив только тривиальную группу.

Если функции в языке это чистые математические функции, то сразу работает не какой-то там, а именно обычный математический (логический, алгебраический и т.п.) ER.

Он и так сразу работает. Если формальная семантика задана. Она за тем и задается.

непонятно, как доказывать равенство, если x и y это на самом деле не термы A, а effectful вычисления

На основе формальной семантики, понятное дело. Ясно, что не очень удобно - но это хотя бы возможно, в отличии от ИО-термов - где ничего вообще доказать нельзя. Просто объявляется что проблемы нету, т.к. мы ее замели под ковер. А раз нету проблемы - то нету и решения.

Тогда io monad — http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf, state monad, free monad над императивным языком, просто абстрактный тип.

Ну дальше-то что? Да, есть очень неудобный путь моделировать это дело через монады. Но это только один путь. И самый кривой из существующих. Зачем его вообще упоминать?

Там ниже упрощённая версия на хаскеле.

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

То есть эквивалентно чистому State — State становится «настоящим» IO когда ему RealWorld подсовывают, а эта штука станет «настоящей» если ей дать настоящую (volatile) память.

Ну память или World не важно - идея одна тут. Но кто мне помешает взять твой World (или память) и раскидать его копии по десятку разных функций? Да никто. И пиздец твоей реализации приходит.

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

Ты можешь рассказать про то как сделать лучше и про то где это сделано лучше, а то вот я не знаю.

Но есть ведь и другие?

Ну дык вперёд — повествуй :) От меня-то что нужно.

Почему же недо?

Логическая это когда ты типу ставишь в соответствие утверждение (логическое, да) и обратно, а вся система получается правильной (относительно работающих программ которые типизируются — если некое свойство утверждается и доказывается в системе, то так и должно быть при выполнении) и непротиворечивой, плюс она должна быть выразительной, в смысле теоретико-доказательной силы. А если взять типичную систему типов и типичный язык — она слабая, она не позволяет логической интерпретации типов, то есть позволяет, но это будет противоречивая «логика» (то есть всё есть истина, так как любой тип населён), она не позволяет проводить ER и т.п. рассуждения над (грязными или нет) функциями.

То есть все интересное из рассмотрения выкидывается, а все тривиальное и неинтересное - остается.

Ну всё интересное по части программ-алгоритмов есть, например — http://www.cis.upenn.edu/~bcpierce/sf/, http://adam.chlipala.net/cpdt/.

По части эффектов и т.п. тоже ничего под ковёр не заметается, например — http://ynot.cs.harvard.edu/.

Ну и тут надо определиться — мы говорим про конкретные языки или вообще про семантику «зависимые типы + мутабельность». Вообще, язык на основе Теории Типов + монадки для эффектов это как бы мейнстрим в вопросе «зависимые типы + мутабельность» — если есть что-то ещё, то интересно что это.

Он и так сразу работает.

Я привёл пример:

x : Nat
x = 4

y : Nat
y = 2 + 2

x-equal-y : x == y
x-equal-y = refl

а потом, если без системы эффектов в монаде, мы меняем y = read-nat-from-stdin. Непонятно, что там «работает» (нет, ну в рамках формальной семантики всё работает как должно, но речь про более универсальный (обычный математический) смысл понятия, и это не только ER может быть, но и вообще FOL, HOL и т.п.).

Ясно, что не очень удобно - но это хотя бы возможно, в отличии от ИО-термов - где ничего вообще доказать нельзя.

«Не очень удобно» это «вообще невозможно рассуждать», потому что код грязный (его нужно сначала от эффектов отделить, чтобы что-то можно было сказать). Ну и я не знаю, в чём у тебя трудности с тем, чтобы что-то доказать про IO.

Спасибо за пояснения... Я постараюсь во все это въехать. Но я вот все-равно не вижу примеров на тему

как они решают проблему косвенных ссылок на один и тот же объект?

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

Я говорю о том что знаю, в частности — человек спросил про зависимые типы и мутабельность, вот я говорю — это давно не проблема

Вот в этом и дело. Ты же человеку не предложил способ решения, вместо этого ты просто заявил, что это «не проблема» - ведь можно взять любой мутабельный код, сказать, что он лифтанулся в ИО, а потому никакой проблемы и нет. То есть она, конечно, по факту никуда не делась - просто из метаязыка перешла к языку ИО-терма. Но ты об этом человеку не сообщил.

Логическая это когда ты типу ставишь в соответствие утверждение

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

А если взять типичную систему типов и типичный язык — она слабая, она не позволяет логической интерпретации типов

При чем тут вообще система типов? Для простоты можно считать, что у нас обычная нетипизированная лямбда. Любое свойство любой программы, написанной на нетипизированной лямбде можно вывести из операционной семантики этой лмябды (из правил редукции). Ничего больше не требуется, совершенно ничего.

Ну всё интересное по части программ-алгоритмов есть, например — http://www.cis.upenn.edu/~bcpierce/sf/, http://adam.chlipala.net/cpdt/.

По части эффектов и т.п. тоже ничего под ковёр не заметается, например — http://ynot.cs.harvard.edu/.

Ну так там и ИО никакого нетути. Это все умеет любой прувер, безо всяких типов.

Вообще, язык на основе Теории Типов + монадки для эффектов это как бы мейнстрим в вопросе «зависимые типы + мутабельность»

Заметание проблем под ковер вместо их решения - всегда было популярным (мейнстримным) методом, да.

Я привёл пример:

и?

а потом, если без системы эффектов в монаде, мы меняем y = read-nat-from-stdin. Непонятно, что там «работает»

Все работает.

нет, ну в рамках формальной семантики всё работает как должно

А ничего больше требовать и не возможно.

«Не очень удобно» это «вообще невозможно рассуждать», потому что код грязный

Ну и что что грязный? Это грязь у нас описана формально строго - так что мы можем делать любые выводы о том, как она себя ведет.Хоть это и сложно.

(его нужно сначала от эффектов отделить, чтобы что-то можно было сказать).

Нет, не надо. Как только мы отделяем от эффектов в то же ИО, то мы уже ничег осказать не можем.

Ну и я не знаю, в чём у тебя трудности с тем, чтобы что-то доказать про IO.

А как? Семантики-то у ИО нету. Фактически мы задачу анализа грязного исходного языка сводим к задаче анализа грязного языка, на котором написаны ИО-термы. Только формального описания ИО-языка у нас нет, и вообще его в хоть сколько-нибудь явном виде нет - а потому и анализировать нечего. У нас даже и терма-то самого нет - есть только некоторая программа, которая генерирует этот терм! То есть вместо того, чтобы анализировать терм с эффектами в соответствии с его семантикой ,мы объявляем, что этот терм (и все подобные термы) - terra incognita, не подчиняется никаким законам, никаким спецификациям, не обладает никакими свойствами, находится за горизонтом событий и делит вселенную на нуль при попытке его вычислить. Другими словами все термы в ИО - это на самом деле совершенно одинаковые термы. В том смысле что мы не можем указать ни одного свойства, которое бы эти термы различало.

Можно сделать такую систему типов, которая просто не даст тебе сделать несколько ссылок на один объект. Тогда все работает. Правда и мутабельность тогда не нужна в явном виде.

Но кто мне помешает взять твой World (или память) и раскидать его копии по десятку разных функций?

Никто не гарантирует, что рантайм на си, сишные библиотеки, ядро, физическая память, порты, процессор и т.п. работают так, как должны.

Вот у тебя есть чисто функциональная спецификация IO которая в качестве модели состояния использует чисто функциональную же структуру данных (какой-то тип, словарь, функция из адресов в значения как модель «массива») для моделирования состояния, она работает ожидаемым образом. Дальше можно доказывать какие-то теоремы — как сочетаются чтение и запись, например. Если теперь хочется чтобы всё это работало с настоящим внешним состоянием, то эту структуру данных нужно заменить на фиктивную абстрактную которая будет вести себя как внешнее состояние, так, как должна. Если «реальный мир» будет себя вести как полагается, то все теоремы из спецификации останутся в силе, если «реальный мир» не ведёт себя как «реальный мир» — извините. Это как с примитивными операциями — они вводятся в язык одними сигнатурами, не определениями, реализуются подходящим для данной архитектуры способом, либо внешними библиотеками, то что железо или RTS библиотеки работают как должны и то что свойства этих операций такие, какими они должны быть можно только постулировать (в агде для этого есть ключевое слово postulate, фактически — axiom).

Зачем тебе нетипизированная лямбда с грязью и внешними утверждениями с сопутствующей FOL? Это где вообще такое? Типы это и есть утверждения, а теория типов вместо FOL, и Curry/Howard/Lambek/... есть, язык для эффектов и конкурентности оформляется явно (по Хоару, например), фиксируется (монадическими) типами, реализации с библиотеками есть, литература, опять же. Ну то есть мне не понятно что ты предлагаешь взамен — названий и ссылок не видно.

На счёт IO — почитай ссылки на Wouter Swierstra и туториал с публикациями про Ynot, там IO (Cmd в Ynot) не абстрактный как в хаскеле, абстрактно может быть внешнее состояние, используется Hoare Type Theory, так что можно доказывать теоремы про код с эффектами. В агде IO это библиотечная вещь — можно клепать по штуке за вечер :) (даром что не нужно).

Но я вот все-равно не вижу примеров на тему

Поставь задачу, а то я не вполне представляю в чём проблема. Что-нибудь модельно простое, но конкретное, чтобы попробовать написать можно было.

Например, у нас есть функция f, принимающая не пустой мутабельный список lst и какую-то функцию g. В теле функции f мы принимаем функцию g для вычисления чего-либо, явным образом не связанного с lst, а далее уже работаем с lst, полагаясь, что список не пуст. И все бы хорошо, но мы можем передать в f такую g, которая на самом деле тем или иным образом захватила тот же самый список(или захватила какую-то функцию, которая захватила список и т.д.) и очищает его. Заметь, что ошибка будет только в том случае, если мы получим пустой список, а не просто будем читать список или даже добавлять его элементы. Мне кажется, что это никаким образом определить нельзя. А подобные вещи с мутабельными типами случаются слишком часто, чтобы забить на это.

Хотя вот Xanadu тот же я так и не посмотрел.

Никто не гарантирует, что рантайм на си, сишные библиотеки, ядро, физическая память, порты, процессор и т.п. работают так, как должны

Считаем, что они работают хорошо и корректно. Так вот, твое ИО мне не гарантирует, что в этих предположениях мой код будет корректен - потому что я могу распихать копии world и все сломается. То есть нет гарнатий корректности ИО-интерфейса. А вот в Clean есть - можно написать ИО-монаду корректность которой будет доказана тайпчекером.

Вот у тебя есть чисто функциональная спецификация IO которая в качестве модели состояния использует чисто функциональную же структуру данных

То есть тягает ее в виде аналога World? Ну вот о чем и речь - рантайм у нас в этом случае работает хорошо, корректно (т.к. сам чисто функционален), но корректность ИО гарантировать нельзя.

Типы это и есть утверждения

Но плохие, неудобные. Зачем ограничиваться таким подходом?

фиксируется (монадическими) типами

Зачем монадическими-то? :)

То есть f принимает мутабельную ссылку на обычный список. Если сигнатура f утверждает, что это ссылка на непустой список, то это значит только лишь что при вызове f нужно вместе с передачей ссылки доказать что она ссылается на не пустой список, после чего в f поступит именно такая ссылка, но _после_ сама f, g и кто угодно могут изменить значение по этой ссылке — это нормально, сигнатура говорит только о свойствах входа функции, вот если f захочет отдать эту ссылку ещё кому-то кто хочет чтобы данные по ней обладали определёнными свойствами, то f тоже должна будет явно доказать эти свойства. Правда всё это просто только при одной нити управления :)

Ещё если оставлять ссылки и их монады чисто абстрактными, то как-то проблематично выразить «мы вам передаём ссылку значение по которой имеет такие-то свойства», хотя просто делается «мы передаём ссылку с 'только что' (опять привет многопоточности) прочитанным из неё значением которое обладает такими-то свойствами», для примера:

module Refs where

open import Function
open import Relation.Nullary
open import Data.Unit using ( ⊤ )
open import Data.Nat
open import Data.List
open import Data.Product

Decidable₁ : (A : Set) → (A → Set) → Set
Decidable₁ A P = (x : A) → Dec (P x)

-- * Lists.

NotEmpty : {A : Set} → List A → Set
NotEmpty xs = length xs > 0

not-empty : ∀ {A} → Decidable₁ (List A) NotEmpty
not-empty xs = 1 ≤? length xs

NotEmptyList : Set → Set
NotEmptyList A = Σ (List A) NotEmpty
-- ^ <: List A

head : ∀ {A} → NotEmptyList A → A
head ([] , ())
head (x ∷ xs , _) = x

-- * Abstract monadic ref's.

infixl 2 _>>=_
infixl 2 _>>_
infixl 2 _>$>_

postulate

  IO : Set → Set
  return : ∀ {A} → A → IO A
  _>>=_ : ∀ {A B} → IO A → (A → IO B) → IO B

  &_ : Set → Set
  new : ∀ {A} → A → IO (& A)
  *_ : ∀ {A} → & A → IO A
  _≔_ : ∀ {A} → & A → A → IO ⊤

_>>_ : ∀ {A B} → IO A → IO B → IO B
x >> y = x >>= const y

_>$>_ : ∀ {A B} → IO A → (A → B) → IO B
x >$> f = x >>= return ∘ f

-- * Cached ref's.

&_as_ : (A : Set) → (A → Set) → Set
& A as P = & A × Σ A P

on-cached : ∀ {A P} {B : Set} → (Σ A P → B) → & A as P → B
on-cached f = f ∘ proj₂

try-use : ∀ {A B P} → & A → Decidable₁ A P → (& A as P → IO B) → B → IO B
try-use {A} {B} &x p f d = * &x >>= validate where
  validate : A → IO B
  validate x with p x; ... | yes wt = f (&x , (x , wt)); ... | no _ = return d

-- * ...

f : IO ⊤ → & List ℕ as NotEmpty → IO ℕ
f g (&xs , pre-readed) = g >> try-use &xs not-empty head-after-g 0 >$> _+_ head-before-g where
  head-before-g = head pre-readed
  head-after-g = return ∘ on-cached head

t : IO ℕ
t = new [] >>= λ &xs → push 1 &xs >> let g = &xs ≔ [] in try-use &xs not-empty (f g) 0 where
  push : ∀ {A} → A → & List A → IO ⊤
  push x &xs = * &xs >$> (_∷_ x) >>= _≔_ &xs

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

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

Ещё если оставлять ссылки и их монады чисто абстрактными, то как-то проблематично выразить «мы вам передаём ссылку значение по которой имеет такие-то свойства»

В чем отличие от «мы передаем значение, которое имеет какие-то свойства»? То есть банально лифтим все «свойства» (тип, то есть, весь все свойства содержатся в типе) в Ref и все, не?

Считаем, что они работают хорошо и корректно.

То есть нет гарнатий корректности ИО-интерфейса.

Считаем, что он работают хорошо и корректно.

Ну и если даже язык IO более явный и видимо корректный, а абстрактен сам World, то его некорректность это из серии «прищемить яйца дверью».

Зачем ограничиваться таким подходом?

Не зачем, конечно. Вот как будет что-то хорошее, удобное, так сразу :)

Зачем монадическими-то?

Это не причина, а свойство (в чистом языке, по крайней мере).

Свойства же нужны не ссылки, а значения по ней. То есть надо прочитать, то есть погрузиться в IO, то есть вместо Set/Prop будет IO Set/Prop в роли Set/Prop (IO уровнем выше), что как-то не очень реально. То есть такой пи-тип — {A : Set} {P : A → Set} (ref : & A) → ? (* ref) P, непонятно, что делать с ?.

Считаем, что он работают хорошо и корректно.

Давайте вообще тогда любую программу считать корректной, чего уж там :)