Scala
Читаю книжку Одерского, до основной шизы еще не добрался, но такое ощущение, что в скале чрезмерно много синтаксического сахара. Типа "тут вы можете скобки опустить, а тут вместо скобок использовать фигурные скобки, а тут мы прямо в параметрах класса сделаем их полями, а в multiline string literal вы можете сделать отступ и stripMargin" и прочая и прочая в том же духе.
Основное из этого, видимо - 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-код написанный прямо внутри скала-кода.Сижу уже 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, без точек и скобок, что делает код более лаконичным, одновременно позволяя при желании превратить код в нечитабельный ад.
Заодно по наводке
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
Примеры там, конечно, знатный 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
По-моему, это уже достаточно сложно, чтобы увлечь психов и стать новыми крестиками. Вот
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
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" вообще не является синтаксически корректным высказыванием.
> что эти аксиомы не являются "определением равенства"
Именно определением они и являются. Впрочем, это уже зависит от смысла, который мы вкладываем в слово "определения". В рамках текущего обсуждения этот вопрос не актуален.