LINUX.ORG.RU

[ЖЖ] *морфизм, Haskell & Lisp

 


3

1

Вот все праздники разбирался с Template Haskell, квазицитированием, SYB и ghc7, не забывая такие важные вещи как распитие спиртных напитков и игру в FreeCiv :)

И вот какая идея мне пришла в голову... Катаморфизм ведь — штука всеобъемлющая, и если лисперы могут называть свои S-выражения алгебраическими типами данных, то почему же мы не можем называть алгебраические типы данных S-выражениями?

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

Единственное, «но» в подходе лисп-систем к компиляции, там компилятор «внутри», а не «с боку» как в более традиционных подходах. А так, работы ведутся, та же Java, та же Scala позволяет вмешиваться в работу компилятора. А в GHC есть Template Haskell, который идеологически близок к лисповским макросам, с той только разницей, что они стоят по разные стороны относительно катаморфизма: лисп как списки, хаскель как алгебраические типы с соответствующей типизацией.

В ООП языках все еще интереснее, там для реализации лисповского подхода нужно две вещи: а) классы должны быть объектами первого класса; б) должен быть способ узнавать конкретный тип объекта в рантайме. В Яве есть и первое (на худой конец в рамках JVM), и второе. В С++ есть RTTI, а вот с первым дела обстоят вроде бы не очень, хотя Александреску в своей книге показывал, вроде бы, как можно генерить иерархию классов с помощью шаблонов. Про Scala, вообще молчу, там алгебраические типы «из коробки» имеются.

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

★★★★★
Ответ на: комментарий от archimag

> Для этого и придумали REPL, что бы постоянно запускать в нём код. А толку от постоянного запуска кода? У тебя просто висит несколько условий, которые при тестовом запуске false, в результате чего ветка с битым методом не выполняется. Или наоборот - у тебя определение функции в какой-то ветке, которая обычно выполняется в тестах, а потому все работает, но как только условие не будет выполнено - получим пиздец в рантайме.

anonymous
()
Ответ на: комментарий от anonymous

> У тебя просто висит несколько условий, которые при тестовом

запуске false


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

archimag ★★★
()
Ответ на: комментарий от archimag

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

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

one_more_hokum ★★★
()
Ответ на: комментарий от archimag

[code] (defun foo (x) (when (not (eq? 45677856423785623785678 x)) (defun yoba () `yoba)))

(foo (read)) (yoba) [/code] А теперь скажи, как мне это запустить, чтобы оно упало?

anonymous
()
Ответ на: комментарий от one_more_hokum

> И как ты планируешь обойти все узлы состояний системы, если их там over 9000, и на некоторых происходит затык?

А никак. Если есть евал - то это даже теоретически невозможно.

anonymous
()
Ответ на: комментарий от anonymous

> (eval (read))

Ну, REPL, ну и что? Само наличие eval, по твоему, даст прохождение по всем условиям и значениям входных переменных само собой?

one_more_hokum ★★★
()
Ответ на: комментарий от one_more_hokum

> Ну, REPL, ну и что? Само наличие eval, по твоему, даст прохождение по всем условиям и значениям входных переменных само собой?

Не понял, о чем ты? Какое прохождение?

anonymous
()
Ответ на: комментарий от anonymous

> Не понял, о чем ты? Какое прохождение?

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

one_more_hokum ★★★
()
Ответ на: комментарий от anonymous

и к чему ты это говоришь?

К тому, что сам по себе REPL не обеспечит тебе прогон всех условий, и, следовательно, не обеспечит 100% гарантии выполнения твоего (достаточно объёмного) кода у клиента.

Или мы вообще о чём говорим-то???

one_more_hokum ★★★
()
Ответ на: комментарий от archimag

> Я таки понял, что статически компилируемые языки гарантируют на 100%?

Таки не 100%, но поболе, чем языки с динамической типизацией, да ещё и интерпретируемые. Точное соотношение, разумеется, не скажу, ибо.

one_more_hokum ★★★
()
Ответ на: комментарий от one_more_hokum

Конечно РЕПЛ никак не автоматизирует прогон условий. Он всего лишь значительно облегчает тестирование различных участков кода, особенно тех, в поведении которых ты не уверен. Если тебе западло тестировать, то толку от РЕПЛа один фиг ноль; драть и убивать.

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

staseg ★★★★★
()
Ответ на: комментарий от staseg

> мифических вызовах несуществующих функций

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

или сегфолтов


А это здесь при чём?

one_more_hokum ★★★
()
Ответ на: комментарий от archimag

> Я таки понял, что статически компилируемые языки гарантируют на 100%?

Ты верно понял.

anonymous
()
Ответ на: комментарий от staseg

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

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

anonymous
()
Ответ на: комментарий от anonymous

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

one_more_hokum ★★★
()
Ответ на: комментарий от one_more_hokum

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

А кто говорил про _любые_ ошибки? Но, например, агда.

anonymous
()
Ответ на: комментарий от anonymous

> А кто говорил про _любые_ ошибки? Но, например, агда.

Логические она точно не отловит. Или когда ошибка в самой спецификации.

anonymous
()
Ответ на: комментарий от anonymous

> Или когда ошибка в самой спецификации.

Ну то, что программа соответствует спецификации, доказать можно. А больше ничего доказывать смысла нет.

anonymous
()
Ответ на: комментарий от anonymous

> Ну то, что программа соответствует спецификации, доказать можно.

А больше ничего доказывать смысла нет.


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

archimag ★★★
()
Ответ на: комментарий от archimag

> Поскольку в реальности спецификации обычно начинают более-менее чётко выглядеть только в концу разработки

Так нам и надо к концу. Нам надо доказать отсутствие ошибок перед тем, как программа заказчику уйдет, а какие там ошибки на стадии разработки - нам плевать.

anonymous
()
Ответ на: комментарий от anonymous

> Нам надо доказать отсутствие ошибок перед тем, как программа

заказчику уйдет


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

archimag ★★★
()
Ответ на: комментарий от archimag

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

«Конец разработки» - это когда программа соответствует спецификации, удовлетворяющей заказчика. То, что потом спецификация может измениться - уже не важно, важно что на тот конкретный момент конкретная программа должна соответствовать конкретной спецификации.

anonymous
()
Ответ на: комментарий от anonymous

> «Конец разработки» - это когда программа соответствует спецификации,

удовлетворяющей заказчика.


Я правильно понимаю, что статическая типизация не совместима с XP и другими прогрессивными методиками разработки?

archimag ★★★
()
Ответ на: комментарий от anonymous

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

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

Этого сделать на данный момент нельзя, да и никому не надо.

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

anonymous
()
Ответ на: комментарий от archimag

> Я правильно понимаю, что статическая типизация не совместима с XP и другими прогрессивными методиками разработки?

И отчего всякие Haskell-и да OCaml-и считаются лучшими языками для прототипирования?..

one_more_hokum ★★★
()
Ответ на: комментарий от one_more_hokum

> И отчего всякие Haskell-и да OCaml-и считаются лучшими языками для прототипирования?..

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

anonymous
()
Ответ на: комментарий от archimag

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

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

anonymous
()
Ответ на: комментарий от archimag

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

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

Вот посмотри на разработки по спецификациям: House OS на Хаскеле, seL4 , TRON, EROS и BitC , драйвера DevIL (описание)

Тут сначала описана спецификация (в случае seL4 — спецификация не на сам L4, который уже был, а спецификация проверки на безопасность), затем спецификация формально верифицируема, затем пишется ОС (или драйвер) по формально проверенной спецификации. То есть, спецификации становятся исполняемыми — потому что формально верифицируемы и доказаны на корректность.

Для приложений сурового ынтерпрайза гугли в сторону метамоделей, по «Metamodel framework» . Например, у Eclipse есть EMF /TMF /ECF/EPF метамодели. Из всего этого выводка наиболее интересен с точки зрения функциональности Xtext как средство создания DSL, почти что language workbench на базе Eclipse.

Я как бы прозрачно намекаю, что DSL — это тоже исполняемая спецификация.

Вообще почитай хотя бы того же Джоэля, что он пишет о правильной, полезной спецификации. А то, то что ты называешь спекой — это записки на манжетах, а не спецификация.

anonymous
()
Ответ на: комментарий от anonymous

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

и так далее, вплоть до драйверов и ОС

Этого сделать на данный момент нельзя,


вообще-то, можно

да и никому не надо.


но не нужно.

у т.е. всякие факториалы еще можно гарантировать, а что-то сложнее трудно.


сразу на ум приходит многопоточное программирование и отсутствие race conditions. И ещё что-то по характеристикам GC и/или JIT — только они владеют динамической полной информацией.

anonymous
()
Ответ на: комментарий от archimag

> Я же и говорю, что написан код, который реально никогда не запускался. Что просто бред. Разработчика застрелить прямо на рабочем месте.

Только если разработчик делает формочки к БД. Но, уверяю тебя, бывают более алгоритмически содержательные задачи.

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

> Только если разработчик делает формочки к БД.

Я х.з., никогда таким не занимался, не знаю специфики.

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


Ради бога, что ты думаешь, я задач разных не видел, не решал?

Ну т.е. ты считаешь, что писать код и не проверять его это нормально?

archimag ★★★
()
Ответ на: комментарий от archimag

> Ради бога, что ты думаешь, я задач разных не видел, не решал? Ну т.е. ты считаешь, что писать код и не проверять его это нормально?

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

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

> Хорошо, расскажи, сколько и каких тестов надо написать

Вы о чём вообще? Речь шла совсем о другом.

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

archimag ★★★
()
Ответ на: комментарий от archimag

предлагаю общаться на «ты»

Речь шла совсем о другом.

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

например, в g++ например есть gcov, который может гарантировать, что при тестовом прогоне прошли все строки (хотя половинки строк он не проверяет) — я ожидаю, что есть и допустим юзается для лиспа какой-то аналог

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

> ну так можно отвлечься немного и все же выяснить, колько и каких

тестов надо написать, чтобы 100% быть уверенным, что нигде не

вызывается неопределенная функция



Гарантировать этого, конечно, нельзя. В динамических языках и не нужно.

archimag ★★★
()
Ответ на: комментарий от archimag

> Гарантировать этого, конечно, нельзя. В динамических языках и не нужно.

Это ты к тому, чтобы ловить исключение «вызов неизвестного метода» и юзать к своей выгоде?

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

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

> Это ты к тому, чтобы ловить исключение «вызов неизвестного метода»

и юзать к своей выгоде?


Нет, я к другому. В CL вызов несуществующий метод в обычном коде вызовет предупреждение компилятора, а нормальные разработчики обычно стараются, что бы никаких предупреждений не было. Так что основная проблема это funcall или apply. И тут есть две ситуация. Первая - по логике данный вызов должен безусловно быть и тогда разработчик должен убедиться что он есть, непосредственным запуском кода и/или написание тестов. Вообще, в таком случае что бы где-то был вызов несуществующего метода и что бы это прошло через тесты и через простое тестирование работоспособности приложения - я такого никогда не видел. Вторая - метода действительно может не быть и разработчик знает об этом на этапе разработки, тогда он должен предусмотреть адекватную реакцию, ибо это есть часть логики программы.

archimag ★★★
()
Ответ на: комментарий от anonymous

REPL всё равно удобнее, чем write-save-compile-run-test

anonymous
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.