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

WH>"type-level literals" это литералы, превращённые в типы.

Это параметры типов прямо по определению.


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

Смотри, ты рядом говорил о том, что ЗТ могут работать с БЕСКОНЕЧНЫМИ значениями величин.
Ты ж именно так на меня капсил. Было? Было.

Предлагаю остановиться именно на этом моменте, бо он ключевой. Остальное — лирика.

Итак.

Во-первых, твоя формулировка как обычно не верная. Пример работы ЗТ над bool или любым ограниченным в значениях типом (char, short и т.д.) — тому доказательство.

В-вторых, компилятор с языка с ЗТ производит операцию дедукции над значениями и тут зависит от того, научили ли разработчики компилятора его дедукции над каким-то типом значений или нет. Т.е., если среди встроенных типов нет, скажем, некоего BigInt для представления произвольно большого числа, то и рассуждения сразу неверные.

В третьих, рассуждения твои, тем не менее, близки к истине, но как обычно ты ходишь кругами вокруг сути, не умея попасть в яблочко. Самая главная фишка ЗТ — это работать с произвольным, т.е. потенциально бесконечным кол-вом ТИПОВ в рантайм.

Например, простая структура из десятка обычных int способна представить фактически бесконечное кол-во значений с т.з. любой современной вычислительной системы.

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

Арифметика Пеано считает на палочках, поэтому не всегда удобна.

Например, возьми тупл параметров типа некоей длины: (BoolTag, BoolTag, BoolTag, ...) — и вот получишь поразрядное кодирование.
Именно такие вещи сейчас активно изучаются хаскелистами — сейчас модно обсуждать type-level вычисления на синглтонах и даже есть соответствующие фреймворки на Хаскеле.

По-прежнему "неудобно", ес-но, но описанные задачи решает.

Потому что твоё определение зависимых типов верно только в терминах классификации лямбда-куба, где сам лямбда-куб — лишь одна из классификаций.
https://en.wikipedia.org/wiki/Pure_type_system

Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy.

Теория чистых систем типов[en] (англ. pure type systems, PTS) обобщает все исчисления лямбда-куба и формулирует правила, позволяющие вычислить их как частные случаи. Её независимо построили Берарди (Berardi) и Терлоу (Terlouw). Чистые системы типов оперируют только понятием типа, рассматривая все понятия других исчислений только в виде типов — потому они и называются «чистыми». Не производится разделения между термами и типами, ...

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

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

Для начала, в Хаскеле через -> обозначается не только функциональная зависимость, но и зависимость м/у типами (на всяк случай для читателей).

Далее. Запись "Vec :: * -> Nat -> *" означает ограничения на "сигнатуру" конструктора параметрического типа. "Сигнатура" в кавычках, потому что используется как аналог/демонстрация из мира сигнатур функциональных типов.

Конструирование параметрического типа — это присвоение типовым переменным конкретных типов, здесь мы на эту операцию вводим ограничения.
Писал уже:

Через род типа можно определить его общее устройство.

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

ЧТД.
Не понимаешь.


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

При том, что твоя классификация — неполная, неверная и не отражает сути обсуждаемого.
Сорта типов нас вообще не интересует.
Потому что, для примера, сорт функциональных типов никак не пересекается с сортом "обычных" типов.
Точно так же как сорт типа поля (как пример — указатель на мембер в С++) — тоже никак не пересекается с обычными типами (обычными указателями в С++).

Т.е., ты построил иерархию, но в Хаскеле нет такой иерархии, в этом языке любые расширения мономорфных типов (независимо от их сорта) ортогональны друг другу и каждое из них (расширений) образует ровно один уровень, безо-всяких иерархий.

Про Хаскель так и говорится — это ортогональный язык.

Классы типов служат для параметрического полиморфизма, т.е. объединяют типы в группы по реализуемым над ними операциям.
Классы типов с удовольствием работают над обычными типами (алгебраическими), функциональными и т.д. — т.е. любых сортов.

Роды типов служат для структурного полиморфизма, т.е. объединяют типы в группы по способу конструирования типов.
Точно так же замечательно работают над любыми сортами и их комбинациями, если у конструктора типа более одного параметра.

Т.е. эти вещи работают как совместно, так и независимо и им плевать друг на друга.


WH>Иерархия
WH>значение : тип : род : сорт : ...
WH>к классам типов вообще никакого отношения не имеет.

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

Предметная область там была — НЕКИЕ формулы вычислений.
Например, у твоего альфа-бленда есть пару сотен алгоритмов наложения (из исходного базиса):
http://www.gamedev.ru/code/terms/Blending

Поэтому, на конкретные формулы плевать с большой колокольни.


WH>И сделано это было исключительно с целью доказать, что кодогенерация не нужна.

Т.е., замени одну формулу на другую и ДЕЙСТВИТЕЛЬНО станет не нужна???
Ты хоть сейчас понял что ты сказал?

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

Вот тут я верно твою проблематику расписал:
http://www.rsdn.org/forum/philosophy/6708663.1
Да/нет?


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

Пытаешься повторить тот же трюк? У меня уже рука устала тянуться к лицу. ))

Я предлагал крутить на шаблонах формулы вполне конкретного вида.
Да, в семантику этих формул не вникал, бо целевым в них было — возможность обобщения вычислений на разные способы кодировки цвета.
Это всё, что обсуждалось.
Остальное — злостный офтоп.


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

Ага, как у меня сейчас насчет алгоритма Флойда — Уоршелла.
Вот я в нем жутко некомпетентный на прямо сейчас.
Уличил так уличил...

=========
Кароч, тут ведь возможен не только тот вариант, что ты НЕ УМЕЕШЬ формулировать свои мысли, не?
А может ты прекрасно умеешь, но специально не формулируешь, в надежде "половить" там кого-то, когда тебя самого к стенке прижмут, ы?
Ну вот тебе показали, что твой пример кодогенерации нелеп, потому что она там не требовалась.
Тебе там нечего было на это ответить.
Т.е., может ты специально так делаешь, чтобы иметь возможность перевести стрелки, вместо ответа на прямые вопросы по-существу?
Чувствуешь, чем это попахивает?
Это г-но манеры, вот что это.
Предполагая, что у тебя просто каша в голове и ты мечешься вправо-влево не специально, я делаю тебе ба-а-а-альшое одолжение, фактически оправдываю твои нечистоплотные манеры рассеяностью внимания. Но вот я уже не уверен, что дело в рассеянности.