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

[migmit]

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

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

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

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

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

Comments

[krlz.livejournal.com]

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

[migmit.livejournal.com]

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

[migmit.livejournal.com]

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

[krlz.livejournal.com]

Там можно писать что-то вроде:

val x = ...
val y: x.T = ...

те мы можем ссылаться на type member-ы pure value-ов, и тип у нас реально зависит от значения

[krlz.livejournal.com]

Но это не полноценные dependent type-ы как в агде конечно. Реально у нас есть только dependent function types, а dependent products на скале не выразить (я не знаю как по крайней мере).

def xyz(a: BBB): a.T = {...}

[migmit.livejournal.com]

Не от значения, а от ссылки. Потому что, если я правильно понимаю, возможно, что x == y, но x.T и y.T не совместимы.

[krlz.livejournal.com]

Тут они синтаксически сравниваются (как и в dependent type-ах), те после нормализации всех типовых функций, синтаксические деревья должны быть одинаковы. Вообще, прочитать более подробно то что это такое и как работает можно в книжке Design Concepts of Programming Languages в главе про модули.

[migmit.livejournal.com]

Так, это уже надо проверять. Ща займёмся.

[migmit.livejournal.com]

scala> class X {class Y; def test(y: Y) {}}
defined class X

scala> val x = new X;
x: X = X@1194cf5

scala> val xx = new X;
xx: X = X@17fc1e7

scala> val y = new x.Y
y: x.Y = X$Y@5d174f

scala> val yy = new xx.Y
yy: xx.Y = X$Y@dfbabd

scala> x.test(y)

scala> xx.test(yy)

scala> x.test(yy)
:12: error: type mismatch;
 found   : xx.Y
 required: x.Y
              x.test(yy)
                     ^

Или я что-то не понимаю, или x и xx не отличаются ничем, кроме физического расположения в памяти.

[krlz.livejournal.com]

В этом конкретно примере ничего плохого быть не может. Надо другой немного пример:

class X {type Y; def test(y: Y) {}}
val x: X = new X { Y = Int }
val xx: X = new X {Y = Bool}

Вот тут как раз это будет иметь смысл.

[migmit.livejournal.com]

> В этом конкретно примере ничего плохого быть не может.

Не понял это утверждение. Как говорится, "нет ничего страшного в том, чтобы помыть микроволновку". Пример показывает, что равенство значений ничего не даёт.

[migmit.livejournal.com]

То есть, если я правильно понял, происходит примерно следующее: для каждой переменной x создаётся новый тип x.type, который наследует все поля и методы того типа, который для x объявлен; внутренние типы становятся его членами.