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

[migmit]

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

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

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

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

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

Comments

[deni-ok.livejournal.com]

Это сузит пространство возможностей.

(++) : Vec A n -> Vec A m -> Vec A (n + m)

Конкатенируя Vec A 3 и Vec A 4 мы получим Vec A 7, только эта семёрка гарантировано не будет ссылочно равна никакой другой семёрке.

[migmit.livejournal.com]

Конечно, сузит. С другой стороны, возможно, это позволит получить некоторые плюшки зависимых типов, не нагружая программиста доказательствами. Т.е., доказательства сведутся к синтаксической проверке.

Я имею в виду плюшки такого типа:

data Ord a = Ord {compare :: a -> a -> Ordering}
data Set a (Ord a) = какая-то реализация
ordInt :: Ord Int
ordInt = Ord {compare = compareInt#}
a :: Set a ordInt
...
ordIntFake :: Ord Int
ordIntFake = Ord {compare = flip compare ordInt}

Ни в каком случае a не будет воспринято как Set a ordIntFake. Система классов и инстансов в Хаскеле этого не обеспечивает — можно описать разные инстансы в разных модулях и закрутить всё так, что они не станут друг другу мешать; в результате вполне можно получить, например, Set, содержащий какое-то значение несколько раз. Если же запихивать значение внутрь Set-а, то будет сложно делать union, например. А так — всё хорошо.