gds (gds) wrote,
gds
gds

Решил вынести ответ на камент в отдельный пост. Так как дело было в жыжыцэ, пост будет тоже жэжэшный.

Исходный комментарий -- http://diam-2003.livejournal.com/527676.html?thread=1267516#t1267516 :
> Но ведь с другой стороны, у людей, которые всё это пишут, тоже ведь есть мозг.

Конечно есть, но мотивы их писюлек далеко не всегда исходят из желания "сделать людям хорошо", и не из желания поделиться _работающим_ решением (особенно учитывая, что про подобные решения, работающие на практике, мало кто слышал -- а какая-то информация таки просочилась бы).

Немалая часть подобных документов сделана только из-за того, что человек осилил какой-то тупой-простой частный случай, например, "если нет одновременной записи в память -- параллелится", и решил либо в ВУЗе что-то оформить (курсовую, диплом), либо на конференцию поехать. Вот что-то подобное в весьма стилизованном виде читал тут: http://voker57.psto.net/ghegi

Про параллелизацию в пределах хоста -- что-то не встречал более умных подходов, чем ручной, использующий work-stealing queues, но вот чото в теорию не вписывается, да и мутабельность... Если брать параллелизацию вне пределов хоста -- не видел использований какой-нибудь там InfiniBand.

Кроме того, когда я вбросил на тему "зависимые типы нужны только для проверки длины массива, gadt'ы -- только для typed interpreters", мало кто мог показать более годные примеры. Видимо, это какое-то особое, тайное знание, которым никто не делится.

Ну и про gadt'ы Олег писал недавно, как бы подтверждая: "Somehow typed tagless interpreters (embeddings of a typed language) and length-parameterized lists with the append function are the most popular examples of GADTs. Neither of them seem to be particularly good or compelling examples. One can write typed interpreters in the final-tagless style, with no GADTs. Writing append function whose type says the length of the resulting list is the sum of the lengths of the argument lists is cute. However, this example does not go too far, as one discovers when trying to write List.filter for length-parameterized lists."

То есть, как я понимаю, кто-то поставил какую-то задротскую проблему, а другие задроты, решая блеснуть мозгом, предлагают различные её решения. 1. "как ограничить типом возвращаемое конструктором АТД значение" -- gadts, 2. "как проверить, что функция List.nth будет безошибочна" -- dependent types, 3. "expression problem" -- различные извращения разной степени тяжести, если брать решения на х-е, 4. "как контролировать сайд-эффекты" -- манатки и тонны папиров про х-евые решения, Ю-монаду и прочий ональный ад с тоннами других манаток, каждая под свою цель, и с их трансформерами. (блеять, я за последние 5 лет кодинга на окамле только 2 раза натыкался на проблемы со смешиванием ввода-вывода, и где-то раза 4 на проблемы с мутабельностью -- специально считал!).


Теория такая теория.
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 4 comments