Здравствуйте, D. Mon, Вы писали:

V>>Ну, любой ссылочный тип у нас имеет T+1, потому что мы храним как значение T, так и ссылку на него.
DM>Чего-чего? Не надо про любой ссылочный тип, у них может быть разная семантика.

А если ты имел ввиду, что "ссылочность" значения прячется от системы типов, то ты в этом случае НЕ можешь рассуждать о ссылочном типе — это будет просто некая тонкость реализации.


DM>Трюк как в Option<Box<T>> годится только если Box<T> не может быть нулевым указателем.

Да понятно.
Правда, в этом случае не нужен промежуточный Box<T>, т.е. достаточно лишь Option<T>, не?

Потому что, если я правильно тебя понял насчет устройства Option<> в Rust, то можно был бы сделать так, чтобы из Option<T> получать сразу Box<T> при наличии значения. И такая операция была бы "просто на бумаге", т.е. это было просто приведение типов, а ссылка была бы та же.


DM>Если ты не можешь отличить null как None от null как значение исходного ссылочного типа, то все, приехали

Ссылочный тип по-определению — это зависимый тип.
Тот самый, угу.

Т.е., тип, зависящий от значения:
* валидный адрес — тип T
* нулевой адрес — тип None.


DM>это уже не тот Option из теории типов, это уже кривая поделка, где алгебра не работает и жди проблем.

Тпру-у-у ))

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

Потому что ссылочный тип уже имеет необходимую семантику зависимого типа. И потому что зависимый тип конечного диапазона можно представить как простой алгебраик (вернее, завернуть зависимый тип в алгебраик, стирая/маскируя "зависимость" типа через сумму типов), что и делается в той же монаде Maybe в Хаскель.

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


V>>Ну и попутно заметил, что для ссылочных классов многократное "оборачивание" null не требуется.
DM>С т.з. алгебры и теории типов — как раз требуется.
DM>F(T) = T + 1
DM>F(F(T)) = T + 1 + 1 = T + 2
DM>F(F(F(T))) = T + 3
DM>В частности, если T = 1, то F(F(T)) = 1 + 1 + 1 = 3, т.е. тип с тремя разными возможными значениями. Так из Option можно натуральные числа делать.

Надеюсь, сейчас ты и сам увидел, что ты малость недопонял, что я тебе говорил?

Смотри, сейчас показал типы, которые в С++ можно было выразить вот так: T*, T**, T*** и т.д.
Да, из этих T***..* можно натуральные числа делать, верное замечание, но это будет детсад, первая четверть и не об этом сейчас речь.

Речь была о том, что в отличие от некоего value-type Nullable<Nullable<...<T>...>>, переменной ссылочного типа можно присвоить просто None (null, NULL, Nil и т.д.) — т.е. присвоить некое значение, НЕ связанное с типом T (а не конструировать значение вот этого страшного типа с длинным именем).

Почему просто null? Потому что это алгебраик — сумма типов.

Дотнет не поддерживает value-type алгебраики, однако, барабанная дробь, тра-та-та-та...
Так почему же C# позволяет писать вот так:

Nullable<int> x = null;

?
Ответ: это хак системы типов сугубо для Nullable<>. Компилятор знает этот тип в лицо (у-у-упс?), т.е. напиши рядом свой аналогичный MyNullable — и будет ошибка компиляции.

В общем, ты там пытался выше наезжать на ссылочные типы, но в дотнете, наоборот, хакают систему типов так, чтобы некий специальный value-тип мимикрировал под ссылочный. Разве не весело? ))


V>>"У дураков мысли сходятся, смотрю" (С)
DM>Верно!

Ну, мне просто понравилось, что в Rust не стали повторять ошибок дотнета.
Я где-то слышал, что Rust разрабатывали укушенные нейтивом, поэтому "мысли сходятся", ы-ы-ы.
Так-то я этот язык не знаю от слова совсем, спасибо за инфу, как грится.