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

[migmit]

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

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

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

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

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

Comments

[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 для предикатов

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