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

V>Мде...
V>Пока что очевидно только то, что ты так и не понял работу этого трюка. ))
Ох.
Это я показал тебе этот трюк. До этого ты не понимал, что числа в шаблонах С++ это не числа, а типы.
Даже по твоей ссылке написано, что "не является зависимой". Я это даже выделил.
Но ты продолжаешь это твердить.

V>Ну конечно, в системе типов Хаскеля зависимых типов нет.
V>Но зато в Хаскеле есть зависимость типов от типов.
V>На этой зависимости с помощью арифметики Пеано и такой-то матери представляются натуральные числа.
Ох. Зависимый тип — это такой тип, который зависит от значений времени исполнения.

V>Вот D.Mon тоже (зачем-то) упомянул этот трюк:
V>

V>F(F(F(T))) = T + 3
V>В частности, если T = 1, то F(F(T)) = 1 + 1 + 1 = 3, т.е. тип с тремя разными возможными значениями. Так из Option можно натуральные числа делать.

Да ты вообще не понял, что тут написано. К данному разговору это вообще отношения не имеет.

V>С помощью этого трюка они на Хаскеле решают именно такие задачи, которые можно решать только на языках с ЗТ:
V>

V>Но обычно такой выразительностью обладают лишь системы с зависимыми типами, реализованные в таких языках, как Agda, Coq и др.

V>Например, на стандартном ML такое не выразить.
Ты даже не понял к чему эта фраза. А она вот к этому:

Решение условно предполагает, что фантомный тип n будет использоваться для моделирования целочисленного параметра вектора на основе аксиом Пеано — то есть будут строиться только такие выражения, как Succ Zero, Succ Succ Zero, Succ Succ Succ Zero и т. д. Однако, хотя определения записаны на языке типов, сами по себе они сформулированы бестиповым образом. Это видно по сигнатуре Vec :: * -> * -> *, означающей, что конкретные типы, передаваемые в качестве параметров, принадлежат роду *, а значит, могут быть любым конкретным типом. Иначе говоря, здесь не запрещаются бессмысленные ти?повые выражения вроде Succ Bool или Vec Zero Int.[83]

Всё что делает это расширение это запрещает писать Succ Bool, Vec Zero Int и подобные бессмысленные типы. Всё.

V>Вот как раз самый простой пример — длину вектора проверять НЕ надо, бо она зашита в тип.
V>Т.е. тип вектора зависит от его длины, но в рантайме работает один и тот же код, независимо от длины вектора.
Ох. Ну попробуй прочитать длину вектора из консоли. И создай вектор этой длинны.
Ты не сможешь. Ибо данное расширение не добавляет в язык зависимые типы.

WH>>Они значения превращают в типы, а тип превращают в род (тип типов).
V>Сама программа строится так, что по мере добавления элементов в вектор его тип меняется.
Но она всё равно не зависит от значений времени исполнения.
Ты можешь зять вектор длинны N и получить вектор длинны N + 1. Но только при условии, что N известно на этапе компиляции.

WH>>То же самое делает компилятор С++ для целых чисел.
V>Компилятор С++ для рантайма должен будет сгенерить код для каждого инстанса типа из шаблона.
V>Однако, когда компилятор встречает неограниченную генерацию для рантайма из шаблонного кода, он ругается и отказывается работать.
Так и у хаскеля тоже количество вариантов ограничено статически.

V>В случае Хаскеля ограничение на "длину" типа будет зависеть только от входных данных в рантайме.
Бред полный. Покажи мне код на хаскеле который это делает.
Вот код на Dafny я показать могу. А на хаскеле ты это не сделаешь.
Ибо нет там зависимых типов.

V>В стандартном ML система типов на лямбда кубе — это термы, зависимые от типов и типы, зависимые от типов.
А зависимые типы — это типы которые зависят от термов.
Все остальные типы зависимыми не являются. Просто по определению. А что ты там себе нафантазировал никому не интересно.

method SelectionSortRange(a : array<int>, begin : int, end : int)
  requires 0 <= begin <= end <= a.Length;

Вот это код на Dafny.
Множество значений, которое может принимать begin зависит от значения end и размера массива.
Множество значений, которое может принимать end зависит от значения begin и размера массива.
Именно зависимость от значений времени исполнения делает типы begin и end зависимыми.

Синтаксически зависимость прописана не в типе, а рядом просто по тому что так нагляднее и понятнее человеку.

V>Так вот. Допиливание системы типов Хаскеля позволило организовывать типы в счётные м-но внутри эдаких "родов".
V>И "пересчитывать" их. Вот так: раз, два, три, четыре...
Отношение между родом и типом такое же как между типом и термом.
Тип — это именованное множество термов.
Род — это именованное множество типов.
Сорт — это именованное множество родов.
И так далее до бесконечности.

V>Кароч, я так думаю, что ты хотя бы приблизительно понял о чем речь, а если напряжешься хотя бы минут на 15 поймёшь окончательно.
Я всё точно понял и уже давно. А ты так до сих пор ничего и не понял.

WH>>Нет. Это вы с гапертоном офтопить начали.
WH>>Разговор был про генерацию кода. Я показал пример генерации кода для преобразования цветов между различными цветовыми пространствами.
WH>>И понеслось...
V>Так тем более пофик на альфу, если кодогенерация.
Так зачем вы с гапертоном начали меня учить? Причем тому что не имеет отношения к реальности?

V>Обделался тот, кто включил неадеквата, ес-но.
То есть вы с гапертоном.