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

V>>Ну, хаскелисты утверждают, что такими св-вами обладают лишь языки с ЗТ.
WH>

WH>В 2012 году было построено[83] расширение языка Haskell, реализующее более развитую систему родо?в и делающее вышеприведённый код корректным кодом на Хаскеле. Решение состоит в том, что все типы (за определёнными ограничениями) автоматически «продвигаются» (англ. promote) на уровень выше, формируя одноимённые рода?, которые можно использовать явным образом. С этой точки зрения, запись Vec :: * -> Nat -> * не является зависимой — она означает лишь, что второй параметр вектора должен принадлежать к именованному роду Nat, а в данном случае единственным элементом этого рода является одноимённый тип.

WH>Ты даже один абзац текста понять не можешь. Да ещё и фигурно его порезал. И после этого ещё имеешь наглость обвинять меня в нечистоплотности.

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

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

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

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

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

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

Например, на стандартном ML такое не выразить.

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


WH>Они значения превращают в типы, а тип превращают в род (тип типов).

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


WH>То же самое делает компилятор С++ для целых чисел.

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

В случае Хаскеля ограничение на "длину" типа будет зависеть только от входных данных в рантайме.
В случае аналогичного трюка для вычислений времени компиляции на шаблонах С++ — от неких поданных и закодированных в кач-ве параметра шаблона эдаких "внешних" (по отношению к шаблону) данных.


WH>Короче теорию типов ты не знаешь от слова совсем.

Уже ломашься как девочка. ))

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

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

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

Считай, вот только сейчас у тебя появились первые слабые проблески насчёт того, о чем шла речь. ))


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

Так тем более пофик на альфу, если кодогенерация.


WH>Гапертон начал учить меня преобразовывать RGB <-> sRGB (нелинейное преобразование) при помощи матриц.
WH>Ты начал утверждать, что каналы независимы после того как я тебе показал, что бывает, когда работать с каналами независимо ты начал петь про фильтры.

Так ты нашел тот топик или нет?


WH>В общем тогда вы оба неслабо обделались.

Обделался тот, кто включил неадеквата, ес-но.
Это всё было вовсе не рокет саенс, а скорее ровно наоборот.
Сформулировал бы ты свой аргумент членораздельно — сходу получил бы от меня плюсик.
Перидически я тебя плюсую, если заметил...

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

V>>Ну, хаскелисты утверждают, что такими св-вами обладают лишь языки с ЗТ.
WH>

WH>В 2012 году было построено[83] расширение языка Haskell, реализующее более развитую систему родо?в и делающее вышеприведённый код корректным кодом на Хаскеле. Решение состоит в том, что все типы (за определёнными ограничениями) автоматически «продвигаются» (англ. promote) на уровень выше, формируя одноимённые рода?, которые можно использовать явным образом. С этой точки зрения, запись Vec :: * -> Nat -> * не является зависимой — она означает лишь, что второй параметр вектора должен принадлежать к именованному роду Nat, а в данном случае единственным элементом этого рода является одноимённый тип.

WH>Ты даже один абзац текста понять не можешь. Да ещё и фигурно его порезал. И после этого ещё имеешь наглость обвинять меня в нечистоплотности.

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

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

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

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

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

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

Например, на стандартном ML такое не выразить.

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


WH>Они значения превращают в типы, а тип превращают в род (тип типов).

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


WH>То же самое делает компилятор С++ для целых чисел.

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

В случае Хаскеля ограничение на "длину" типа будет зависеть только от входных данных в рантайме.
В случае аналогичного трюка для вычислений времени компиляции на шаблонах С++ — от неких поданных и закодированных в кач-ве параметра шаблона эдаких "внешних" (по отношению к шаблону) данных.


WH>Короче теорию типов ты не знаешь от слова совсем.

Уже ломашься как девочка. ))

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

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

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

Считай, вот только сейчас у тебя появились первые слабые проблески насчёт того, о чем шла речь. ))


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

Так тем более пофик на альфу, если кодогенерация.


WH>Гапертон начал учить меня преобразовывать RGB <-> sRGB (нелинейное преобразование) при помощи матриц.
WH>Ты начал утверждать, что каналы независимы после того как я тебе показал, что бывает, когда работать с каналами независимо ты начал петь про фильтры.

Так ты нашел тот топик или нет?


WH>В общем тогда вы оба неслабо обделались.

Обделался тот, кто включил неадеквата, ес-но.
Это всё было вовсе не рокет саенс, а скорее ровно наоборот.
Сформулировал бы ты свой аргумент членораздельно — сходу получил бы от меня плюсик.
Перидически я тебя плюсую, если заметил...