Интересно, типа.
Feb. 3rd, 2013 10:33 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
migmitВот есть, типа, такая типа штука, называется типа "зависимые типы". Когда сам тип содержит в себе значение. И два таких типа будут (типа) совместимы, если эти значения равны. А поскольку значения будут известны только в рантайме, приходится давать доказательство того, что значения таки равны.
А вот во всяких джавах с сиплюсплюсами равенств как минимум два. Не помню точно, как они называются, но, в общем, равенство по ссылке и по значению. Первое сильнее второго. То есть, если какие-то штуки лежат в одном и том же месте, то это одна и та же штука, и, значит, они одинаковые. Но если они одинаковые — это ещё не значит, что они лежат в одном и том же месте.
В агде, если мой эклер меня не обманывает, требуется равенство по значению. А есть ли зависимые типы с равенством по ссылке? То есть, для того, чтобы
Такое где-нибудь есть?
Update: подсказали, что это, вроде, называется "path dependent types".
А вот во всяких джавах с сиплюсплюсами равенств как минимум два. Не помню точно, как они называются, но, в общем, равенство по ссылке и по значению. Первое сильнее второго. То есть, если какие-то штуки лежат в одном и том же месте, то это одна и та же штука, и, значит, они одинаковые. Но если они одинаковые — это ещё не значит, что они лежат в одном и том же месте.
В агде, если мой эклер меня не обманывает, требуется равенство по значению. А есть ли зависимые типы с равенством по ссылке? То есть, для того, чтобы
Vector n Int был тем же типом, что и Vector m Int нужно не только n=m, нужно, чтобы n и m были одной и той же переменной.Такое где-нибудь есть?
Update: подсказали, что это, вроде, называется "path dependent types".
no subject
Date: 2013-02-04 07:22 am (UTC)no subject
Date: 2013-02-04 07:51 am (UTC)Не понял вопроса.
> как на них ссылаться
Не понял вопроса.
> и как доказывать равенство ссылок иначе чем в рантайме?
Чисто синтаксической проверкой. Если используется одна и та же переменная, то они совпадают, если нет - не совпадают.
no subject
Date: 2013-02-07 10:57 pm (UTC)как на них ссылаться -- ну например по адресу... а вообще вопрос наверно был "какой структурой данных представлять в рантайме тип данны", так?
и как доказывать равенство ссылок иначе чем в рантайме -- x.Y=z.Y если и только если компилятор может доказать что x=z; обычно доказательство черезвычайно тупо, но этого хватит