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

WH>>Теперь если у нас есть обобщённый код который работает с хештаблицей и в него передадут Hashtable<int, Option<string>> то без этой фичи код не будет знать есть элемент или в таблице лежит None.
WH>>Из-за этого алгоритм может сломаться.
A>всё так, но только подобную семантику нужно выражать явно, а для этого просто нужен тип, который явно хранит информацию об ошибке, а-ля предлагаемого для C++ std::expected, и в случае ошибки строить логику вокруг именно инстанса ошибки, а не вокруг нагруженного лишними смыслами optional
Тут вообще не идёт речь об ошибках. Вообще не понимаю откуда ты это взял.

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

WH>>>Но похоже ничего кроме трёпа от него так и не будет. Видимо показывать просто нечего.
V>>Показываю.
WH>Опять исключительно трёп.

Борзеем...


WH>Код где?

Тебе кто-то обещал выложить публично код из проекта?
Бредить изволим?
Выложи сюда исходный код Решарпера++.

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

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

#define int_c(x) [v=int(x)]{return v;} //макрос только для красоты, а не как необходимое средство

int n;
cin>>n;//читаем длину из консоли
auto size=int_c(n);//вот наш особое значение-тип
auto v1=make_my_vector(size);//параметризуем наш вектор этим значением-типом
auto v2=make_my_vector(size);
auto size2=int_c(n+1);
auto v3=make_my_vector(size2);

У v1 и v2 будут одинаковые типы, а у v3 другой.

P.S. Я этим самым не пытаюсь доказать, что в C++ есть нормальные зависимые типы. Но очень многие задачи из данной области тривиально решаются и подобными инструментами. )

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

WH>Тут вообще не идёт речь об ошибках. Вообще не понимаю откуда ты это взял.
я на самом деле тут задумался, ты опять впадаешь в демагогию или правда можешь понять почему expected это обобщение optional. Если первое — то это печально, но ожидаемо, а если второе, то всё очень печально

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

WH>>Тут вообще не идёт речь об ошибках. Вообще не понимаю откуда ты это взял.
A>я на самом деле тут задумался, ты опять впадаешь в демагогию или правда можешь понять почему expected это обобщение optional. Если первое — то это печально, но ожидаемо, а если второе, то всё очень печально
Печально тут то что ты не можешь понять, что отсутствие значения в optional это не ошибка.
expected это не обобщение optional. Это два разных типа для разных ситуаций. И они оба нужны.

optional используется, когда отсутствие значения нормальная рабочая ситуация.
Нет значения в словаре. Пользователь не заполнил опциональное поле в форме итп.

Исключения и expected который должен использоваться только для перехвата исключений, а не сам по себе, должны использоваться для обработки ожидаемых, но редких сбоев типа проблем с сетью.

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

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

WH>>Опять исключительно трёп.
V>Борзеем...
А как ещё с треплом разговаривать?

V>Тебе кто-то обещал выложить публично код из проекта?
V>Бредить изволим?
Покажи мне любой код GLR парсера который соответствует твоим обещаниям.
Можешь написать (там же по твоим утверждениям всё очень просто) или найти уже кем-то написанный. Мне всё равно.
По тому что пока не будет кода, соответствующего твоим обещаниям ты будешь треплом.

V>Выложи сюда исходный код Решарпера++.
А это тут вообще причем? Я код этого проекта только на мониторах разработчиков видел.

Здравствуйте, 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>То есть вы с гапертоном.

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

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

VD>Для варианта с ValueOption предупреждение будет:
VD>

VD>warning : matching is not exhaustive, example unmatched value: (HasValue = (false, false))

ок


VD>Кстати, я тут пока с тобой общался немного подумал и допилил напильником макро-оператор ??. Теперь он поддерживает не конкретные типы, а в том числе любой тип реализующий идиому HasValue/Value. Так что оператор ?? теперь можно использовать для ValueOption:
VD>

VD>WriteLine(VSome(42) ?? -1);
VD>WriteLine(VNone() ?? -1);
VD>

Продолжая эту идею, для любого типа можно было бы определить (схематично):

[NullWhen(NotSet)]
enum Color {
  NotSet
  Red, 
  Yellow, 
  Green 
}

[NullWhen(NullableFoo(-1))]
struct NullableFoo {
  value : int;
}

// или
[NullWhen(value = -1)]
struct NullableFoo2 {
  value : int;
}

Здравствуйте, 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>Ты обиделсо на подобного рода критику и попытался уличить окружающих в непонимании тонкостей целевой прикладной области.
Я просто уличил вас в полной некомпетентности и всё.

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

V>Продолжая эту идею, для любого типа можно было бы определить (схематично):...

Это можно сделать отдельным макросом. Вопрос только насколько это нужно.

Там и вручную то не много работы:
http://rsdn.org/forum/nemerle/6710594.1

Автор: VladD2
Дата: 28.02.17

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

WH>>>Опять исключительно трёп.
V>>Борзеем...
WH>А как ещё с треплом разговаривать?

Трепло тут ты, еще и недогоняющее элементарнейших вещей. ))

Ты НЕ МОЖЕШЬ требовать у меня аргументов до тех пор, пока у тебя не будет своих, опровергающих.
Собсно, ты ни у кого не можешь требовать аргументов в таком стиле, потому на прямо сейчас мне НЕ НА ЧТО аргументировать.
Zero, у тебя ноль инфы, за которую мне надо было бы "бороться".

Вот если бы у тебя был код парсера LR(0), и ты бы получил совершенно ПРОТИВОПОЛОЖНЫЕ результаты от озвученного мною — тогда ОК, еще было бы о чем с тобой разговаривать.

А пока ходи мимо, бо выглядишь как любитель халявы. ))


V>>Тебе кто-то обещал выложить публично код из проекта?
V>>Бредить изволим?
WH>Покажи мне любой код GLR парсера который соответствует твоим обещаниям.

Э, нет, возьми готовый код LR(0) или напиши сам — и тогда тебе будет что возразить по-существу или согласиться.
Я же не могу спорить с самим собой, верно? Ведь тебя в споре нет, ты на позициях не спорящего, а просящего, еще и злящегося, что бесплатно не подают. ))


WH>Можешь написать (там же по твоим утверждениям всё очень просто) или найти уже кем-то написанный. Мне всё равно.

Ну так можешь написать или найти уже кем-то написанный аналог решарпера, мне всё-равно ))


WH>По тому что пока не будет кода, соответствующего твоим обещаниям ты будешь треплом.

Это твои личные половые трудности.
По моим утверждениям "все просто" для понимания работы LR(0), т.е. почему он работает на уровне лексера. Т.е. я считаю, что это на порядки проще для понимания чем ПЕГ/Пакрат и твоё упорство тут — лишь демонстрация лени ума. Тебе надо на блюдечке с каёмочкой.


V>>Выложи сюда исходный код Решарпера++.
WH>А это тут вообще причем? Я код этого проекта только на мониторах разработчиков видел.

Ну, у меня конкретно в моей реализации слишком много чего прибито гвоздями друг к другу.

Например, в стеке разбора не хранятся абстрактные коды нетерминалов, хранятся сразу данные, операция свертки стека линкует эти данные, а не вызывает некий колбэк (обязательно виртуальный и жутко тяжеловесный) для построения некоего абстрактного АST (еще более тяжеловесная хрень).

И еще куча трюков.
Главный трюк я тебе уже озвучил — на однозначных цепочках получил эффективность обычного LR(0).
Показать этот трюк? Не уверен. Словами описал, умный человек сможет повторить, если захочет. А для остальных любителей халявы выкладывать наработки из коммерческого проекта... таки не уверен ни разу. Тема-то очень специфичная, тут на всём сайте понимающих на пальцах одной руки пересчитать можно.

В общем, прямо отсюда ты или смотришь внимательно на LR(0) или завязываем тему, бо надоел своей беспредметностью.

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

VD>Там и вручную то не много работы

Для структуры согласен, а для enum?
NotSet — это часто используемая идиома.

Здравствуйте, 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>Я просто уличил вас в полной некомпетентности и всё.

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

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

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

V>Для структуры согласен, а для enum?

Для него ничего не надо делать. У меня ни разу такое желание не возникало.

Вообще, исходить надо из практической целесообразности. Вот чувствуешь ты неудобство от чего-то — это надо пофиксить, а не чувствуешь — не надо.

V>NotSet — это часто используемая идиома.

Дык option/ValueOption/nulable же есть (последний нужен только для совместимости). Они 99% случаев покрывают. А это уже оптимизации.

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

V>Ты НЕ МОЖЕШЬ требовать у меня аргументов до тех пор, пока у тебя не будет своих, опровергающих.
1)Доказывать должен тот, кто утверждает. То есть ты.
2)Твои утверждения противоречат ВСЕМ работам по GLR которые я видел.

V>Вот если бы у тебя был код парсера LR(0), и ты бы получил совершенно ПРОТИВОПОЛОЖНЫЕ результаты от озвученного мною — тогда ОК, еще было бы о чем с тобой разговаривать.
Причём тут LR(0)? Разговор про GLR.

Короче трепло как оно есть.

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

WH>>"type-level literals" это литералы, превращённые в типы.
V>Это параметры типов прямо по определению.

Numeric literals are of kind Nat, while string literals are of kind Symbol. This feature is enabled by the XDataKinds language extension.

Род(kind) это множество типов. Прямо по определению.
Те значения рода — это типы прямо по определению.

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

WH>>Наоборот. Я обвиняю вас именно в том, что вы переключились с первого на второе. Да ещё и не понимая предмет.
V>Предметная область там была — НЕКИЕ формулы вычислений.
Разговор был про генерацию кода. Я показал зачем мне она нужна.
Вы на пару с гапертоном попытались выставить меня некомпетентным. Но сами обосрались.

V>Например, у твоего альфа-бленда есть пару сотен алгоритмов наложения (из исходного базиса):
V>http://www.gamedev.ru/code/terms/Blending
Ой блин... Это вообще к делу не относится.

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

Короче трепло как оно есть.

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

WH>Код на хаскеле который читает с консоли число и создаёт вектор тип которого зависит этого числа в студию.

Извините, что встреваю в вашу цивилизованную ученую дискуссию, но такой код как раз несложно пишется:

{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies #-}
module Main where

-- натуральные числа по Пеано
data Nat = Z | S Nat deriving (Show, Eq, Ord)

-- вектор, индексированный натуральной длиной
data Vec :: Nat -> * -> * where
   V0    ::                  Vec Z x
   (:>)  :: x -> Vec n x ->  Vec (S n) x

infixr 5 :>

-- это к задаче не относится, но чисто ради фана сделаем сложение чисел и конкатенацию векторов
type family (m :: Nat) :+ (n :: Nat) :: Nat
type instance  Z    :+  n  =  n
type instance  S m  :+  n  =  S (m :+ n)

vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
vappend  V0         ys  =  ys
vappend  (x :> xs)  ys  =  x :> vappend xs ys

toList :: Vec n a -> [a]
toList V0 = []
toList (x :> xs) = x : toList xs

-- семейство синглтон типов: по одному рантайм-значению для каждого типового натурального числа
data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

-- сделать вектор заданной длины
makeVec :: Natty n -> a -> Vec n a
makeVec Zy _ = V0
makeVec (Sy k) x = x :> makeVec k x

-- тут самая мякотка: получаем рантайм значение, делаем вектор такой длины и показываем
test :: Int -> IO ()
test n = loop n Zy where   -- цикл нужен, чтобы получить натуральное число из инта
  loop :: Int -> Natty m -> IO ()
  loop 0 m = print $ toList $ makeVec m 7
  loop k m = loop (k-1) (Sy m)

--запрашиваем число из консоли, показываем вектор из указанного пользователем количества семерок
main :: IO ()
main = do
  putStrLn "enter n:"
  nstr <- getLine   
  test $ read nstr

enter n:
5
[7,7,7,7,7]

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

WH>>Код на хаскеле который читает с консоли число и создаёт вектор тип которого зависит этого числа в студию.
DM>Извините, что встреваю в вашу цивилизованную ученую дискуссию, но такой код как раз несложно пишется:
1)Ты очень вольно интерпретируешь слово зависит.
Тип Vec не параметризуется терминалом. А значит зависимым не является просто по определению.
Nat в данном случае поднимается на уровень рода, а его значения на уровень типа.

2)Попробуй вернуть этот вектор в функцию main таким образом, чтобы тип сохранился.

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

WH>>>Код на хаскеле который читает с консоли число и создаёт вектор тип которого зависит этого числа в студию.
DM>>Извините, что встреваю в вашу цивилизованную ученую дискуссию, но такой код как раз несложно пишется:
WH>1)Ты очень вольно интерпретируешь слово зависит.
WH>Тип Vec не параметризуется терминалом. А значит зависимым не является просто по определению.
WH>Nat в данном случае поднимается на уровень рода, а его значения на уровень типа.

Терминалом?
Все так, и при этом: длина вектора закодирована в типе, вектор таки создается той длины, что дана в рантайм-значении, полученным из консоли. Зависимость реализована опосредованно, через третий тип, "соединяющий" соответствующие термы и типы. Это трюк, о котором vdimas и говорил. И да, это не зависимые типы. Это демонстрация того полиморфизма, позволяющего не знать все значения тайп-левел чисел во время компиляции.

WH>2)Попробуй вернуть этот вектор в функцию main таким образом, чтобы тип сохранился.

Не умею.

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

WH>>2)Попробуй вернуть этот вектор в функцию main таким образом, чтобы тип сохранился.
DM>Не умею.
А зависимые типы умеют.