(no subject)
Oct. 7th, 2014 11:21 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
yigal_sТолком еще ничего не изучив, было б интересно отдельно разобраться, в чем ПРИНЦИПИАЛЬНО различаются системы типов в Haskell, Ocaml, Scala и, если угодно, С++. Какие у них есть ПРИНЦИПИАЛЬНЫЕ ограничения одной относительно другой?
Т.е., например, в Haskell есть Type Class, а в С++ нет (если не будем вспоминать неудавшуюся попытку введения "концептов", или не пытаться смоделировать то же Type Class через C++ SFINAE и прочие хардкорные извращения). Факт наличия Type Class - конечно, интересен, но взятый сам по себе не является принципиальным ограничением С++, скорее уж это структурирующее "ограничение" Haskell. Опять же, кто-то где-то писал о полиморфных константах в Haskell - но и это преспокойно себе моделируется на С++.
В свете вышесказанного, было бы интересно именно понять где мощь одного языка категорически выходит за пределы мощи другого в области системы типов.
Есть ли что-то внятное почитать-посмотреть по данной теме?
В принципе, интересует разница между Haskell, Ocaml, Scala. C++ - это так, опционально )))
Т.е., например, в Haskell есть Type Class, а в С++ нет (если не будем вспоминать неудавшуюся попытку введения "концептов", или не пытаться смоделировать то же Type Class через C++ SFINAE и прочие хардкорные извращения). Факт наличия Type Class - конечно, интересен, но взятый сам по себе не является принципиальным ограничением С++, скорее уж это структурирующее "ограничение" Haskell. Опять же, кто-то где-то писал о полиморфных константах в Haskell - но и это преспокойно себе моделируется на С++.
В свете вышесказанного, было бы интересно именно понять где мощь одного языка категорически выходит за пределы мощи другого в области системы типов.
Есть ли что-то внятное почитать-посмотреть по данной теме?
В принципе, интересует разница между Haskell, Ocaml, Scala. C++ - это так, опционально )))
no subject
Date: 2014-10-07 04:09 pm (UTC)http://migmit.livejournal.com/32688.html
Код на Haskell: http://lpaste.net/112244
На C++ это повторить-таки получится, но лишь ручками реализовав аналогичный механизм (через void*'ы по сути, прикрутив проверку типов уже поверх), как он реализован в Haskell, а SFINAE и извращения сами по себе не помогут.
По поводу полиморфных констант претензия аналогичная, ибо, собственно, они в коде и использованы в виде "пользователь вводит число, функция на это число выдаёт два вектора (не std::vector) со статической гарантией одинаковости их длины". В C++ не получится, ибо тип должен быть известен compile-time, а пользователь же может ввести число любое, заранее неизвестное.
Стоит отметить чистоту Haskell. В Haskell мы можем принять в качестве аргумента чистую функцию, в C++ - нет, гарантировать этого нельзя. Либо можем задать монаду, в рамках которой допустимы строго определённые операции, как, например, в реализации software transactional memory (http://hackage.haskell.org/package/stm-2.4.3) — внутри atomically нельзя выполнить ничего запрещённого, тогда как в C++, например, ничто не мешает внутри аналогичной функции заниматься, чем угодно. Как это решено (и решено ли) в Ocaml и Scala, я не знаю, ибо ими не пользовался.
Упомяну ленивость, хоть, может, не совсем к месту. Можно орудовать бесконечными списками, а также там, где надо породить некий список, по которому надо пройтись один раз - в C++ придётся либо таки создавать его, либо выворачивать код наизнанку.
Собственно, можно оценить разницу в коде тут: http://toster.ru/q/137223?e=652941#answer_392417
Наверное, можно упомянуть и rewrite rules (http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/rewrite-rules.html), но насколько возможность такого имеет отношение к системе типов - я не знаю.
no subject
Date: 2014-10-07 05:44 pm (UTC)Спасибо, очень интересно. Хотя, мне кажется, должны быть и какие-то более показательные примеры haskell vs C++. Чисто нутрянное ощущение.
Кстати, что данный пример демонстрирует проблемы полиморфных констант, я не соглашусь. Если "пользователь вводит число" - то это уже не константа, т.е. иными словами, не литерал.
no subject
Date: 2014-10-07 05:58 pm (UTC)Более показательные примеры чего? Например, http://toster.ru/q/137223?e=652941#answer_392417 не подходит в качестве такого примера?
no subject
Date: 2014-10-07 06:22 pm (UTC)Пример невозможной вещи в С++ - функция, возвращающая указатель на собственный тип.
> http://toster.ru/q/137223?e=652941#answer_392417 не подходит в качестве такого примера?
Мне бы очень не хотелось это демонстрировать ))) но мне кажется подобное haskell-решению можно и на С++ написать.
no subject
Date: 2014-10-07 06:55 pm (UTC)no subject
Date: 2014-10-07 07:08 pm (UTC)по какому из списков в
concatMap (`replicateM` alphas) [1..n]
надо пробежать всего один раз и почему какого-нидь std::list в С++ будет недостаточно или почему невозможен подобный однократный пробег в С++ ???
no subject
Date: 2014-10-08 07:06 am (UTC)Т.е. это перебор всех комбинаций (с повторяющимися элементами), начиная от односимвольных и заканчивая n-символьными.
std::list в общем случае недостаточно, потому что поведение будет другое - создастся целиком список, тогда как в Haskell благодаря ленивости этого не будет. Например, для n = 6 и alphas = ['a' .. 'z'], результирующий список должен содержать как минимум (посчитаем только 10-символьную серию) 308915776 элементов по 6 символов каждый, т.е. порядка 1.7 Гб. Тогда как в Haskell вычисление длины всего списка или запись этого списка в файл отъедает около 400 Мб. А, к примеру, взятие первых 10000 из них не отъедает памяти вообще:
x = gen ['a'..'z'] 10
y = take 10000 x
main = mapM_ putStrLn y
Тем не менее, конкретно приведённый код для n ≥ 7 и alphas = ['a'..'z'] таки начинает кушать память. Я попробовал replicateM заменить на код, который делает то же самое (для списка):
replicateList :: Int -> [a] -> [[a]]
replicateList 1 xs = [[x] | x <- xs]
replicateList n xs = concatMap (\x -> map (x :) $ gen (n - 1) xs) xs
И кушать перестало.
Таким же образом, например, можно оперировать бесконечными списками типа [1..] (1, 2, 3...) или repeat 1 (бесконечный список единиц).
Но это скорее необычный пример, чем обычная практика. Во многих случаях можно развернуть работу со списками на циклы, но суть в том, что Haskell можно отдельной функцией описать такой вот список, а другими функциями с ним работать. Например, можно написать так:
gen alphas = concatMap (`replicateList` alphas) [1..] -- [1..] - бесконечный
И мы получим список, который я описывал выше, но бесконечный, где длина серий будет расти и расти. А уже тот, кто список пользует, может, к примеру, ограничить только теми, которые короче 4:
takeWhile ((< 4) . length) $ gen ['a'..'z']
Конечно, в C++ можно сделать так же, но для этого надо будет писать какой-то генерирующий итератор, т.е. вывернуть код наизнанку.
То есть если списки планируются небольшие, можно и std::vector/list, а если они вдруг оказываются больше, чем надо, а целиком они не нужны, то придётся код выворачивать, а std::vector/list по нужде создавать на основе вывернутого кода, что гораздо менее удобно писать. На Haskell считай автоматом второй вариант, но при этом с краткой записью.
no subject
Date: 2014-10-08 01:07 pm (UTC)Подобный код на С++, пожалуй, без имплементации генераторов не напишешь, я согласен. Это действительно можно рассматривать как ограничение С++.
Но это сильно в сторону от того, что ищу я изначально в данном посте))) Мне интересны буквально вещи, выразимые на уровне одного языка с помощью системы типов, и не выразимые в другом языке, а уж сколько это будет жрать в рантайме памяти, мне в данном случае пофиг.
no subject
Date: 2014-10-08 02:08 pm (UTC)Рекомендую посмотреть на Agda2 или Idris, ибо там есть зависимые типы (dependent types). В Haskell с последними расширениями GHC какую-то часть возможностей можно изобразить, но я, если честно, не разбирался. Есть такое видео, которое я сам пока не посмотрел :) но там вроде как раз и Agda есть, и Haskell: https://www.youtube.com/watch?v=rhWMhTjQzsU
В копилку к зависимым типам надо упомянуть изоморфизм Карри-Ховарда. В языке с зависимыми типами можно формулировать утверждение, которое суть тип, а также доказательства утверждений, которые суть значения этих типов. Если у типа нет значения, то нет и доказательства. Т.о. например 4 ≤ 3 - это тип такой (типа как Map Int String, только тут имя типа ≤ и его аргументы - 4 и 3), но у него нет значений, а вот у типа 0 ≤ 10 есть значение - z≤n. Полное определение типа можно посмотреть тут. У этого типа два конструктора:
z≤n : ∀ {n} → zero ≤ n
Т.е. 0 не более любого числа
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
Т.е. если m не более n, то suc m не более suc n (suc наряду с zero - конструктор натурального числа, где zero - 0, а suc n на единицу больше n, т.е. "следующее")
Т.о. в функции можно затребовать в качестве аргумента, к примеру, доказательство того, что первый аргумент не более второго, или что произведение первого и второго не более 100. Причём доказательство можно как привести статически (например, если одно число ввёл пользователь, а второе получено путём вычитания первого из ста, то их сумма, ясное дело, не превышает 100, и рантайм проверки тут не надо, можно просто доказать, что для любого n верно (n + (100 - n)) ≤ n, задав функцию, которая конструирует соответствующий тип), если имеющейся информации достаточно для его конструирования, либо ветвясь.
no subject
Date: 2014-10-08 02:11 pm (UTC)no subject
Date: 2014-10-07 07:15 pm (UTC)no subject
Date: 2014-10-07 07:19 pm (UTC)Скажем, в Ada есть "new" type. А в С++ его нет. В Haskell есть Type Class, а в С++ их можно в лучшем случае смоделировать, скрипя зубами (впрочем С++ весь насквозь юзается скрипя зубами).
no subject
Date: 2014-10-08 02:12 am (UTC)А что такое "new type" в Аде? Беглый гугл ничего не нашел.
no subject
Date: 2014-10-08 03:47 am (UTC)В Ада можно было написать что-то вроде
type Apple is new Integer;
и получался тип, который вёл себя как Integer, но с Integer не смешивался (неявное кастирование в обе стороны было запрещено).
ИМХО, достаточно удобная вещь, если мы не хотим складывать яблоки с грушами, а километры с рублями.
no subject
Date: 2014-10-08 04:47 am (UTC)no subject
Date: 2014-10-08 12:51 pm (UTC)хотя общую степенную размерность они не поддерживали.