![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Scala
Читаю книжку Одерского, до основной шизы еще не добрался, но такое ощущение, что в скале чрезмерно много синтаксического сахара. Типа "тут вы можете скобки опустить, а тут вместо скобок использовать фигурные скобки, а тут мы прямо в параметрах класса сделаем их полями, а в multiline string literal вы можете сделать отступ и stripMargin" и прочая и прочая в том же духе.
Основное из этого, видимо - function literals и вызов методов в стиле a methodName b, без точек и скобок, что делает код более лаконичным, одновременно позволяя при желании превратить код в нечитабельный ад.
Заодно по наводке![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
jdevelop глянул на http://spray.io/ https://github.com/spray/spray/wiki
Примеры там, конечно, знатный abuse возможностей языка и вычислений на типах, типа extraction-директив с HList в качестве параметра типа.
Clojure по сравнению с этим выглядит более простой и логичной, хотя я не уверен, можно ли сравнивать совершенно разные языки, общего у которых только функциональщина и иммутабельность иногда.
PS: Вот, к примеру:
https://github.com/spray/spray/blob/master/docs/documentation/spray-routing/code/docs/HttpServiceExamplesSpec.scala
В SimpleService HttpResponse реализован как html-код написанный прямо внутри скала-кода.Сижу уже 30 минут ищу, где это преобразование реализовано и как. Т.е. не видя отдельных литералов и их типов (которые без загрузки всего оного кода с зависимостями в IDE/интерпретатор еще и не увидишь), с ходу догадаться, что происходит, достаточно сложно. XML literals, встроенные в язык и где-то implicit для конверсии.
PPS: implicit evidence:
http://jim-mcbeath.blogspot.com/2008/11/scala-type-infix-operators.html
http://stackoverflow.com/questions/3427345/what-do-and-mean-in-scala-2-8-and-where-are-they-documented
По-моему, это уже достаточно сложно, чтобы увлечь психов и стать новыми крестиками. Вотxeno_by еще приделает макросы - и совсем хорошо станет.
Основное из этого, видимо - function literals и вызов методов в стиле a methodName b, без точек и скобок, что делает код более лаконичным, одновременно позволяя при желании превратить код в нечитабельный ад.
Заодно по наводке
jdevelop глянул на http://spray.io/ https://github.com/spray/spray/wiki Примеры там, конечно, знатный abuse возможностей языка и вычислений на типах, типа extraction-директив с HList в качестве параметра типа.
Clojure по сравнению с этим выглядит более простой и логичной, хотя я не уверен, можно ли сравнивать совершенно разные языки, общего у которых только функциональщина и иммутабельность иногда.
PS: Вот, к примеру:
https://github.com/spray/spray/blob/master/docs/documentation/spray-routing/code/docs/HttpServiceExamplesSpec.scala
В SimpleService HttpResponse реализован как html-код написанный прямо внутри скала-кода.
PPS: implicit evidence:
http://jim-mcbeath.blogspot.com/2008/11/scala-type-infix-operators.html
http://stackoverflow.com/questions/3427345/what-do-and-mean-in-scala-2-8-and-where-are-they-documented
По-моему, это уже достаточно сложно, чтобы увлечь психов и стать новыми крестиками. Вот
xeno_by еще приделает макросы - и совсем хорошо станет.
no subject
Я не знаю, что оно значит на бесконечных списках. Каково определение "="? Можно определить рекурсивно на конечных списках - но для бесконечных оно работать не будет. Можно определить как эквивалентность термов (соответствующих нормальных форм) - но я не знаю, как проверять на эквивалентность термы, без нормальной формы (а аппенд от бесконечного списка нормальной формы не имеет).
> Переход в трансфинитной индукции таков: из предположения, что P(x) выполняется при всех x < y, выводится, что верно P(y).
Я об этом и сказал. Никакого отношения к непрерывности.
> Проблема в том, что нам нужна индукция до омеги. А вот тут вас математическая индукция не спасёт. Нужно доказать, что если что-то верно для всех конечных списков, то верно и для бесконечных.
Все дело в том, как вы определяете "=". Оно и в вашем доказательстве указанное равенство выполняется не из-за какой-то там непрерывности, а просто by-definition.
no subject
Э... вообще-то, равенство в математике присутствует изначально. Его не надо определять.
Скажите, если вас так смущает равенство, смутит ли вас отношение "для любого n элементы xs !! n и ys !! n равны"?
> но я не знаю, как проверять на эквивалентность термы
Вы всё думаете о том, как что-то проверить на компьютере. Если мы ведём рассуждения о программах, это не значит, что мы должны ограничиваться компьютерными конструкциями.
> Оно и в вашем доказательстве указанное равенство выполняется не из-за какой-то там непрерывности, а просто by-definition.
Нет.
no subject
В математике присутствует равенство множеств. Равенство любых других объектов (натуральных чисел или рациональных чисел или действительных чисел или списков или термов или чего угодно) надо определять отдельно. И это всегда делается.
> Скажите, если вас так смущает равенство, смутит ли вас отношение "для любого n элементы xs !! n и ys !! n равны"?
Определенно, смутит. Отношение должно быть задано корректно - то есть взяв любую пару списков мы должны иметь возможность сказать равны они или нет. Если же определять так как предлагаете вы, то мы сможем найти такие списки, для которых ни равенство ни неравенство в указанном вами смысле доказуемо не будет. В самом деле - мы можем взять список, который представляет конкантенацию всех ненулевых членов последовательностей Гудстейна, взятых по порядку, а потом применить к нему функцию, которая отфильтрует все ненулевые элементы списка. Потом мы сравним полученный список со списком нулей. Если теорема Гудстейна верна, то эти списки окажутся в согласии с вашим определением равны, если неверна - неравны (в результате наших манипуляций получится пустой список, следует воспользоваться свойством append xs ys = xs если xs бесконечен). Но теорема Гудстейна недоказуема в АПП. И здесь речь не о проверке - здесь речь именн оне о проверке, а именно о корректном задания отношения. То есть оно однозначно определено должно быть.
> Вы всё думаете о том, как что-то проверить на компьютере. Если мы ведём рассуждения о программах, это не значит, что мы должны ограничиваться компьютерными конструкциями.
Здесь дело не в проверке, опять же. Бета-эквивалентность вообще алгоритмически неразрешима - но я ж об этом не упоминаю. Мы просто постулируем - если нормальная форма совпадает, то термы эквивалентны. Проблема с термами не имеющими нормальной формы - в этом случае единственный логичный выход определить, что все ненормализуемые термы равны друг другу и жопе. но тогда для бесконечных списков все доказывается очень просто:
append xs append (ys zs) = (_|_) = append (append xs ys) zs, если хотя бы один из списков бесконечен.
> Нет.
Вы бы равенство для начала определили. А потом доказали что ваши утверждения про неподвижные точки и т.п. работают в частности для этого равенства.
no subject
Ничего подобного. В любой математической теории (кроме некоторых вырожденных случаев, рассматриваемых только логиками) равенство предполагается существующим изначально.
И почему вам не нравится равенство бесконечных списков, но устраивает равенство бесконечных множеств?
> Отношение должно быть задано корректно - то есть взяв любую пару списков мы должны иметь возможность сказать равны они или нет
Первая часть правильная, вторая — нет. Для корректности отношения алгоритм проверки не обязателен.
> Если же определять так как предлагаете вы, то мы сможем найти такие списки, для которых ни равенство ни неравенство в указанном вами смысле доказуемо не будет.
Ну и что? Вопрос не в том, что там доказуемо. Сможем доказать — хорошо, не сможем — ну, значит, не знаем.
> Мы просто постулируем - если нормальная форма совпадает, то термы эквивалентны
Так. Тогда чем вам не нравится вариант "для любого n элементы xs !! n и ys !! n равны"? Его тоже можно "просто постулировать".
> Проблема с термами не имеющими нормальной формы - в этом случае единственный логичный выход определить, что все ненормализуемые термы равны друг другу
Нет, конечно, потому что для разных ненормализуемых термов x и y может найтись такой терм p, что "p x" и "p y" имеют нормальные формы, но разные. Так что с логикой всё не так просто.
> А потом доказали что ваши утверждения про неподвижные точки и т.п. работают в частности для этого равенства.
Мне не нужно. Профессор Дана Скотт уже давно всё сделал за меня.
no subject
Я не понимаю, что это значит. Что такое "существует изначально"? Если есть какое-то отношение - оно должно конкретно определяться. Например - набором соответствующих аксиом, которые задают это отношение (для равенства на множествах: a = b <=> (forall x in a => x in b) and (forall x in b => x in a)). Очевидно, что мы не может просто объявить что "вот этот значок будет равенством", не прояснив свойства того значка, которым он обязан удовлетворять.
Так что извольте предоставить определение равенства. Это отношение эквивалентности, которое удовлетворяет свойствам... каким?
> И почему вам не нравится равенство бесконечных списков, но устраивает равенство бесконечных множеств?
Мне просто не нравится. Но давайте поступим конструктивно и примем предложенное определение: "для любого n элементы xs !! n и ys !! n равны".
Теперь докажите, что в согласии с этим определением append xs (append ys zs) = append (append xy yx) zs для бесконечных списков. И для конечных тоже докажите, а то старое доказательство уже не работает.
> Так. Тогда чем вам не нравится вариант "для любого n элементы xs !! n и ys !! n равны"? Его тоже можно "просто постулировать".
Мы можем разные определения "просто постулировать", да. И вариант с термами мне нравится не более чем ваш вариант с "для любого n элементы xs !! n и ys !! n равны". Но как я выше сказал - давайте примем "для любого n элементы xs !! n и ys !! n равны",
> Мне не нужно. Профессор Дана Скотт уже давно всё сделал за меня.
Безусловно, по-этому вы могли доказательство ассоциативности аппенда не приводить, а просто сказать "Профессор Дан Скоттт уже все доказал". Это, однако, не сильно конструктивно, т.к. на практике придется доказывать как раз то, что уважаемым профессором доказано еще не было. А мы ведь как раз и начали с удобства соответствующего инструментария, не так ли?
no subject
Ровно то же самое, что и в случае множеств.
> Например - набором соответствующих аксиом, которые задают это отношение (для равенства на множествах: a = b <=> (forall x in a => x in b) and (forall x in b => x in a)).
Ну, начнём с того, что данная аксиома во многих вариантах теории множеств не выполняется. Например, для теории множеств с атомами.
На самом деле, аксиомы, связанные с равенством, разумеется, существуют. Список их варьируется, но, в целом, из одного варианта всегда можно вывести другой. Фокус, однако, в том, что эти аксиомы не являются "определением равенства" и тем более не являются алгоритмом для проверки.
> Мне просто не нравится.
Простите, но с этим я ничего поделать не могу.
> Но давайте поступим конструктивно и примем предложенное определение: "для любого n элементы xs !! n и ys !! n равны".
Давайте не будем. Давайте вместо этого поймём, что "равенство" — такое же базовое понятие, как и "множество". Даже в теории категорий, где, казалось бы, изоморфные объекты можно просто отождествлять, равенство всегда присутствует.
> Это, однако, не сильно конструктивно, т.к. на практике придется доказывать как раз то, что уважаемым профессором доказано еще не было. А мы ведь как раз и начали с удобства соответствующего инструментария, не так ли?
Тьфу. Профессор Скотт доказал, что семантика доменов работает. Мы можем этим пользоваться, что я и делаю.
no subject
Если под "базовым понятием" предполагается некий объект, который не имеет определения, то разговор дальше не имеет смысла продолжать - тогда никакой ассоциативности равенства мы доказать не можем. И вообще никаких свойств "=" доказать не можем - т.к. свойства объекта можно получить лишь двумя способами - постулированием (то есть аксиомами и определениями) либо выводом из этих аксиом и определений. Если определения нет - выводить не из чего.
Вот смотрите, у вас есть два терма x_1 и x_2, вам надо доказать, что x_1 ? x_2, где ? - некоторый символ метатеории. При чем вы не знаете что это за символ и в конструкции метатеории он никак не участвует, в ее сигнатуре не отражен. Чего вы теперь делать то собираетесь с этим символом? Вы, в конце концов, даже не знаете, что это предикат - быть может "x_1 ? x_2" вообще не является синтаксически корректным высказыванием.
> что эти аксиомы не являются "определением равенства"
Именно определением они и являются. Впрочем, это уже зависит от смысла, который мы вкладываем в слово "определения". В рамках текущего обсуждения этот вопрос не актуален.