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

V>Ты меня с кем-то путаешь.
V>Я не помню, чтобы ты на Хаскеле мне что-то показывал.
Я тебе это на С++ показывал.

WH>>До этого ты не понимал, что числа в шаблонах С++ это не числа, а типы.
V>Твоё определение чисел в шаблонах (в т.ч. адресов объектов с внешней линковкой) — дилетанское. Это термы-параметры типа времени компиляции, их грамотное название "type-level literals". Cобсно, потому и literals.
Это ты просто не понимаешь, что происходит.
"type-level literals" это литералы, превращённые в типы.
Превратили типы Nat и Symbol в рода, а все их значения в типы.

WH>>Даже по твоей ссылке написано, что "не является зависимой". Я это даже выделил.
V>Никто не утверждал, что в Хаскеле есть зависимые типы изкаробки в виде именно зависимостей от чисел (и прочих термов).
V>Опять споришь с воображаемым собеседником, очевидно.
Но это определение зависимых типов.
Зависимый тип — это тип который зависит от термов.
Это единственное определение зависимых типов. Другого нет.
Всё что ты тут делаешь это споришь с этим определением.

V>Спорь со мной:
V>в задаче требовалось выразить зависимость типа вектора от его длины в рантайм.
V>Из вики "такой выразительностью обычно обладают языки с зависимыми типами".
В вики говорят исключительно про рода типов. Читай внимательно.

С этой точки зрения, запись Vec :: * -> Nat -> * не является зависимой — она означает лишь, что второй параметр вектора должен принадлежать к именованному роду Nat

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

V>Так вот, в системе типов Хаскеля появилось нечто большее, чем простая зависимость типов от типов.
Нет, не появилось.

V>Например, в случае простой зависимости типов от типов можно написать не только F(F(F(T))), но и F(X(Y(Z))).
V>Но Хаскель позволяет описывать рода типов, например, строго такого вида: F(F(F(...
V>https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_guide/promotion.html
Рода типов не делают типы зависимыми.

V>Это позволяет генерировать одну и ту же версию бинарного кода для всех инстансов такого типа. В этом трюк.
Это позволяет выдавать сообщения об ошибках и ничего более.

V>Таким образом, кол-во оперируемых типов в рантайме становится теоретически бесконечно, потому что Хаскель позволяет "расти" типам одного рода в рантайм.
Это бред.

V>Всё, что требовалось для понимания, я уже написал тебе в прошлых сообщениях, но ты всё еще плаваешь.
Нет это ты тупишь.

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

V>Всё? ))
V>А голову включить?
Вот и включи.

V>Вот нахрена надо было вводить такое ограничение? Ради любви к искусству?
Для нормальных сообщений об ошибках.

V>Это для такой фишки, как полиморфизм родов.
Тут нет полиморфизма родов.

V>Ведь параметр Nat по ссылке участвует только в type-level вычислениях и никак не представлен в данных.
V>Отсюда появляется та самая возможность генерирования единственного тела полиморфной ф-ии для для разных инстансов Nat.
1)Для тебя новость что есть типы без значений?
2)Типы у которых нет значений в том же С++ часто используются. Никакого рокетсайнс тут нет.

V>Т.е. нужна возможность объявить некую полимофную рекурсивную ф-ию, в которую можно подать V(n), и которая способна будет вызвать себя же с типом V(n+1). Именно в этом месте компилятор С++ ругается, т.к. происходит неограниченный рост специализации шаблонов в процессе компиляции. В Хаскеле — не происходит, т.к. начинает работать полиморфизм родов.
1)Код в студию.
2)Полиморфизма родов тут нет. У всех типов тут один род Nat.

V>Как "вернуть" затем такой прочитанный типизированный вектор? — через полиморфный же колбэк, который будет вызван по окончании считывания файла.
Ты не звизди. Ты код покажи.
Возьми хаскель и напиши код.

V>Тут самое смешное, что мне очень хорошо понятно, что именно тебе не понятно.
V>Ты ставишь знак равенства м/у системой типов Хаскеля и С++.
Это ты путаешь систему типов с деталями реализации.

V>>>В случае Хаскеля ограничение на "длину" типа будет зависеть только от входных данных в рантайме.
WH>>Бред полный.
V>Шаблон порвало?
Код в студию. Трепло.

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

V>Через род типа можно определить его общее устройство.
V>Через класс типа — список доступных операций над ним.
V>Эти возможности системы типов ортогональны.
Причём тут вообще классы типов?
Иерархия
значение : тип : род : сорт : ...
к классам типов вообще никакого отношения не имеет.

V>И это ортогональные темы: кодогенерация vs некие тонкости целевой прикладной области, для которой используется кодогенерация.
V>Ты пытался объявить коллег виноватыми лишь потому, что они не переключились мгновенно с первого на второе.
V>Круто. Тонкости целевой предметной области — это никого не интересующий оффтоп.
Наоборот. Я обвиняю вас именно в том, что вы переключились с первого на второе. Да ещё и не понимая предмет.
И сделано это было исключительно с целью доказать, что кодогенерация не нужна.

V>Тем более, что там кодогенерация была вовсе необязательна.
V>Через т.н. "селекторы", можно обобщать на шаблонах С++ алгоритм на произвольные по устройству структуры.
А алгоритм Флойда — Уоршелла ты тоже предлагаешь на шаблонах С++ крутить?

V>Ты обиделсо на подобного рода критику и попытался уличить окружающих в непонимании тонкостей целевой прикладной области.
Я просто уличил вас в полной некомпетентности и всё.