?

Log in

No account? Create an account
Почему LISP? - Жить не можем без проблем! [entries|archive|friends|userinfo]
Жить не можем без проблем!

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Почему LISP? [Jan. 13th, 2011|02:05 pm]
Жить не можем без проблем!

ru_lisp

[aralex]

Как говорил Ворошилов, вопрос к Знатокам (к знатокам LISP-а в данном случае)! Почему таки LISP? Или, если конкретнее, вопроса три:

  1. Для каких именно задач LISP подходит больше, чем другие языки?
  2. За счёт чего для них он подходит больше?
  3. В чём именно выражается его преимущество?

Если не в лом, приведите, pls, коротенькие иллюстрации на LISP-е (или ссылочку на них). Заранее благодарен!

Исходно данный пост был размещён в сообществе ru_programming, но там Знатоков, способных ответить внятно и по сути, увы, не нашлось :(

linkReply

Comments:
From: (Anonymous)
2011-01-16 04:37 pm (UTC)
> Но типов - как логики для рассуждения о программах, средства метаконтроля программ, - в Лиспе нет и это единственное упущение Лиспа.

По-моему, гораздо полезнее обнаружения ошибки возможность быстро ее найти и исправить (потому что ошибки в любом случае будут, если только мы не доказывали корректность руками или не использовали что-то вроде Агды), а с этим у лиспа все в порядке. Ну и зависит многое от задач, конечно. Если мы имеем четкую спецификацию, то логично использовать язык с развитой системой типов, если же у нас спецификация сильно плывет, то особого профита система типов, наверное, не даст. Ну и, опять же, в лиспе есть возможность написать под спецификацию дсл, а потом доказать корректность этого дсл, что будет горазло проще доказательства корректности голого кода.
(Reply) (Parent) (Thread)
[User Picture]From: thesz
2011-01-16 05:00 pm (UTC)
>По-моему, гораздо полезнее обнаружения ошибки возможность быстро ее найти и исправить

Великолепно!

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

Наоборот. При наличии спецификации можно обложиться тестами и тогда система типов не большой помощник. А вот когда спецификации нет, или когда она изменяется, то типы позволяют не допускать глупых ошибок при её создании, а при изменении спецификации - распространять изменения всюду, где это необходимо.
(Reply) (Parent) (Thread)
From: (Anonymous)
2011-01-17 04:33 am (UTC)
> Великолепно!

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

> При наличии спецификации можно обложиться тестами и тогда система типов не большой помощник.

В какой вселенной тесты стали гарантией корректности? Ее даже 100% покрытие путей не дает.

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

А зачем нам делать изменения всюду, где это необходимо, если потом спецификация изменится, и нам все это, что мы меняли, придется менять снова? Наша цель - корректность готового подукта (под готовым понимается то, что он идет в эксплуатацию), ведь так? С чего бы нас должна волновать его корректность на стадии разработки? Есть ошибки? Пусть будут - процессу разработки они ничуть не мешают, а значит, и исправлять их смысла нет.
То есть я вот к чему - типы позволяют доказать, что наша программа соответствует некоторому подмножеству спецификации. Если спецификации пока нет - доказывать нечего. Если спецификация меняется - то мы тратим ресурсы на зряшнюю работу, потому что актуально только последнее доказательство. Все предыдущие нам ничего не дали. Возникает вопрос - зачем эти траты? Мы можем получить тот же результат, добавив типы _в конце_, но при этом экономим на начальной и средней стадии. Где в моих рассуждениях ошибка?
(Reply) (Parent) (Thread)
[User Picture]From: thesz
2011-01-17 08:36 am (UTC)
>Я имел в виду не конкретную одну ошибку, а в общем, конечно же. то есть полезнее уметь быстро локализовывать и исправлять любую ошибку, чем уметь обнаруживать некий узкий класс ошибок на раннем этапе.

Вы считаете, что эти две вещи мешают друг другу? Серьёзно?

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

Почему мы будем менять "всё это, что мы меняли"?

Уберите квантор всеобщности, у вас даже вопроса не получится.

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

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

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

Мы более уверены, что это не ошибка программы, чем если бы типов не было.

Собственно, именно по этому критерию я и выбрал когда-то Хаскель. Как язык для написания прототипов, инструмент для исследования пространства решений, дающий при этом максимальные (на тот момент) гарантии правильности (соответствия задуманному) реализации решения.
(Reply) (Parent) (Thread)
From: (Anonymous)
2011-01-18 09:33 am (UTC)
> Вы считаете, что эти две вещи мешают друг другу?

Нет, конечно, с чего вы взяли?

> Уберите квантор всеобщности, у вас даже вопроса не получится.

Хорошо:
А зачем нам делать изменения всюду, где это необходимо, если потом спецификация изменится, и нам то, что мы меняли, придется менять снова?

> Наоборот. Дали. Очень много дали. Они показали нам, что программы, правильно реализующие все предыдущие спецификации, не удовлетворяет каким-то критериям.

А зачем нам это знание?

> Мы более уверены, что это не ошибка программы, чем если бы типов не было.

Не понял. Что именно не ошибка программы?
(Reply) (Parent) (Thread)
[User Picture]From: thesz
2011-01-18 08:34 pm (UTC)
>> Вы считаете, что эти две вещи мешают друг другу?
>Нет, конечно, с чего вы взяли?

Они у вас противопоставляются. "то есть полезнее уметь быстро локализовывать и исправлять любую ошибку, чем уметь обнаруживать некий узкий класс ошибок на раннем этапе."

"Полезней достичь одного, чем другого." Если нельзя достичь этих целей вместе, значит, они как-то мешают друг другу.

Не так? Я неправ?

>Хорошо: А зачем нам делать изменения всюду, где это необходимо, если потом спецификация изменится, и нам то, что мы меняли, придется менять снова?

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

Если это не так, то спецификации нам спускают сверху, мы работаем в Индии и получаем $20 в сутки.

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

Для того, чтобы двигаться в правильном направлении. Всем проектом в целом.
(Reply) (Parent) (Thread)
From: (Anonymous)
2011-01-19 03:21 am (UTC)
> Не так? Я неправ?

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

> Потому, что следующая спецификация обязательно будет результатом переработки предыдущей.

Это ответ на какой-то другой вопрос.

> Для того, чтобы двигаться в правильном направлении.

И как оно помогает двигаться? Вообще для меня очень неожиданна мысль о том, что программа может обладать некоторыми соответствиями спецификации, о которых нам неизвестно. Откуда эти соответствия взялись-то? "Случайно вышло"? Изначально программа ничему не соответствует и только потом мы доказываем, что определенные соответствия есть, так? По-моему, можно считать, что нету никаких других соответствий, кроме доказанных, потому что вероятность такого "случайно вышло" пренебрежимо мала.
(Reply) (Parent) (Thread) (Expand)
(no subject) - (Anonymous) Expand
From: (Anonymous)
2011-01-17 05:09 am (UTC)
Кстати, еще хотелось бы узнать - что за бред вы несете на счет спецформ? Языков без спецформ не существует, даже в обычном лямбда-исчислении есть спецформа - сама лямбда. И у вас в хаскеле полно спецформ - do, let, class, type etc., причем их больше чем в лиспе, и никого не возмущает, что они не передаются в функцию. Спецформа ничем не отличается от кейворда в обычном языке.
(Reply) (Parent) (Thread)
[User Picture]From: thesz
2011-01-17 08:42 am (UTC)
>Спецформа ничем не отличается от кейворда в обычном языке.

Она выглядит, как функция.

Как и макрос.
(Reply) (Parent) (Thread)
From: (Anonymous)
2011-01-18 09:40 am (UTC)
Во-первых - какие проблемы с тем, что она выглядит как функция?
Во-вторых - в хаскеле тоже так, вот "type a = b" это выглядит в точности как определение функции type с одним аргументом: "f a = b"
(Reply) (Parent) (Thread)
From: (Anonymous)
2011-01-18 10:15 am (UTC)
"Во-вторых - в хаскеле тоже так, вот "type a = b" это выглядит в точности как определение функции type с одним аргументом: "f a = b""
Malformed head of type or class declaration
Может вам составить какое-то представление о хаскеле сначала? Это может положительным образом сказаться на уровне дискуссии.
(Reply) (Parent) (Thread) (Expand)
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
[User Picture]From: thesz
2011-01-18 08:51 pm (UTC)
>Во-вторых - в хаскеле тоже так, вот "type a = b" это выглядит в точности как определение функции type с одним аргументом: "f a = b"

Как я понимаю, вы не знаете Хаскель вообще никак.

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

Эта область обещает быть чрезвычайно плодовитой. Её основание, положенное учеником Колмогорова Мартином Пером Лёфом, не содержит противоречий, в отличии от систем типов большинства языков программирования (и Хаскеля в том числе). Используя её, я могу заставить программиста доказать существование определённого объекта, чтобы он построил доказательство его существования, написав программу. Я говорю "заставить" потому, что у него не будет шансов допустить ошибку.

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

Так что, если не хотите всю жизнь писать "type a = b" в спорах "Лисп супротив Хаскеля, Лисп играет белыми", посмотрите на Coq или Agda2 (или на Qi, он на Лиспе, но на последний не советую - фигня-с, судя по всему). Эти языки могут сэкономить кучу времени при создании действительно сложных систем.

Как сейчас мне экономит время Хаскель, но ещё лучше.
(Reply) (Parent) (Thread) (Expand)
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
[User Picture]From: freiksenet
2011-01-18 11:53 am (UTC)
Вообще существует. Например kernel language.
(Reply) (Parent) (Thread)
From: (Anonymous)
2011-01-18 03:10 pm (UTC)
И еще комбинаторное исчисление. Но мы же говорим о чем-то, что можно практически использовать? кстати, само определение функции в хаскеле - тоже спецформа, которая синтаксически не отличается от аппликации. f x = 5 - применяем функцию f к аргументам x, =, 5.
(Reply) (Parent) (Thread)
[User Picture]From: freiksenet
2011-01-18 09:43 pm (UTC)
Ну kernel language, если бы у него был рабочая имплементация, вполне был бы юзабельным.
(Reply) (Parent) (Thread)