Интересно, типа.

[migmit]

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

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

В агде, если мой эклер меня не обманывает, требуется равенство по значению. А есть ли зависимые типы с равенством по ссылке? То есть, для того, чтобы Vector n Int был тем же типом, что и Vector m Int нужно не только n=m, нужно, чтобы n и m были одной и той же переменной.

Такое где-нибудь есть?

Update: подсказали, что это, вроде, называется "path dependent types".

Comments

[akuklev.livejournal.com]

Это называется runtime path dependent types. Могут быть реализованы в языках с зависимыми типами и individual types aka entities, т.е. “ран-тайм метками, равными только самим себе: совпасть должно не только место определения в коде, но и тред/момент создания”. Нужен оператор new, создающий такую метку, и процедуры использующие этот оператор — уже не чистые функции, результат их повторного выполнения с теми же аргументами отличается от исходного. Ещё можно красиво обобщить монады State и IO, так, чтобы там допустимо было использовать оператор new, тогда и только тогда, когда созданные объекты пихаются в состояние или вывод, а возвращаемое значение при одинаковых аргуменах одинаковое.

Бывают еще nominal path dependent types, там для равенства совпасть должно лишь место определения в коде, они эмулируются через экзистенциальные типы.

[migmit.livejournal.com]

> Это называется runtime path dependent types.

Э-э-э, почему runtime-то?

> Могут быть реализованы в языках с зависимыми типами

Defeats the purpose.

> они эмулируются через экзистенциальные типы.

КАК?

[akuklev.livejournal.com]

Ой, я был неправ, в DOT (такая концептуальная нью-скала) используются более другие "номинальные" путезависимые типы, в которых равенство не по совпадению места определения переменной, с которой ассоциирован тип, а таки по тому что “в компайл тайме можно проследить, что переменная была одна и та же”. Ну то есть, если есть объект, поименованный o1 и объект, поименованный o2 с вложенными типами .T, то o1.T == o2.T лейблы o1 и o2 являются физически одной и той же строкой, либо алиасами одной и той же сущности. И оно через экзистенциальные типы не эмулируется.

[migmit.livejournal.com]

Так. Картина мира потихоньку выпрямляется.

А как быть с вариантом про "совпадение места определения переменной"?

[akuklev.livejournal.com]

> А как быть с вариантом про "совпадение места определения переменной"?
Он в целом оказался ущербным и нигде кроме toy models не применяется.

[migmit.livejournal.com]

А как он, всё-таки, через экзистеншиалы эмулировался?

[akuklev.livejournal.com]

Да вот не знаю сам, а сходу чёт не придумывается. Поищу в статьях по этой теме.

[akuklev.livejournal.com]

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

Предположим, у нас есть тип Canvas, у объектов которого есть внутренний тип Point. (Чтобы сравнивать точки с разных холстов было невозможно, системы координат-то разное, а стало быть сравнение бессмысленное.)

Возьмём выражение val a = new Canvas; println([a.Point] == [a.Point]). Оно выдаст true. А если подставить, то выйдет println([(new Canvas).Point] == [(new Canvas).Point]), будет false. Исчисление с путезависимыми типами по-сути линейное, дупликация в нём только в явном виде допустима.

[migmit.livejournal.com]

Ну дык тайпчек идёт до редукций, так что пофигу.

[migmit.livejournal.com]

Фигню написал. Не совсем пофиг — развалится классическое требование "редукция сохраняет типизируемость", на котором куча всего построена. Но с этим наверняка можно справиться.

[m e (from livejournal.com)]

> Не совсем пофиг — развалится классическое требование "редукция сохраняет типизируемость", на котором куча всего построена. Но с этим наверняка можно справиться.

очень интересно взглянуть на эту "кучу"

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

[migmit.livejournal.com]

Ничего не понял.

[m e (from livejournal.com)]

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

[migmit.livejournal.com]

Как я понял, Scala справляется с этим, вводя синглетоновые типы x.type, где x — переменная.

[akuklev.livejournal.com]

Угу. И это затейливо. Хаскельную систему типов наивный подход к PDT поломает на раз, если не продумать всё оооочень аккуратно.

[m e (from livejournal.com)]

в упор не вижу ниче затейливого -- наоборот, все выглядит очень естественно (вне контекста х-я) и только так и должно быть

может расскажешь? особенно интересно, что сломают в хаскеле наивные PDT?

[akuklev.livejournal.com]

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

[m e (from livejournal.com)]

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

в реальном мире уже сам по себе факт, что мы может назвать одно х, а другое у, говорит о том, что они чем-то отличаются; возможно, конечно, что они отличаются только путем доступа, но (опять я скатываюсь на роль к.о.) нельзя 2 раза войти в одну реку (разным путем, гы-гы)

а еще я думаю, что часто Canvas будет определятся так, чтобы new_canvas().Y == new_canvas().Y, и проблемы нет

[m e (from livejournal.com)]

однако при этом

assert(new_canvas().Y == new_canvas().Y); // ok
c1 = new_canvas();
c2 = new_canvas()
assert( c1.Y == c2.Y ); // ok
c2.change_Y_to_Z();
assert( c1.Y == c2.Y ); // fail !!!

и если компилятору удается доказать, что от одного момента до другого втихую не была вызвана change_Y_to_Z(), то получаем PDT, а иначе программисту придется доказывать или вынести проверку c1.Y==c2.Y в рантайм, где в случае чего кидать исключение

[m e (from livejournal.com)]

короче, все эти (ваши) типы данных -- это fancy names для предикатов

но что действительно интересно -- что нечистота (а это она, родимая) может сломать в тайпклассах?