Re[26]: Мифический Haskell
От: vdimas Россия  
Дата: 23.03.12 21:07
Оценка:
Здравствуйте, Klapaucius, Вы писали:

K>Это разные идентификаторы. Они в разных пространствах имен и могут поэтому совпадать.


В каких разных? Продемонстрируй плиз разные пространства имен для конструктора АлгТД и для одноименного идентификатора метки типа в конструкции ПМ некоего значения, созданного с помощью этого конструктора.


V>>Еще раз — курить Алгебраические типы


K>Курим:

K>

K>Алгебраический тип данных — в теории программирования любой тип, значения которого являются значениями некоторых иных типов, «обёрнутыми» конструкторами алгебраического типа.

K>Т.е. все как я и сказал. Никакие типы в АлгТД не упаковываются. Упаковываются значения.

Эээ... колега, а что вообще могло бы означать "упаковка другого типа" для АлгТД? Можно мне поинтересоваться, что другое ты мог подумать? Как ты себе представляешь упаковку самих типов, а не их значений в системе, где описательная информация о типах недоступна?

Вот фраза, вызвавшая сложность в понимании:

Матчинг АлгТД в Хаскеле аналогично проверяет в рантайм дискриминатор объединения, то бишь запакованный тип.


А если так перефразировать:
Матчинг АлгТД в Хаскеле аналогично проверяет в рантайм дискриминатор объединения, то бишь тип запакованного значения.

(По моему ИМХО, одно упоминание АлгТД подразумевает все связанные с этим детали, которые не обязательно повторять в каждом предложении.)


K>Ну, может и можно сказать, что конструктор типа "упаковывает" типа по аналогии с тем, как конструктор "упаковывает" значение. Вот только конструкторы типов в рантайме не матчатся (в рантайме их нет).


А как конструкторы могут матчиться? Ведь конструктор — это ф-ия. Может матчиться лишь некое ID размеченного объединения, то бишь матч всегда идет по ЗНАЧЕНИЮ, в данном случае это значение метки типа. Т.е. можно сказать, что идет матч по типу завернутого значения.


V>>Похоже, та специфика минималистичности Хаскеля, что одновременно с объявлением АлгТД объявляется (вводится) мн-во оборачиваемых им типов-туплов, совершенно сбивает тебя с толку.

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

Угу, ты повторно налегаешь на подтипирование, хотя я его не упоминал. Я догадываюсь, что ты намекаешь на реализацию наподобие АлгТД в Немерле, но я-то здесь при чем?

Размеченное объединение обязательно хранит метку обернутого в АлгТД типа. Почему именно типа? Потому что согласно определения, размеченное объединение хранит в себе не только сам элемент, но обязательно некий уникальный идентификатор мн-ва, к которому принадлежит хранимый элемент. Мн-во — это тип, элемент мн-ва — это значение типа.

data List a = Nil | Cons a (List a)

Для значения дескриминатора Nil_tag хранится tuple(/*empty*/), для значения Cons_tag хранится tuple(a, List<a>). Оба тупла и есть хранимые значения. Но сии значения-туплы имеют тип, как ни крути. Теперь перечитай ту фразу еще раз:

Похоже, та специфика минималистичности Хаскеля, что одновременно с объявлением АлгТД объявляется (вводится) мн-во оборачиваемых им типов-туплов, совершенно сбивает тебя с толку.

Я теперь более чем уверен, что это именно так.

И да, от техники подтипирования в том же Немерле такая схема по-сути не отличается. Хоть ты и додумал за меня малость, насчет подтипирования, но происходящие в обоих случаях проверки типов при паттерн-матчинге — это суть проверки значения некоей метки. Вся разница лишь в том, что в Хаскеле метка представлена "унутре" интегральным значением, а в Немерле — адресом (сылкой) на дескриптор типа. По идее, тоже интегральным значением (адреса).


K>Ну так boost::variant это не сумма, а объединение — чего вы от него хотите. variant< int, bool > это int или bool.


Не так, это еще хранимый признак типа, как и положено. Поэтому это или container<0, int> или container<1, bool>. Т.е. в плане хранения — дотягивают. Они недотягивают в момент диспетчеризации по конкретным хранимым типам, бо для одного и того же типа будет вызвана одна и та же ветка диспетчеризации, хотя их контейнер имел разные типы, например для случая variant<int, bool, int> будет вызвана одна и та же ветка диспетчеризации в клиентском коде для container<0, int> и для container<2, int> с аргументом просто int, т.е. эти случаи будут неразличимы. Жаль. Было бы неплохо генерить ошибку компиляции для случая одинаковых типов.


K>С суммами все иначе: Either Int Bool не является ни Int ни Bool.


Как я только что показал — вовсе не иначе. Проблема в сценариях и гарантиях. Хотя, проблему нетипизированного union они решили.


K>Поэтому variant не "недотягивает" до АлгТД — это вовсем другая штука со своими достоинствами и недостатками и слабопересекающейся с АлгТД областью применения.


Ну как раз область применения пересекается нормально. Особенно для случая уникальных типов в варианте. И особенно в случае boost::make_recursive_variant — как раз под такие же сценарии.


K>Одно непонятно: зачем так фиксироваться на суммах? В описываемом примере они вовсе не используются. Тайплевел вычисления делаются на Nil и Cons, первый — единица с тегом, второй — произведение с тегом.


Да пофиг. Реализация инстансов классов на технике-аналоге vtable ничем по-сути от происхоящего с помощью АлгТД не отличается. Вернее, наоборот, реализация матча по АлгТД во многих сценариев может быть выполнена на таблицах ф-ий.

Тем более, что обсуждаемый пример можно переписать на АлгТД и обойтись без классов типов. Не в этом суть. Суть была в стоимости итерирования по боксированным типам.


K>Реализация (в компиляторе) требуется. место в памяти в рантайме — нет. В рантайме нет типов.


Для тега алгТД место в рантайме таки требуется.


K>Еще раз. Динамической типизации тут нет. a == 3 динамическая типизация? Нет, 3 не тип.


Повторю, для алгТД есть:
data Box = IntBox int | StringBox string

isThree Box b =
  case b of
    IntBox a -> a == 3
    StringBox a -> a == '3'


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


K>Совершенно верно. Это масимум того, что можно получить от ML-like полиморфизма. Для большего нужны зависимые типы.


Именно. А приводимый пример фактически надуманный, т.к. что там проверять-то?, коль списки формируются параллельно. А для любого другого сценария, действительно требующего проверки, эта магия уже не работает.


V>>а не от того, что полностью поддерживается параметрический полиморфизм в том смысле, как нам пытаются показать в примере.


K>От того. Без поддержки ПП это не заработает.


Да неполноценный это ПП ни разу. В любой точке примера используется один и тот же тип для обоих списков, а потом заявляется, что мы якобы проверяем что типы одинаковы. Хотя такими их объявили сами же. Хочется спросить автора — он хорошо себя чувствует?

Нет ничего проще взять тот же самый n, сформировать сначала один список, потом другой, потом попробовать проделать тот же самый фокус. И хотя тип списков будет опять одинаковый, но фокус уже не сработает. Где ты там увидел работающее ПП? В примере показан несложный трюк, основанный на том, что компилятор Хаскеля способен два одинаково объявленных типа в одной области видимости считать одинаковыми. Стоит выйти из области видимости — и всякое ПП исчезает.


V>>Ну и в С++ вызов ф-ии — это ф-ии времени компиляции, а в Хаскеле — это обращение к группе ф-ий и выбор конкретной через паттерн-матчинг:

V>>main' 0 _ as bs = scalarProduct as bs
V>>main' n i as bs = main' (n-1) (i+1) (Cons (2*i+1) as) (Cons (i^2) bs)

K>Это не верно. Никакой группы функций нет. Вот так:

K>
K>test' :: ScalarProduct a => Integer -> Integer -> a -> a -> Integer
K>test' n i as bs | n == 0    = scalarProduct as bs
K>                | otherwise = test' (n-1) (i+1) (Cons (2*i+1) as) (Cons (i^2) bs)
K>

K>тоже сработает.

Угу, как возражение, что при вызове ф-ий используется неявное ПМ привел явную реализацию на ПМ. Поздравляю.


K>Классы типов тут тоже ничего в рантайме не диспетчеризуют (для ранг-2 полиморфизма будут, но это здесь не используется).


Табличная диспетчеризация таки есть.

V>>В сухом остатке: хотя имеем статическую типизацию (проверку соответствий типов), конкретные типы проверяются в рантайм,


K>Не верно, все типы проверяются в компайл-тайм. Иначе как ошибка появилась бы при компиляции?


V>> конкретные ф-ии тоже выбираются в рантайм

K>Не верно. Все функции выбираются в компайл-тайм.



K>Выбор между двумя видами scalarProduct происходит на этапе компиляции


Каким образом? Чтобы выбор сделать, надо отказаться от боксированного представления, т.е. заранее знать, где конец списка. Если же в compile-time компилятор не знает где конец, то данные надо связывать с кодом, например посредством таблиц ф-ий.

K>Но весь смысл этого куска кода в compile-time проверке!


Да нет там никакой проверки, не изобретай! Ограничение идет прямо в самой сигнатуре main':
main' :: ScalarProduct a => Integer -> Integer -> a -> a -> Integer

Т.е. в самой сигнатуре main' черным по белому сказано, что a->a. Как можно было потом радоваться, что у нас скомпиллировалась строчка в теле main':
scalarProduct a1 a2
или
scalarProduct (Cons x a1) (Cons y a2)
если a1 и a2 имеют один и тот же тип по опредедению main'?

Это как написать x = 2 * 2 и радоваться, что получилось 4.

Ты мне покажи вот так:
main' :: Integer -> Integer -> a -> b -> Integer

Потом подай на a и b одинаковые типы извне. Вот это и будет настоящий ПП, а не тот, которым вы хотите незаслуженно обозвать систему типов Хаскеля.

V>>Для сравнения, Хаскель сначала требует через ПМ распаковать содержимое АлгТД, т.е. уменьшить мощность (или "логическую косвенность") для нашего сценария рекурсивного типа


K>Сюрприз: в обсуждаемом коде на хаскеле 0 (ноль) рекурсивных типов.

K>а в коде-то — смотрите-ка:
K>
K>data Nil = Nil
K>data Cons a = Cons Integer a
K>

K>Никаких рекурсивных типов. Никаких сумм.

Ну коль Cons a параметризируется типом Cons a', то у нас выходит, скажем, де-факто параметрический рекурсивный тип в примере. Дело в том, что в С++ возможны только такого рода рекурсивные типы, если рекурсия объявлена по-значению (через поле или базовый класс), а не по ссылке/указателю. В приведенной неудачной попытке реализации примера на С++ был именно этот вид рекурсии.

И да, как раз случай простого боксирования для обычного рекурсивного типа неинтересен, бо код действительно будет один и тот же на любой глубине рекурсии, т.к. тип один и тот же. Гораздо интереснее вариант такой полиморфной рекурсии, как в примере. Если код main' должен быть одинаковым для каждого шага рекурсии (а он однозначно должен быть одинаковым, коль n может быть сколь угодно большим и неизвестным в compile-time), то должна присутствовать та или иная техника диспетчеризации вызова интерфейсной ф-ии scalarProduct.

V>>Не путаю. Дескриминатор-то типа проверяется в рантайм.


K>Дескриминаторов типа в Хаскеле просто не существует


True, False, Cons, Nil — вот тебе существующие в рантайм дискриминаторы, хранимые вместе с данными. Для случая True, False, Nil данные представляют из себя пустой тупл.


K>Integer — алгебраический тип (и по стандарту, а 3 — его конструктор) и в реализации. Не забудьте еще алгебраический тип Bool. True и False, кстати, тоже типы по-вашему?


Это конструкторы АлгТД в одном контексте и теги АлгТД, то бишь теги хранимого типа — в другом, например в конструкции ПМ. А что, тебя смущает вырожденный случай размеченного объединения навроде Bool?


K>Да. Там где проверять не нужно — там вы не будете проверять ни в хаскеле, ни в C++. Там где без этого не обойтись (например, это указатель на следующий элемент списка или на null) — вы будете проверять в рантайме и там и там.


Это если у нас связанный список боксированных вычислений, то будет так же. А так-то вычисления на подобных шаблонных рекурсивных типов на С++ не то, что не рекурсивны, там даже циклов нет с проверками, есть просто линейный код, повторенный столько раз, сколько глубина рекурсии. Ну и оптимизация в регистрах получается существенная, т.к. помимо ухода затрат на организацию цикла, освобождаются лишние регистры, т.е. кач-во оптимизации выходит получше. Например, для фильтрации нерекурсивным фильтром, эта техника дает увеличение в 1.8-3 раза по сравнению с вариантом двух вложенных циклов... Там же еще играют роль всякие вещи: например, ветвление по выходу из цикла в 100% случаев провоцирует сброс конвейера процессора, а в случае цепочек таких линейных вычислений — никогда. В общем, факт в том, что любой if — тоже дорогая операция, бо может сбросить конвейер. Виртуальные ф-ии в этом плане предпочтительней тега АлгТД, т.к. адрес выбирается безусловно механизмом процессора еще до исполнения инструкции ядром, и плюс компилятор оптимизирует так, что адрес ф-ии достается в начале цикла лишь однажды.
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.