Re[5]: Монады в теории категорий
От: Кодт Россия  
Дата: 05.10.07 15:11
Оценка: :))) :)))
Здравствуйте, palm mute, Вы писали:

PM> Это что, я сети Байезана (Bayesian networks) в одной книге видел.


Армяне, наверно — Картезян и Байесян. Или гасконцы.
... << RSDN@Home 1.2.0 alpha rev. 655>>
Перекуём баги на фичи!
Re: Монады в теории категорий
От: Quintanar Россия  
Дата: 05.10.07 08:37
Оценка: -3
Здравствуйте, Аноним, Вы писали:

А>Самая правильная схема изучения монад:

А> категории -> функторы -> натуральные преобразования -> монады
А>An Introduction to Category Theory, Category Theory Monads, and Their Relationship to Functional Programming
А>http://citeseer.ist.psu.edu/62964.html

Абсолютно бессмысленная потеря времени. То, что монады из теории категорий прикрутили проволокой к Хаскелю, не означает, что их изучение даст какие-либо полезные знания в области программирования. Монады в программировании сами по себе зло. Они не имееют никакого отношения к математическим монадам, поскольку для большинства из них не выполняются условия определения (да и проверить, что они выполняются часто просто невозможно), а значит вся теория для них не работает. Они сложны для понимания и создают ложное ощущение, что в них имеется какой-то скрытый мегамощный смысл, хотя, реально, они всего лишь решают обычные задачи только через заднее место. Монады — особенность Хаскеля, следствие его ущербности в императивном плане, в других языках они просто не нужны, поскольку там все монадные проблемы решаются напрямую, грубо но эффективно. Да даже в ленивых языках есть альтернативные, зачастую намного более эффективные подходы к решению проблемы разрушающего присваивания, см. Clean.
Re[4]: Монады в теории категорий
От: palm mute  
Дата: 05.10.07 13:48
Оценка: :)
Здравствуйте, Трурль, Вы писали:


Т> Вспомнился "картезианский продукт" из одного руководства по SQL.


Это что, я сети Байезана (Bayesian networks) в одной книге видел.
Re[5]: Монады в теории категорий
От: deniok Россия  
Дата: 05.10.07 14:30
Оценка: :)
Здравствуйте, palm mute, Вы писали:

PM>Здравствуйте, Трурль, Вы писали:



Т>> Вспомнился "картезианский продукт" из одного руководства по SQL.


PM> Это что, я сети Байезана (Bayesian networks) в одной книге видел.


Угу, я свою диссертацию писал, переводя свои же англоязычные статьи. И делал это по ночам; и вот шеф читает и спрашивает, а что это у тебя за "индекс рефракции"? Я говорю, ну как что — index of refraction. Он смеётся, говорит: "Вообще-то по-русски это — показатель преломления".
Re[4]: Монады в теории категорий
От: Кодт Россия  
Дата: 05.10.07 15:11
Оценка: +1
Здравствуйте, Quintanar, Вы писали:

K>>Странно, в статье "The Haskell Programmer’s Guide to the IO Monad" приводится формальное доказательство того, что IO — монада. Для списков и mayble, если не ошибаюсь, там тоже приведено доказательство.


Q>Да, руками доказать можно, автоматически нет. Т.е. нет той выгоды, что несет проверка типов. Если в определении монады есть ошибка, то вылезет она только в рантайм.


Информация о произвольной аксиоматике — это предмет более высокого уровня, чем система типов.

Можешь, для разнообразия, проверить корректность предиката, заявленного на роль отношения "строгий/нестрогий порядок".
Например, предикат задан таблицей истинности, размером N^2 (где N — мощность универсума элементов).
Наивная проверка аксиомы транзитивности All x, All y, All z (x<y) & (y<z) => (x<z)
требует пропинговать N^3 значений — если, конечно, у авторов валидатора не были заготовлены эвристики...
И что, компилятор должен такой фигнёй маяться?

Но это не значит, что надо всё бросить и отказаться от классов Eq и Ord.
... << RSDN@Home 1.2.0 alpha rev. 655>>
Перекуём баги на фичи!
Монады в теории категорий
От: Аноним  
Дата: 04.10.07 17:19
Оценка:
Самая правильная схема изучения монад:
категории -> функторы -> натуральные преобразования -> монады
An Introduction to Category Theory, Category Theory Monads, and Their Relationship to Functional Programming
http://citeseer.ist.psu.edu/62964.html
Re[2]: Монады в теории категорий
От: Кодт Россия  
Дата: 05.10.07 11:27
Оценка:
Здравствуйте, Quintanar, Вы писали:

Q>Абсолютно бессмысленная потеря времени. <...> Да даже в ленивых языках есть альтернативные, зачастую намного более эффективные подходы к решению проблемы разрушающего присваивания, см. Clean.


Попался! Это в тебе заговорило ложное ощущение того, что монады — эмуляция императивности. Кто сказал, что монады только для этого нужны?
Советую поразмышлять на тему list comprehensions (и обобщения их на set и maybe), во-первых, и на тему Reader, во-вторых. Потом ткни пальцем в то место, где там разрушающее присваивание.
... << RSDN@Home 1.2.0 alpha rev. 655>>
Перекуём баги на фичи!
Re[2]: Монады в теории категорий
От: konsoletyper Россия https://github.com/konsoletyper
Дата: 05.10.07 11:45
Оценка:
Здравствуйте, Quintanar, Вы писали:

Q>Абсолютно бессмысленная потеря времени.


Касательно конкретно этой статьи — да. Касательно монад вообще — не согласен. Статья по монадам для программистов на Haskell не долна залезатьв ТК, а просто пояснять, как работают имеющиеся монады, и как юзать do-нотацию.

Q>То, что монады из теории категорий прикрутили проволокой к Хаскелю, не означает, что их изучение даст какие-либо полезные знания в области программирования.


Их изучение на уровне ТК даст мало. Но вообще — это полезная штука.

Q> Монады в программировании сами по себе зло. Они не имееют никакого отношения к математическим монадам, поскольку для большинства из них не выполняются условия определения (да и проверить, что они выполняются часто просто невозможно), а значит вся теория для них не работает.


Странно, в статье "The Haskell Programmer’s Guide to the IO Monad" приводится формальное доказательство того, что IO — монада. Для списков и mayble, если не ошибаюсь, там тоже приведено доказательство.

Q> Они сложны для понимания и создают ложное ощущение, что в них имеется какой-то скрытый мегамощный смысл, хотя, реально, они всего лишь решают обычные задачи только через заднее место.


Ну не так уж, чтобы через заднее место. Просто несовсем привычно. Тем более, что do-нотация всё это прячет от программиста, и чтобы осилить её, не обязательно знать, что такое монады.

Q>Монады — особенность Хаскеля, следствие его ущербности в императивном плане, в других языках они просто не нужны, поскольку там все монадные проблемы решаются напрямую, грубо но эффективно. Да даже в ленивых языках есть альтернативные, зачастую намного более эффективные подходы к решению проблемы разрушающего присваивания, см. Clean.


Clean не смотрел. Можно пример? По поводу ущербности Хаскелля не понял. И кто сказал, что монады нужны только для внесения императивности?
... << RSDN@Home 1.2.0 alpha rev. 710>>
Re[2]: Монады в теории категорий
От: Аноним  
Дата: 05.10.07 13:00
Оценка:
Здравствуйте, Quintanar, Вы писали:

Q>Здравствуйте, Аноним, Вы писали:


А>>Самая правильная схема изучения монад:

А>> категории -> функторы -> натуральные преобразования -> монады
А>>An Introduction to Category Theory, Category Theory Monads, and Their Relationship to Functional Programming
А>>http://citeseer.ist.psu.edu/62964.html

Q>Абсолютно бессмысленная потеря времени. То, что монады из теории категорий прикрутили проволокой к Хаскелю, не означает, что их изучение даст какие-либо полезные знания в области программирования. [....]


Почему прикрутили? Там в статье написано же что "...a current use of monads bears a closer resembles to Kleisli
triples",и до этого "... a Kleisli triples can be thought as a different syntactic presentation of monad".
Теория категорий на самом деле довольно проста , интересна и, более того она упращает работу программистам.
Например, полиморфные функции можно рассматривать как натуральные трансформации. Это означает сразу, что
к ним применим закон для натуральных трансформаций. Скажем для функции обращение списка rev:T -> T, справедливо
f:S->T
revT * mapList(f) = mapList(f) * revS
(Pierce стр. 42)

Почему к Хаскелю? Не только к Хаскелю. Как Вам монадические парсеры в C# ?
http://blogs.msdn.com/lukeh/archive/2007/08/19/monadic-parser-combinators-using-c-3-0.aspx
Кстати, там ссылка на реализацию в Scala, в которой тоже без монад не обошлось.
Обидно, понимаете ли. Во всем мире дети знают теорию категорий, а у нас...
Re[3]: Монады в теории категорий
От: Трурль  
Дата: 05.10.07 13:17
Оценка:
Здравствуйте, Кодт, Вы писали:

К>Советую поразмышлять на тему list comprehensions (и обобщения их на set и maybe), во-первых, и на тему Reader, во-вторых. Потом ткни пальцем в то место, где там разрушающее присваивание.


А где там монады?
Re[4]: Монады в теории категорий
От: Кодт Россия  
Дата: 05.10.07 13:31
Оценка:
Здравствуйте, Трурль, Вы писали:

К>>Советую поразмышлять на тему list comprehensions (и обобщения их на set и maybe), во-первых, и на тему Reader, во-вторых. Потом ткни пальцем в то место, где там разрушающее присваивание.

Т>А где там монады?

А собственно, Maybe и List — не монады, что ли?
... << RSDN@Home 1.2.0 alpha rev. 655>>
Перекуём баги на фичи!
Re[3]: Монады в теории категорий
От: Трурль  
Дата: 05.10.07 13:33
Оценка:
Здравствуйте, Аноним, Вы писали:

А> Например, полиморфные функции можно рассматривать как натуральные трансформации.

Вспомнился "картезианский продукт" из одного руководства по SQL.
Re[3]: Монады в теории категорий
От: Quintanar Россия  
Дата: 05.10.07 14:23
Оценка:
Здравствуйте, Аноним, Вы писали:

А> Почему прикрутили? Там в статье написано же что "...a current use of monads bears a closer resembles to Kleisli

А>triples",и до этого "... a Kleisli triples can be thought as a different syntactic presentation of monad".
А> Теория категорий на самом деле довольно проста , интересна и, более того она упращает работу программистам.
А> Например, полиморфные функции можно рассматривать как натуральные трансформации. Это означает сразу, что
А> к ним применим закон для натуральных трансформаций. Скажем для функции обращение списка rev:T -> T, справедливо
А> f:S->T
А> revT * mapList(f) = mapList(f) * revS
А> (Pierce стр. 42)

Все эти конструкции должны удовлетворять определениям. Проверить, что монада удовлетворяет монадным законам автоматически нельзя. Значит, если использовать какие-либо преобразования, которые используют эти законы, то будут баги, найти которые, я так думаю, будет посложней, чем в раскопать 100-килобайтный error в Boost.

А> Почему к Хаскелю? Не только к Хаскелю. Как Вам монадические парсеры в C# ?

А>http://blogs.msdn.com/lukeh/archive/2007/08/19/monadic-parser-combinators-using-c-3-0.aspx
А> Кстати, там ссылка на реализацию в Scala, в которой тоже без монад не обошлось.

Одна из множества возможных реализаций. И что дальше, Монадные парсеры уже захватили мир, как bison и yacc?

А> Обидно, понимаете ли. Во всем мире дети знают теорию категорий, а у нас...


Да прям, знают. Во все мире синус от тангенса только каждый 100-й отличит.
Re[3]: Монады в теории категорий
От: Quintanar Россия  
Дата: 05.10.07 14:25
Оценка:
Здравствуйте, Кодт, Вы писали:

К>Попался! Это в тебе заговорило ложное ощущение того, что монады — эмуляция императивности. Кто сказал, что монады только для этого нужны?

К>Советую поразмышлять на тему list comprehensions (и обобщения их на set и maybe), во-первых, и на тему Reader, во-вторых. Потом ткни пальцем в то место, где там разрушающее присваивание.

А в Хаскель и нет разрушающего присваивания. Монады и есть способ решения этой проблемы.
Re[3]: Монады в теории категорий
От: Quintanar Россия  
Дата: 05.10.07 14:29
Оценка:
Здравствуйте, konsoletyper, Вы писали:

K>Странно, в статье "The Haskell Programmer’s Guide to the IO Monad" приводится формальное доказательство того, что IO — монада. Для списков и mayble, если не ошибаюсь, там тоже приведено доказательство.


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

K>Clean не смотрел. Можно пример? По поводу ущербности Хаскелля не понял. И кто сказал, что монады нужны только для внесения императивности?


Clean — это к Gaperton.

Нет, монады в некотором смысле полезны. Но считать, что они настолько хороши, что их нужно внедрить во все остальные языки, я бы не стал.
Re[4]: Монады в теории категорий
От: Аноним  
Дата: 05.10.07 14:48
Оценка:
Здравствуйте, Трурль, Вы писали:

Т>Здравствуйте, Аноним, Вы писали:


А>> Например, полиморфные функции можно рассматривать как натуральные трансформации.

Т> Вспомнился "картезианский продукт" из одного руководства по SQL.

Извините, когда долго читаешь по англицки начинаешь заговариваться.
Так ведь русских мануалов нет.
А по делу? Действительно монады бесполезны?
Они же используются в куче научных работ, посвященных семантике языков программирования,
компиляторам и черт знает еще чему.
Тот же Мейджер или Вадлер все это знают в совершенстве.
Чем мы хуже?
Re[4]: Монады в теории категорий
От: Кодт Россия  
Дата: 05.10.07 15:11
Оценка:
Здравствуйте, Quintanar, Вы писали:

К>>Попался! Это в тебе заговорило ложное ощущение того, что монады — эмуляция императивности. Кто сказал, что монады только для этого нужны?

К>>Советую поразмышлять на тему list comprehensions (и обобщения их на set и maybe), во-первых, и на тему Reader, во-вторых. Потом ткни пальцем в то место, где там разрушающее присваивание.

Q>А в Хаскель и нет разрушающего присваивания. Монады и есть способ решения этой проблемы.


Тот же вопрос, дубль два. Зачем в list comprehensions могло бы понадобиться разрушающее присваивание, из-за отсутствия которого, якобы, хаскель вынужден реализовывать его на монадах?
... << RSDN@Home 1.2.0 alpha rev. 655>>
Перекуём баги на фичи!
Re[5]: Монады в теории категорий
От: Quintanar Россия  
Дата: 05.10.07 19:21
Оценка:
Здравствуйте, Кодт, Вы писали:

>Тот же вопрос, дубль два. Зачем в list comprehensions могло бы понадобиться разрушающее присваивание, из-за отсутствия которого, якобы, хаскель вынужден реализовывать его на монадах?


Подмена причины и следствия. List Compr. и монады не связаны жестко друг с другом. LC можно реализовать и без монад (на макросах, например). Монады нужны в первую очередь ради ввода-вывода.
Re[5]: Монады в теории категорий
От: Трурль  
Дата: 06.10.07 14:10
Оценка:
Здравствуйте, Кодт, Вы писали:

К>А собственно, Maybe и List — не монады, что ли?

Монады. Но ведь первокласники не изучают полугруппы, а в пятом классе как-то обходятся без колец и полей.
Re[5]: Монады в теории категорий
От: Аноним  
Дата: 07.10.07 09:50
Оценка:
Интересно, а как насчет бананов?
Они тоже считаются бесполезными?
Re[6]: Монады в теории категорий
От: Аноним  
Дата: 07.10.07 11:14
Оценка:
А изоморфизм Карри-Ховарда-Ламбека тоже не нужен?
Положительно, господа, чего не хватишься -ничего вам не нужно !
Ведь без теории категорий это все не изучить.
Re[7]: Монады в теории категорий
От: deniok Россия  
Дата: 07.10.07 12:18
Оценка:
Здравствуйте, Аноним, Вы писали:

А>Положительно, господа, чего не хватишься -ничего вам не нужно !


Да нужно, нужно.

Я вот понял, что вадлеровские халявные теоремы — действительно халявные, после того как стрелочки научился рисовать
Re[6]: Монады в теории категорий
От: Кодт Россия  
Дата: 08.10.07 08:40
Оценка:
Здравствуйте, Трурль, Вы писали:

К>>А собственно, Maybe и List — не монады, что ли?

Т>Монады. Но ведь первокласники не изучают полугруппы, а в пятом классе как-то обходятся без колец и полей.

Кто не изучает, а кто и изучает Моя мама — преподаватель в институте, например, приходила к нам в 2-3 класс и рассказывала о Началах математики — естественно, на пальцах, но именно о полугруппах и прочем

И потом, уважайте Хаскель: его авторы и так уже сделали шаг по конкретизации, выкинув из Гофера универсальные comprehensions и ++ над монадами. (А зря!!!)
... << RSDN@Home 1.2.0 alpha rev. 655>>
Перекуём баги на фичи!
Re[6]: Монады в теории категорий
От: Кодт Россия  
Дата: 08.10.07 08:40
Оценка:
Здравствуйте, Quintanar, Вы писали:

Q>Подмена причины и следствия. List Compr. и монады не связаны жестко друг с другом. LC можно реализовать и без монад (на макросах, например). Монады нужны в первую очередь ради ввода-вывода.


Для ввода-вывода нужны не монады, а последовательное выполнение. А как именно сделать — на продолжениях функций, на уникальных типах, на монадах — тут возможны варианты.
Можно было вообще ввести модификатор типа "volatile", операции над которым всегда строго последовательны. Т.е. прибить на уровне языка. (В принципе, это та же монада IO, но не обращаясь к её монадной сути).
... << RSDN@Home 1.2.0 alpha rev. 655>>
Перекуём баги на фичи!
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.