Интересно, типа.
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-03 06:49 pm (UTC)no subject
Date: 2013-02-03 07:47 pm (UTC)no subject
Date: 2013-02-03 08:01 pm (UTC)no subject
Date: 2013-02-03 08:10 pm (UTC)no subject
Date: 2013-02-03 08:14 pm (UTC)no subject
Date: 2013-02-03 08:21 pm (UTC)no subject
Date: 2013-02-03 08:23 pm (UTC)no subject
Date: 2013-02-03 09:10 pm (UTC)Глупо было бы не иметь бесплатного "точно равно, т.к. физически указатели на один и тот же объект".
no subject
Date: 2013-02-04 07:26 am (UTC)no subject
Date: 2013-02-04 09:51 am (UTC)no subject
Date: 2013-02-04 10:02 am (UTC)