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

V>>Пока что очевидно только то, что ты так и не понял работу этого трюка. ))
WH>Это я показал тебе этот трюк.

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


WH>До этого ты не понимал, что числа в шаблонах С++ это не числа, а типы.

Твоё определение чисел в шаблонах (в т.ч. адресов объектов с внешней линковкой) — дилетанское. Это термы-параметры типа времени компиляции, их грамотное название "type-level literals". Cобсно, потому и literals.

В GHC есть соответствующее расширение:
https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_guide/type-level-literals.html

Их строковый Symbol смущать не должен — точно так же можно задать строку с внешней линковкой в С++ и пользовать указатель на её как параметр шаблона.

В общем, это расширение HGC не добавляет ничего нового в сравнении с константами в шаблонах С++, т.е. это сугубо статическая хрень.
Т.е., как с тем order в С++, для всех используемых значений зависящие от них типы надо "сгенерить" статически:
https://habrahabr.ru/post/253157/

Поэтому, речь НЕ о числах в шаблоне.


WH>Даже по твоей ссылке написано, что "не является зависимой". Я это даже выделил.

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

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

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

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

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


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

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


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

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

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

Да еще обвиняешь окружающих в этом. ))


WH>

WH>а значит, могут быть любым конкретным типом. Иначе говоря, здесь не запрещаются бессмысленные ти?повые выражения вроде Succ Bool или Vec Zero Int.

Тут верно.


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

Всё? ))
А голову включить?
Вот нахрена надо было вводить такое ограничение? Ради любви к искусству?
Это для такой фишки, как полиморфизм родов.
Ведь параметр Nat по ссылке участвует только в type-level вычислениях и никак не представлен в данных.
Отсюда появляется та самая возможность генерирования единственного тела полиморфной ф-ии для для разных инстансов Nat.


WH>Ты можешь зять вектор длинны N и получить вектор длинны N + 1. Но только при условии, что N известно на этапе компиляции.

На этапе компиляции достаточно, чтобы был известен только тип V(0) и однозначный способ построения в рантайме типа вектора V(n+1) из любого текущего V(n).

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

Итого, прочитал из файла символ, сформировал новое значение нового типа V(n+1), вызвал опять же себя рекурсивно.
Я думаю, ты же помнишь, что в Хаскеле циклы делаются через рекурсии? ))

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

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


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

Тут самое смешное, что мне очень хорошо понятно, что именно тебе не понятно.
Ты ставишь знак равенства м/у системой типов Хаскеля и С++.
В то время как даже просто параметрический полиморфизм у них работает по-разному: в С++ происходит инстанс уникального бинарного кода для каждой специализации шаблона (т.е. происходит кодогенерация), а в Хаскель работает т.н. "истинный полиморфизм" (как они сами говорят), когда физически может исполняться один и тот же код для разных типов, заданных классом типов.

Аналог происходящего в этом случае в Хаскеле — это полиморфизм подтипов в ООП, примерно так (С++):

struct Base {
    virtual void foo() = 0;
};

void callFoo(Base * obj) {
  obj->foo();
}

Тело метода callFoo будет единственным для любого obj.

Думаю, в этом месте должно стать кристально ясно, зачем в Хаскеле алгебраики представлены ссылочными типами.


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

Шаблон порвало?


WH>Покажи мне код на хаскеле который это делает.
WH>Вот код на Dafny я показать могу. А на хаскеле ты это не сделаешь.

Ну, у первой версии Agda зависимые типы реализовались так же как в Хаскеле с обсуждаемым расширением, т.е. вовсе не как в Dafny, а тоже через трюки Пеано.


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

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

WH>Вот это код на Dafny.

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


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

Дык, на синтаксис Dafny никто и не претендовал.
Понятно, что в явном виде "понятнее человеку", ы-ы-ы много раз.

Соответствующее расширение Хаскеля готовится к 2018-му году, т.е. поддержка зависимых типов явным образом.
Это будет лишь расширение полиморфизма родов на type-level literals. Опять ву а ля.


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

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


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

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

Тем более, что там кодогенерация была вовсе необязательна.
Через т.н. "селекторы", можно обобщать на шаблонах С++ алгоритм на произвольные по устройству структуры.
Ты обиделсо на подобного рода критику и попытался уличить окружающих в непонимании тонкостей целевой прикладной области.
Классика перевода стрелок, однако.
Да нас-ть на все эти тонкости с большой колокольни, скажем прямо. Там примитивщина в любом случае.


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

Ну ты этим постом опять и снова показал такую же неадекватность.
Несерьёзно всё это...