Логическое программирование в Scala. Контекстные абстракции

[XViivi]

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

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

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

[Underskyer1]

На данный момент потенциал логического программирования остаётся нераскрытым, ввиду перечисленных в статье актуальных факторов популярности языков программирования и парадигм в целом. Поэтому сейчас мало смысла говорить о ситуациях, когда путь вычисления описать вручную "сложно". Сообщество пока далеко от таких задач, вот и я не стал заморачиваться с поиском и обоснованием подобных сценариев. Мне кажется, что сейчас полезнее рекламировать ЛП как инструмент для избавления от рутины и сокращения количества кода, каждая строчка которого имеет свою стоимость.

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

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

[XViivi]

Мне кажется, что сейчас полезнее рекламировать ЛП как инструмент для избавления от рутины и сокращения количества кода, каждая строчка которого имеет свою стоимость.

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

Думаю, что вероятность получить неожиданное поведение при ручной композиции программы выше,

в идеале бы конечно потыкаться в это, чтобы понять так ли это, но в любом случае, если такая композиция требует грамотной типизации, то не думаю, что и человек в таких условиях особо ошибётся.

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

но опять же, наверное не попробовав самому на ± хорошем примере не понять, и, может быть, это сократит скорее какие-нибудь рутинные случаи

Однако реализация правил для такого вывода опирается на зависимые типы и выходит за рамки обзора.

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

[Underskyer1]

описания всех given-ов может оказаться дороже по объёму

Вовсе нет. Было упомянуто, что основное отличие заключается только в замене val (или def) на given.

не думаю, что и человек в таких условиях особо ошибётся.

Любой код - это источник ошибок)) Даже популярная тавтология вида val elephant: Elephant = new Elephant(). Ошибок нет только в том коде, которого нет. А встроенные или библиотечные алгоритмы проверяются гораздо надёжнее чем пользовательский код.

Синтаксис различных языков (особенно Scala) сильно перегружен не самыми полезными возможностями. Они нужны только как дань привычкам и сложившейся системе обучения. У given есть свои ограничения, но они не то чтобы сильно мешали. Кстати, статическая типизация как раз и нужна чтобы сократить набор допустимых действий, точнее, защититься от недопустимых. Ограничения - наше всё.

Я не призываю слепо менять парадигму. Лишь пытаюсь привлечь внимание к весьма перспективной концепции, многие преимущества которой ещё предстоит раскрыть.

Да, готовлю материал по зависимым типам. Пока не определился с форматом и составом публикаций и ещё многое предстоит предварительно изучить. Вот только не знаю, смогу ли остаться в теме. Полгода уже без работы сижу - буквально за пару лет опытные программисты резко стали никому не нужны...