Мне в такие моменты не хватает всяких там obvious proof search и нормальной поддержки typed holes как в идрисе.

Мне что-то лень эти соглашения вспоминать-запоминать, как-то оно не ложится у меня, короче.

И, кстати, раз уж тут все такие умные, чо почитать про решение уравнений на типы?

Я хочу решить ξ = Пx:ξ.T, где T упоминает x, относительно ξ, или формально доказать, что нетривиальных невырожденных решений нет.

@graninas хороший список книг и статей там по ссылке где-то, спасибо. Я тут без комплюктера останусь на пару недель, будет, чем заняться.

😊

Наоборот, может быть. Как раз в императивном языке можно довольно просто повысить человека до кодообезьянки, которая будет делать всякие полезные мелочи в отведённых рамках.

Думаю, ФП само по себе предназначено для сеньоров, потому что необходимый опыт теории и практики программирования, чтобы начать замечать, что с императивщиной ЧТО-ТО НЕ ТАК — это как раз примерно тот же опыт, который требуется, чтобы претендовать на сеньорство

У меня с discoverability оптики тоже проблемы, в голову всё сразу загрузить не выходит. Вот эта страница очень помогает, если пользуетесь lens: https://github.com/ekmett/lens/wiki/Operators

Элитарность?

Нет, просто, полагаю, эволюция из императивных языков в сторону функциональщины более естественна.

Императивности в сторону декларативности скорее естественно

Имхо

Ну чёт пролог не особо мейнстрим

И нет ощущения что туда что-то движется

Допустим, что все языки, кроме хаскелла исчезли. Все императивные программисты умерли. Вместо процессоров теперь производят только лисп-машины. Начинающие разработчики идут в хаскелль, потому что куда ещё идти? Вскоре один из них, потратив годы на изучение фолдов, траверсалов и линз, восклицает: "Я понял, почему всё сложно! Вся проблема в иммутабельности. Вот если бы был язык, где все операции были бы представлены разнесёнными по времени, и компьютер в каждую единицу времени, исполнял бы только одну операцию, так что всегда было бы до и после. И тогда можно было бы написать просто измени значение a на b, и после этого всё, что обращалось к ячейке памяти, получало бы b, а не a. Чёрт, а это ведь математически возможно... Да это бы в тыщщу раз всё упростило! Мы бы смогли свернуть горы!"

Зато ямл девелоперов как грязи)

Мы бы смогли представлять программы не в виде непонятных абстрактных сущностей типа комоноидов и профункторов, а в виде конкретных собачек и кошечек, которые подходят и обнюхивают друг друга. Вот это да!

Сложно

И вся история пойдёт по кругу, в чём и вывод: чтобы понять вполне, зачем нужно сложное и малопонятное функциональное программирование, надо сначала накушаться императивщины, особенно коллективной, сутками посидеть до красных глазок над ошибкой, которая случилась, потому что два месяца назад кто-то перепутал две строчки в далёком файле, и вот тогда только можно брать и грузить человека функциональщиной, потому что он знает: альтернатива много-много хуже.