Тогда возникает второй вопрос: насколько сложные задачи (причем практические, а не теоретические) возможно решить на «завершающемся» подмножестве? Насколько понятно выглядит получающийся код?
Как прекрасно сказал Pierce
Do we want languages where a PhD (and two PhDs for Haskell) is required to understand the library documentation?
Is it better for Jane Programmer to write ~20 more or less correct lines of code / day or ~0 perfect ones?
Разве что тулзу на нём не написать, но речь была не об этом, а о возможностях total fp.
Нет, речь идёт как раз о практической возможности применять языки, для которых проблема остановки разрешима.
Ибо какой толк от языка, для которого легко автоматически ловить ошибки, если обычный программист не может его применять?
Давайте поспорим =)
Вопрос стоит простой: достаточно ли выразительны языки, для которых проблема останова разрешима? Вот скажем простое типизированное лямбда исчисление, для него проблема останова разрешима (= проблема существования нормальной формы)… Но! Y-комбинатор уже не выражается… Как же быть?
Спасибо, диссер интересный, сохранил на почитать… Но диссер про ошибки сопоставления с образцом, а не про завершимость (если я правильно понял заключение).
У меня есть сильное подозрение (вытекающее из моего опыта в compiler construction & formal methods), что верифицировать любой нетривиальный компилятор (особенно если он еще и связан с нетривиальной средой исполнения) можно опухнуть.
Coq же это вообще не язык программирования, как я понимаю, а язык/среда для описания доказательств… А-ля старый добрый Larch…
можно было, но суть от этого не изменилась бы: отладочная печать, она и в африке отладочная печать… и я бы не назвал это «вершиной отладочных технологий»
я сам стараюсь «ловить баги думаньем» (я еще называю это термином «psychic debugging», подсмотренным у Раймонда Чена), но иногда отладчик всё таки удобнее чем все остальные костыли…
да ладно вам сказки рассказывать… компилируется значит работает? старо предание, да верится с трудом… вот я намедни можно сказать починял баг в хаскелевом пакете zip-archive.
так знаете как я его локализовывал? расставляя функции error в кишках сего пакета. я, конечно, привычный и видел более жесткие случаи, но не скажу, что это доставило мне большое удовольствие…
Ну, на мой взгляд важно акцентировать внимание на том, что функция в реальности не вычисляется до того момента, когда понадобится…
Как это написать, я с наскоку не скажу…
Просто вы употребили такие слова как «чистота», «ленивость», «строгость», «полиморфный», «класс» но расшифровки их в тексте нет. Это может стать причиной непонимания.
и еще кое-что… при программировании на Haskell (и многих других функциональных языках, например, Lisp) очень удобно пользоваться редакторами поддерживающими REPL (Read-eval-print loop). Например, emacs'ом (c haskell-mode) или патченым (sic!) vim'ом…
о, как совпало-то;
я как раз собирался сварганить свой ответ Google Notebook, с недостающими мне функциями, но мотивации было недостаточно. а теперь и мотивация появилась. замечательно…
Как прекрасно сказал Pierce
Нет, речь идёт как раз о практической возможности применять языки, для которых проблема остановки разрешима.
Ибо какой толк от языка, для которого легко автоматически ловить ошибки, если обычный программист не может его применять?
Вопрос стоит простой: достаточно ли выразительны языки, для которых проблема останова разрешима? Вот скажем простое типизированное лямбда исчисление, для него проблема останова разрешима (= проблема существования нормальной формы)… Но! Y-комбинатор уже не выражается… Как же быть?
Спасибо, диссер интересный, сохранил на почитать… Но диссер про ошибки сопоставления с образцом, а не про завершимость (если я правильно понял заключение).
У меня есть сильное подозрение (вытекающее из моего опыта в compiler construction & formal methods), что верифицировать любой нетривиальный компилятор (особенно если он еще и связан с нетривиальной средой исполнения) можно опухнуть.
Coq же это вообще не язык программирования, как я понимаю, а язык/среда для описания доказательств… А-ля старый добрый Larch…
вот, вот. т.е. от всех багов не застрахует и Haskell… иными словами фразу
в вашем предыдущем комментарии следует читать так
Сделали fromJust где не надо, и опа-хопа аналог NPE в лоб…
и вообще, неразрешимость проблемы остановки как бы намекает нам на то, что мы никогда не будем полностью спасены.
можно было, но суть от этого не изменилась бы: отладочная печать, она и в африке отладочная печать… и я бы не назвал это «вершиной отладочных технологий»
я сам стараюсь «ловить баги думаньем» (я еще называю это термином «psychic debugging», подсмотренным у Раймонда Чена), но иногда отладчик всё таки удобнее чем все остальные костыли…
так знаете как я его локализовывал? расставляя функции error в кишках сего пакета. я, конечно, привычный и видел более жесткие случаи, но не скажу, что это доставило мне большое удовольствие…
Как это написать, я с наскоку не скажу…
Просто вы употребили такие слова как «чистота», «ленивость», «строгость», «полиморфный», «класс» но расшифровки их в тексте нет. Это может стать причиной непонимания.
я как раз собирался сварганить свой ответ Google Notebook, с недостающими мне функциями, но мотивации было недостаточно. а теперь и мотивация появилась. замечательно…