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

[migmit]

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

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

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

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

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

Comments

[krlz.livejournal.com]

В функциональных языках не может в принципе быть равенства по ссылке. У нас же referential transparency.

[migmit.livejournal.com]

Это какой-то сферический язык в вакууме. В Хаскеле, например, есть IORef-ы.

[krlz.livejournal.com]

Ну да, но есть же Eq IORef a, так что сравнения по ссылкам все равно нет.

[migmit.livejournal.com]

Не понял. Это и есть сравнение по ссылкам.

[jakobz.livejournal.com]

Ну что-то типа этого есть: http://www.haskell.org/ghc/docs/latest/html/libraries/base/System-Mem-StableName.html

Глупо было бы не иметь бесплатного "точно равно, т.к. физически указатели на один и тот же объект".

[thedeemon.livejournal.com]

В окамле есть = и ==, как раз по значению и по ссылке. Изредка даже пригождается на практике.

[krlz.livejournal.com]

Это оптимизация.

[krlz.livejournal.com]

Я не правильно выразился конечно. Имелось ввиду парадигма ФП противоречит равенству по ссылке. Сравнивая по ссылке, мы делаем хак.

[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, например. А так — всё хорошо.

[nealar.livejournal.com]

Vector (IORef n) Int ?

[migmit.livejournal.com]

Не понял, это имеется в виду какой-то существующий язык?

[nealar.livejournal.com]

Это имеется в виду несуществующий тип Vector. Который надо привинтить к существующему языку.

Зависимые типы

[livejournal.livejournal.com]

User nponeccop referenced to your post from Зависимые типы (http://nponeccop.livejournal.com/316607.html) saying: [...] В связи с [...]

[zhengxi.livejournal.com]

внутренние классы в скале ?

[migmit.livejournal.com]

Ха, забавно, очень похоже на правду.

[krlz.livejournal.com]

Имеются ввиду path dependent types? Так это просто разновидность dependent types.

[migmit.livejournal.com]

Так я не спорю, что разновидность.

[migmit.livejournal.com]

Хотя почитал тут — больше похоже на такие расширенные existentials, чем на dependent types.

[akuklev.livejournal.com]

Это называется runtime path dependent types. Могут быть реализованы в языках с зависимыми типами и individual types aka entities, т.е. “ран-тайм метками, равными только самим себе: совпасть должно не только место определения в коде, но и тред/момент создания”. Нужен оператор new, создающий такую метку, и процедуры использующие этот оператор — уже не чистые функции, результат их повторного выполнения с теми же аргументами отличается от исходного. Ещё можно красиво обобщить монады State и IO, так, чтобы там допустимо было использовать оператор new, тогда и только тогда, когда созданные объекты пихаются в состояние или вывод, а возвращаемое значение при одинаковых аргуменах одинаковое.

Бывают еще nominal path dependent types, там для равенства совпасть должно лишь место определения в коде, они эмулируются через экзистенциальные типы.

[migmit.livejournal.com]

> Это называется runtime path dependent types.

Э-э-э, почему runtime-то?

> Могут быть реализованы в языках с зависимыми типами

Defeats the purpose.

> они эмулируются через экзистенциальные типы.

КАК?

[akuklev.livejournal.com]

Ой, я был неправ, в DOT (такая концептуальная нью-скала) используются более другие "номинальные" путезависимые типы, в которых равенство не по совпадению места определения переменной, с которой ассоциирован тип, а таки по тому что “в компайл тайме можно проследить, что переменная была одна и та же”. Ну то есть, если есть объект, поименованный o1 и объект, поименованный o2 с вложенными типами .T, то o1.T == o2.T лейблы o1 и o2 являются физически одной и той же строкой, либо алиасами одной и той же сущности. И оно через экзистенциальные типы не эмулируется.

[nikita-timofeev.livejournal.com]

Объясни мне пожалуйста, где должны находится значения содержащиеся в типе, как на них ссылаться и как доказывать равенство ссылок иначе чем в рантайме?

[migmit.livejournal.com]

> где должны находится значения содержащиеся в типе

Не понял вопроса.

> как на них ссылаться

Не понял вопроса.

> и как доказывать равенство ссылок иначе чем в рантайме?

Чисто синтаксической проверкой. Если используется одна и та же переменная, то они совпадают, если нет - не совпадают.

[m e (from livejournal.com)]

где должны находится значения содержащиеся в типе x.Y -- имелось в виду "где должны находится типы Y, содержащиеся в значении x", так?

как на них ссылаться -- ну например по адресу... а вообще вопрос наверно был "какой структурой данных представлять в рантайме тип данны", так?

и как доказывать равенство ссылок иначе чем в рантайме -- x.Y=z.Y если и только если компилятор может доказать что x=z; обычно доказательство черезвычайно тупо, но этого хватит