lomeo: (лямбда)
На RSDN я очередной раз дискутировал с VladD2 и, кстати, для меня дискуссия получилась довольно полезной. Речь шла, в частности, и о Haskell. Один из необсуждённых (пока?) тезисов высказал VladD2:

Лично по мне так чем дальше инструмент от математического смысла, тем лучше.

Смысл в том, как я понял, что чем ближе инструмент "к математическому смыслу", тем дальше он от практического. Я с этим совершенно не согласен, однако быстро доказать его неправоту не могу. Поэтому попробую продемонстрировать практичность математического аппарата.

Read more... )
lomeo: (лямбда)
К чему я так подробно расписывал получение свёртки для розы? Очевидно, что интуитивно получить её можно сразу. Так я обычно и делаю, воспользовавшись методом размерностей, пардон, программированием "от типов". Возможно, так делаете и вы. Я хочу показать главный недостаток этого подхода - он неформален.

Read more... )

В данном конкретном случае нам очень сильно помогает Curry-Howard, но он не гарантирует уникальности доказательства (реализации), т.е. этот метод не формализуем. А вот на основе ТК, думаю, можно построить CataEval.
lomeo: (лямбда)
Когда я только разбирался с бананами, линзами и т.д. задача описания катаморфизма для розы:
data Rose a = Rose a [Rose a]

вызывала у меня большое затруднение.

Read more... )

Profile

lomeo: (Default)
Dmitry Antonyuk

April 2024

S M T W T F S
 123456
7891011 1213
14151617181920
21222324252627
282930    

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 30th, 2025 12:14 am
Powered by Dreamwidth Studios