Здравствуйте, thesz, Вы писали:
T>Здравствуйте, LaPerouse, Вы писали:
T>>>И это проще, чем добавление "каталог:\n\tchdir каталог\nmake all"? T>>>В случае make у меня всё единообразно — есть список целей, есть способы их достижения. В случае Eclipse?.. LP>>Вот не понимаю я, при чем тут эклипс. nmake — утилита сборки, эклипс — среда разработки. Совершенно разные вещи. Я думал, что тебе тяжело сынтегрировать эклипс с nmake. А теперь я и не знаю, что думать
T>Сборка — это часть разработки. T>Кстати, влияющая на многие стороны разрабатываемого проекта.
Сборка — это сборка. И к эклипсу это не имеет никакого отношения. Все. Точка. Признай наконец-то что сказал чушь.
T>Вот скажи, ты .bat файлами пользуешься? T>Если пользуешься, они компилируются в Java байт-код? T>Так и здесь — на Agda2 ты можешь делать ответственные вещи. Из которых получаются Java классы. Которые ты используешь в других местах твоего проекта.
Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.
Социализм — это власть трудящихся и централизованная плановая экономика.
Здравствуйте, LaPerouse, Вы писали:
LP>Здравствуйте, thesz, Вы писали:
LP>>>Вим, чтобы избежать подобной судьбы, ввел два режима T>>Широта твоей неосведомлённости просто поражает. LP>А какова твоя версия появления двух режимов?
Это не моя, это общепринятая. От автора, так сказать. vi — последователь командных редакторов Unix, см. его историю.
Joy explained that the terse, single character commands and the ability to type ahead of the display were a result of the slow 300 baud modem he used when developing the software and that he wanted to be productive when the screen was painting slower than he could think.[6]
И, кстати, vi старше Emacs.
Так что тут ты неправ вообще нигде.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, LaPerouse, Вы писали:
T>>Сборка — это часть разработки. T>>Кстати, влияющая на многие стороны разрабатываемого проекта. LP>Сборка — это сборка. И к эклипсу это не имеет никакого отношения. Все. Точка. Признай наконец-то что сказал чушь.
Вообще-то имеет.
Ещё раз. Сложности сборки проектов с кодогенерацией под текущими средами разработки практически полностью блокируют её использование.
T>>Вот скажи, ты .bat файлами пользуешься? T>>Если пользуешься, они компилируются в Java байт-код? T>>Так и здесь — на Agda2 ты можешь делать ответственные вещи. Из которых получаются Java классы. Которые ты используешь в других местах твоего проекта. LP>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.
Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Здравствуйте, LaPerouse, Вы писали:
T>>>Сборка — это часть разработки. T>>>Кстати, влияющая на многие стороны разрабатываемого проекта. LP>>Сборка — это сборка. И к эклипсу это не имеет никакого отношения. Все. Точка. Признай наконец-то что сказал чушь.
T>Вообще-то имеет.
T>Ещё раз. Сложности сборки проектов с кодогенерацией под текущими средами разработки практически полностью блокируют её использование.
Это бред. Еще раз. Eclipse не имеет никакого отношения к сборке проекта. И он не осложняет сборку проекта. Вообще никак.
LP>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать. T>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере.
передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.
Социализм — это власть трудящихся и централизованная плановая экономика.
Здравствуйте, LaPerouse, Вы писали:
LP>>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.
Ты это серьёзно? Неужели ты не видишь, что в java полно boilerplate кода, от которого не избавишься из-за недостатков самого языка?
T>>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере. LP>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.
Посмотри на Agda. Java по сравнению с этим языком не дотягивает даже до ассемблера по сравнению с С.
Здравствуйте, LaPerouse, Вы писали:
LP>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.
Правда что ли?
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, LaPerouse, Вы писали:
LP>>>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.
L>Ты это серьёзно? Неужели ты не видишь, что в java полно boilerplate кода, от которого не избавишься из-за недостатков самого языка?
Видишь ли, java — объектно-ориентированный язык, а копипастный код — одно из зол, для борьбы с которой ООП и создавался. Так что зачастую такой код появляется не благодаря, а вопреки идеям, лежащим в основе языка. Но я не собираюсь петь дифирамбы объектной ориентированности и признаю, что на практике копипастный код часто имеет место быть (и у меня тоже, хотя я делаю многое, чтобы этого избежать). Но что ты предлагаешь взамен? Почему ты думаешь, что академический язычок, рядом с которым хаскель выглядит стандартом промышленного программирования, поможет легко решить эту проблему, не породив новые?
T>>>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере. LP>>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код. L>Посмотри на Agda. Java по сравнению с этим языком не дотягивает даже до ассемблера по сравнению с С.
Ну-ну. Расскажите вкратце, что оно из себя представляет. Я почитал вики и ничего не понял. Почему agda, а не epigram? И кстати, там написано, что Агда — "theorem prover". Я слабо разбираюсь во всем этом, но всегда думал, что автоматическое доказательство теорем — удел логических языков типа пролога. Ведь для формулировки теорем нужна возможность формулировать утверждения и задавать цели, которые среда будет стремиться автоматически достичь. А Agda — функциональный язык. Как так?
Социализм — это власть трудящихся и централизованная плановая экономика.
Здравствуйте, LaPerouse, Вы писали:
LP>Видишь ли, java — объектно-ориентированный язык, а копипастный код — одно из зол, для борьбы с которой ООП и создавался. Так что зачастую такой код появляется не благодаря, а вопреки идеям, лежащим в основе языка.
Во-первых, ООП создавался не для борьбы с копипастным кодом. Во-вторых, у ООП есть ряд серьёзных недостатков, хорошо об этом написано у thesz здесь.
LP>Но я не собираюсь петь дифирамбы объектной ориентированности и признаю, что на практике копипастный код часто имеет место быть (и у меня тоже, хотя я делаю многое, чтобы этого избежать).
А у Явы этих недостатков ещё больше. Отсутствие функций высшего порядка приносит просто огромную кучу бойлерплейта. Декоратор для группы строк:
public boolean startsWith(String s)
{
for (String str: strings) {
if (str.startsWith(s)) {
return true;
}
}
return false;
}
public boolean endsWith(String s)
{
for (String str: strings) {
if (str.endsWith(s)) {
return true;
}
}
return false;
}
И ещё куча таких методов, отличающихся только выделенным. Понасоздавать на каждую функцию по классу? Это проблемы языка, а не программиста. Этот код должен генериться. Ну, или копи-пастится, да
LP>Но что ты предлагаешь взамен? Почему ты думаешь, что академический язычок, рядом с которым хаскель выглядит стандартом промышленного программирования, поможет легко решить эту проблему, не породив новые?
Я не пользуюсь Agda в разработке. Но многие приёмы из неё успешно использую в Haskell.
На "Не породив новые" отвечу так — не попробовав не узнаешь.
LP>Ну-ну. Расскажите вкратце, что оно из себя представляет. Я почитал вики и ничего не понял.
Субъективно. Мне ближе его синтаксис.
LP>И кстати, там написано, что Агда — "theorem prover". Я слабо разбираюсь во всем этом, но всегда думал, что автоматическое доказательство теорем — удел логических языков типа пролога.
Есть такая изумительная штука, называется Curry-Howard изоморфизм. Это утверждение о том, что типы данных, есть аксиомы, типы функций — есть теоремы, а программмы (тело функций) — есть доказательство этих теорем. Изоморфизм там явный, его сразу видно. Так вот, в этом смысле между доказательством теоремы и написанием программы нет никакой разницы.
Я тебе уже приводил пример автоматического вывода тела функции по её типу. Этот вывод как раз и строится по аналогии с доказательством теоремы, изоморфной типу этой функции.
LP>Ведь для формулировки теорем нужна возможность формулировать утверждения и задавать цели, которые среда будет стремиться автоматически достичь. А Agda — функциональный язык. Как так?
Curry-Howard изоморфизм. Меня в своё время очень сильно зацепило. Почитай, там и примеры есть отображения.
Здравствуйте, LaPerouse, Вы писали:
T>>Вообще-то имеет. T>>Ещё раз. Сложности сборки проектов с кодогенерацией под текущими средами разработки практически полностью блокируют её использование. LP>Это бред. Еще раз. Eclipse не имеет никакого отношения к сборке проекта. И он не осложняет сборку проекта. Вообще никак.
Осложняет. Осложняет, уверяю тебя.
Нельзя взять Eclipse и сделать в нём какой угодно проект. Надо ещё всякого другого знать и использовать.
LP>>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать. T>>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере. LP>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.
Любой язык программирования является сравнимым с другим. Например, автокод сравним с Прологом, PL/1 — с Java, C# с Direct3D Shading Language. Нам же интересны результаты сравнения, а не просто факт сравнимости.
Поэтому.
Mixfix синтаксис в Java есть?
Параметрический полиморфизм в Java есть?
Функции высших порядков в Java есть?
Зависимые типы данных в Java есть?
Строгое формальное доказательство соответствия программ спецификации есть?
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, LaPerouse, Вы писали:
LP>>Видишь ли, java — объектно-ориентированный язык, а копипастный код — одно из зол, для борьбы с которой ООП и создавался. Так что зачастую такой код появляется не благодаря, а вопреки идеям, лежащим в основе языка.
L>Во-первых, ООП создавался не для борьбы с копипастным кодом.
Здесь вообще мало говорится о том, почему он появился.
L>Во-вторых, у ООП есть ряд серьёзных недостатков, хорошо об этом написано у thesz здесь.
Здесь практически ничего не написано.
LP>>Но я не собираюсь петь дифирамбы объектной ориентированности и признаю, что на практике копипастный код часто имеет место быть (и у меня тоже, хотя я делаю многое, чтобы этого избежать). L>А у Явы этих недостатков ещё больше. Отсутствие функций высшего порядка приносит просто огромную кучу бойлерплейта. Декоратор для группы строк:
Пиши так:
public boolean startsWith(final String s)
{
return atLeastOne(new Predicate<String>() {
public boolean predicate(String str)
{
return str.startsWith(s);
}
});
}
public boolean endsWith(final String s)
{
return atLeastOne(new Predicate<String>() {
public boolean predicate(String str)
{
return str.startsWith(s);
}
});
}
private boolean atLeastOne(Predicate<String> predicate)
{
for (String str: strings) {
if (predicate.predicate(str))
{
return true;
}
}
return false;
}
Predicate<T> определяется один раз и его хватает очень намного
public interface Predicate <T>
{
boolean predicate(T object);
}
L>И ещё куча таких методов, отличающихся только выделенным. Понасоздавать на каждую функцию по классу?
Да нет, использовать то, что есть. И просить у Sun сделать ФВП в 7-ой яве
L>Так не бывает. Что именно ты не понял? Dependently Typed Programming in Agda читал?
Да я ничего не понял, честное слово. Не читал.
LP>>И кстати, там написано, что Агда — "theorem prover". Я слабо разбираюсь во всем этом, но всегда думал, что автоматическое доказательство теорем — удел логических языков типа пролога.
L>Есть такая изумительная штука, называется Curry-Howard изоморфизм. Это утверждение о том, что типы данных, есть аксиомы, типы функций — есть теоремы, а программмы (тело функций) — есть доказательство этих теорем. Изоморфизм там явный, его сразу видно. Так вот, в этом смысле между доказательством теоремы и написанием программы нет никакой разницы.
Ладно, спасибо за ссылки, просто с этим надо очень серъезно разбираться. С ходу понять не получается (по крайней мере у меня).
Социализм — это власть трудящихся и централизованная плановая экономика.
The idea occurred to them of grouping the different types of ships into different classes of objects; each class of objects being responsible for defining its own data and behavior
L>>Во-вторых, у ООП есть ряд серьёзных недостатков, хорошо об этом написано у thesz здесь. LP>Здесь практически ничего не написано.
С наследованием, классами и ООП целиком обязательно ассоциируется, во-первых, неявная диспетчеризация по первому аргументу функции, во-вторых, группировка методов вокруг классов и, в-третьих, но не в последних по значению, открытые типы данных
LP>>>Но я не собираюсь петь дифирамбы объектной ориентированности и признаю, что на практике копипастный код часто имеет место быть (и у меня тоже, хотя я делаю многое, чтобы этого избежать). L>>А у Явы этих недостатков ещё больше. Отсутствие функций высшего порядка приносит просто огромную кучу бойлерплейта. Декоратор для группы строк:
LP>Пиши так:
Ну, когда я первый раз на ФП посмотрел, я так и писал Только согласись, что
1. Кода меньше не стало
2. От бойдерплейта мы не избавились (заменили цикл на объявление локал класса)
3. У тебя ошибка в коде связанная с копи-пастом
4. На языках, поддерживающих ФВП первые три пункта отсутствовали бы как класс:
endsWith = any . endsWith
startsWith = any . startsWith
Ой! Тут тоже бойлерплейт! Да, но в этом языке его можно удалить:
LP>Predicate<T> определяется один раз и его хватает очень намного
Да не хватает их ни фига. Я пример ещё тривиальный привёл. Для стандартных классов можно нагенерить Function2<T,A,R> и использовать. Но тут мы просто разделяем сложность. Клиенту то попроще будет, а вот библиотеку такую писать — сложнее.
L>>И ещё куча таких методов, отличающихся только выделенным. Понасоздавать на каждую функцию по классу? LP>Да нет, использовать то, что есть. И просить у Sun сделать ФВП в 7-ой яве
+1. А потом просить карринг, а потом ленивость..
L>>Так не бывает. Что именно ты не понял? Dependently Typed Programming in Agda читал? LP>Да я ничего не понял, честное слово. Не читал.
Ну почитай, тогда вернёмся.
LP>Ладно, спасибо за ссылки, просто с этим надо очень серъезно разбираться. С ходу понять не получается (по крайней мере у меня).
Я думаю, с первого раза даже у thesz не получалось
Здравствуйте, LaPerouse, Вы писали:
LP>По сравнению с вышеперечисленным хардкорная работа в обычном текстовом редакторе выглядит прошлым веком. Вимы и емаксы кажутся настолько архаичными, примитивными и неудобными, что заставить себя набрать в них хотя бы двадцать строчек кода уже не могу (раньше мог).
У тебя какое-то странное представление о работе в vim/emacs.
Что будем называть IDE? Если IDE это Integrated Development Environment, то в этом смысле, настроенные vim/emacs — тоже вполне себе IDE.
Автокомплит кода там есть. Правда, он не такой продвинутый, как, например, в Visual Studio, но в принципе — хватает. Особенно, если использовать CEDET (для emacs) — тогда это уже дополнение не просто по словам, а контекстно-зависимое, "умное дополнение". Хотя там ещё есть что усовершенствовать.
Некоторая интеграция с отладчиком и переход на строчки с ошибками компиляции — есть.
Переход к месту объявления функции/переменной, перечисление мест, где функция или переменная используется — всё это есть.
Некоторые ошибки — подсвечиваются во время редактирования(непарные скобки, например). Некоторые — нет. Кстати, в том же emacs есть некоторые любопытные функции, которых я пока не видел в "больших IDE" — например, принудительное форматирование блока кода. Иногда это помогает заметить логические ошибки в чужом коде. Хотя сейчас большинство IDE форматируют код при наборе, так что для новых проектов это становится неактуально.
Посему, не стоит думать что vim/emacs так уж кардинально отстают от других IDE по функциональности. В тоже время, "готовые" IDE зачастую сильно завязаны на конкретный компилятор, систему сборки и т.д. Например, в том проекте, над которым я сейчас работаю, этим летом сборку перевели на мейкфайлы. Соответственно, Visual Studio их не понимает и некорректно подсвечивает активные/неактивные участки кода.
С уважением, Artem Korneev.
Re[20]: Жизнь без IDE
От:
Аноним
Дата:
01.11.09 09:58
Оценка:
Здравствуйте, thesz, Вы писали:
T>Строгое формальное доказательство соответствия программ спецификации есть?
Здравствуйте, Аноним, Вы писали:
А>Здравствуйте, thesz, Вы писали:
T>>Строгое формальное доказательство соответствия программ спецификации есть?
А>http://krakatoa.lri.fr/
А для описания спецификаций учить дополнительный язык, Java Modeling Language? Который разбирается Krakatoa, который передает результат в Why, который вызывает прувер, например, COQ, чтобы проверить все спецификации?
Спасибо, но если от меня потребуют доказано соответствующий спецификации код, я лучше непосредственно из COQ нагенерю хаскельный код с приложенным доказательством корректности, или на Agda2 напишу.
Тем более, что наличие в этом JML аннотаций типа pure, подсказывает мне, что стандартный императивный джавовский дизайн всё равно менять придется.
Re[22]: Жизнь без IDE
От:
Аноним
Дата:
01.11.09 11:01
Оценка:
Здравствуйте, deniok, Вы писали:
D>Спасибо, но если от меня потребуют доказано соответствующий спецификации код, я лучше непосредственно из COQ нагенерю хаскельный код с приложенным доказательством корректности, или на Agda2 напишу.
А если, извините, требуется код на Java? Вот требуется, и всё тут? Тогда уж лучше так, чем совсем без аннотаций.
D>Тем более, что наличие в этом JML аннотаций типа pure, подсказывает мне, что стандартный императивный джавовский дизайн всё равно менять придется.
Здравствуйте, Аноним, Вы писали:
А>Здравствуйте, deniok, Вы писали:
D>>Спасибо, но если от меня потребуют доказано соответствующий спецификации код, я лучше непосредственно из COQ нагенерю хаскельный код с приложенным доказательством корректности, или на Agda2 напишу.
А> А если, извините, требуется код на Java? Вот требуется, и всё тут? Тогда уж лучше так, чем совсем без аннотаций.
Не, ну если потребуется код, скажем, на брэйнфаке, то придется и на брэйнфаке писать (но если никто не видит можно не писать, а генерировать, а потом сказать, что написал ). Речь же выше шла о тезисе
java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код
Re[24]: Жизнь без IDE
От:
Аноним
Дата:
01.11.09 11:29
Оценка:
Здравствуйте, deniok, Вы писали:
D>Не, ну если потребуется код, скажем, на брэйнфаке, то придется и на брэйнфаке писать (но если никто не видит можно не писать, а генерировать, а потом сказать, что написал ). Речь же выше шла о тезисе D>
D> java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код
Речь выше шла о тезисе, что средств формальной верификации для Java нет. Я же говорю, что таки есть.