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

[migmit]

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

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

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

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

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

Comments

[migmit.livejournal.com]

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

[m e (from livejournal.com)]

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

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

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

[migmit.livejournal.com]

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

[m e (from livejournal.com)]

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