Языки программирования

[akuklev]

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

Comments

[chaource]

До появленiя FP, въ трудѣ программиста не было мѣста для математическихъ концепцiй. Ни теорiя категорiй, ни теорiя логическихъ доказательствъ, ни теорiя типовъ, ни HoTT не были нужны, потому что они никакъ не облегчали трудъ программиста и даже вообще не относились къ процессу написанiя программъ. Если посмотрѣть на книгу Кнута "Искусство программированiя", то она заполнена угадыванiемъ того, какъ написать программу и потомъ доказательствомъ, что Кнуту удалось угадать правильно.

Только въ FP математика реально используется для построенiя языка программированiя и для написанiя программъ. Только въ FP построенiе языковъ и программъ можно формализовать достаточно содержательнымъ образомъ, чтобы программистъ могъ думать о программѣ въ терминахъ "здѣсь у меня коварiантный функторъ - здѣсь у меня естественное преобразованiе - значитъ, тутъ тоже долженъ быть коварiантный функторъ" и создавать кодъ, пользуясь этими концепцiями.

[akuklev]

Мне теперь в ЖЖ очень нехватает лайков. В данный момент, чтобы поставить их ко всём трём вашим комментариям.

[chaource]

По существу, вы выдвигаете слѣдующую гипотезу: если языкъ программированiя хорошо подходитъ для того, чтобы на немъ записать аксiоматику натуральныхъ чиселъ Пеано, универсальной алгебры, и т.п., то этотъ языкъ программированiя будетъ также хорошъ для написанiя базъ данныхъ, вебъ-браузеровъ и бизнесъ-приложенiй (т.к. языки программированiя въ реальномъ мiрѣ нужны только для этого).

Иными словами, дается рекомендацiя дѣлать такiе языки программированiя, для которыхъ предметная область разнообразныхъ индуктивныхъ алгебраическихъ конструкцiй является "декларативной предметной областью", т.е. чтобы на данномъ языкѣ было легко и просто записать аксiоматику Пеано или аксiомы категорiи или другiя такiя вещи.

Неочевидно, что эта гипотеза вѣрна. Пока что, напримѣръ, неочевидно, что Coq, Agda и Idris существенно облегчаютъ программированiе по сравненiю съ OCaml и Haskell.

[akuklev]

> По существу, вы выдвигаете слѣдующую гипотезу: [...]

Не совсем; я считаю, что языки программирования в идеале должны в том числе подходить и для этого. Я нигде не утверждаю, что этого достаточно для декларативного описания других предметных областей. Пример языка Coq отлично иллюстрирует эту мысль - в этом языке напрочь отсутствует машинерия для концептуализации чего бы то ни было, выходящего за пределы конструктивной математики. (В Idris 2 это уже не так.)

[chaource]

Пока что были безуспѣшны попытки создать языкъ, гдѣ всѣ предметныя области были бы сразу декларативны. Сегодняшнiй подходъ въ томъ, чтобы на данномъ языкѣ дѣлать библiотеки, приближенно декларативныя для необходимой задачи. Поэтому вопросъ въ томъ, на какомъ языкѣ удобнѣе дѣлать такiя библiотеки.

Если для построенiя этихъ библiотекъ сильно помогаютъ индуктивно опредѣленныя алгебраическiя конструкцiи, или разныя модальности и т.п., то въ принципѣ Сoq и Idris должны бы всѣхъ положить на лопатки. Но этого пока не видно. Ну, или пока мы не поняли, какъ надо правильно использовать Coq и Idris, какiе нужны "модальности" и т.п.

[akuklev]

> Если для построенiя этихъ библiотекъ сильно помогаютъ индуктивно опредѣленныя алгебраическiя конструкцiи, или разныя модальности и т.п., то въ принципѣ [...]

Я полагаю, что в этом отношении мы просто стоим в самом начале пути. В особенности это касается субструктурных модальностей, которые только-только наклюнулись в Idris 2 и вообще отсутствуют где-либо ещё.

[clayrat]

из Lean4 кстати грозятся сделать взаправдашний ЯП