![[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
Вы правы, прошу прощения. Просмотрел.
> У вас обычное доказательство по индукции
В некотором роде. Может, вы ещё сможете ответить, индукция по чему ведётся? Только не надо говорить "по длине xs" - доказательство вполне работает и при бесконечном xs.
> только усложненное "оберткой" из непрерывности, неподвижной точки и жопы.
Ну, эта "обёртка" входит в стандартный инструментарий и применяется без напряжения мозга, так что не страшно.
> Может, тогда, вы сами подберете какой-нибудь несложный пример, на котором это преимущество уже будет очевидным?
Может быть, я подумаю.
no subject
Трансфинитной индукцией по ординалам до алеф_0 включительно (все списки конечной длины). Наше утверждение соответствует алеф_1 (бесконечные списки):)
no subject
Какой кошмар.
Алеф-1 — это, если принять ГК, континуум. Откуда вы его там выкопали — я не понимаю.
А "по ординалам" — не пойдёт; грубо говоря, я хочу услышать что-то вроде "индукция по n", а вы мне говорите "индукция по натуральным числам".
no subject
List_n - списки длины
List_n - списки длины <n. Можно было брать <=n, тогда бы остановились на алеф_0. Это совершенно не существенно в нашем случае.
> А "по ординалам" — не пойдёт; грубо говоря, я хочу услышать что-то вроде "индукция по n", а вы мне говорите "индукция по натуральным числам".
По множествам списков длины не превышающей n, это дело по включению изоморфно (как вполне упорядоченное множество) ординалам до алеф_0 (раз вас смущает алеф_1 начнем с нуля :)). Т.к. нам нужен этот самый алеф_0, то индукция трансфинитная. Если ограничиться только конечными списками - тогда достаточно простой индукции.
no subject
Это вы к чему?
> Можно было брать <=n, тогда бы остановились на алеф_0. Это совершенно не существенно в нашем случае.
Может, и не существенно, но я абсолютно не понимаю, что вы имеете в виду. При чём тут вообще алефы, в особенности алеф-1?
> По множествам списков длины не превышающей n
Нет.
> это дело по включению изоморфно (как вполне упорядоченное множество)
Кто "это дело"? Множество списков? Оно не является упорядоченным вообще.
no subject
Да. Ну то есть вы, может, и имели ввиду нечто другое, но и индукции по множествам списков длины менее n вполне достаточно. По включению эти множества образуют вполне упорядоченное множество, изоморфное ординалам до алеф_0 включительно (все-таки нам надо брать List_n - списки длины <n, я выше немного поторопился, иначе у нас не будет множества соответствующего всем конечным спискам). Тогда в результате трансфинитной индукцией получаем утверждение для List_алеф_1 - что есть списки не более чем счетной длины.
no subject
То есть, по-нормальному это называется "трансфинитная индукция по длине списка".
Так вот: нифига. Прелесть в том, что вам приходится изобретать некую числовую (ординальную, кардинальную, whatever) характеристику, по которой вести индукцию. В случае списков выбор достаточно прост, но если предметом рассуждений будут, скажем, деревья, тут уже пойдут варианты - брать число вершин? число листьев? высоту?
В моём варианте индукция совершенно обычная (никакая не трансфинитная) ведётся всегда по одному и тому же: по степени, в которую возводится функция (в данном случае - функция t). И эта характеристика уже есть, она входит в построение неподвижной точки.
Кроме того, вам, чтобы сделать полноценный индукционный переход, всё равно потребуется говорить какие-то слова про непрерывность. Сейчас вы их мягко замолчали.
no subject
Гм. Да, в этом смысле получилось странно :)
Просто нам нужна именно упорядоченность, не количество элементов. А порядок - это про ординалы. Потому ими и проиндексировал, показалось более естественным :)
> Так вот: нифига. Прелесть в том, что вам приходится изобретать некую числовую (ординальную, кардинальную, whatever) характеристику, по которой вести индукцию.
Условно говоря, ординалы (ну или кардиналы :)) нужны только для индексации, вообще можно напрямую взять указанные множества списков, тривиальным образом вполне упорядочить по включению и все.
Надо тут отметить, что вообще это утверждение для бесконечных списков смысла никакого не имеет. Этот предикат в семантике Скотта будет пределом соответствующих предикатов. каждый из предикатов на конечных списков непрерывен, но непрерывность членов последовательности не влечет за собой непрерывности предела - и предикат равенства на бесконечных списках как раз не непрерывен.
> В случае списков выбор достаточно прост, но если предметом рассуждений будут, скажем, деревья, тут уже пойдут варианты - брать число вершин? число листьев? высоту?
Нам же для трансфинитной индукции достаточно фундированности, так что берем множества деревьев конкретной топологии, частично упорядочивая отношением "А есть поддерево Б".
> Кроме того, вам, чтобы сделать полноценный индукционный переход, всё равно потребуется говорить какие-то слова про непрерывность.
Нет, зачем? Индукционных переход делается чисто формальным манипулированием формулами (из одной получается другая - все, переход сделан).
no subject
Получилось нечто странное, ибо между алеф-ноль и алеф-один ординалов ещё до фига.
> вообще можно напрямую взять указанные множества списков, тривиальным образом вполне упорядочить по включению и все.
Это-то можно, но числовая характеристика вам понадобится просто для того, чтобы эти множества задать.
> Надо тут отметить, что вообще это утверждение для бесконечных списков смысла никакого не имеет.
Имеет, конечно. Просто если список xs бесконечен, то append xs ys = xs.
> Этот предикат в семантике Скотта будет пределом соответствующих предикатов. каждый из предикатов на конечных списков непрерывен, но непрерывность членов последовательности не влечет за собой непрерывности предела - и предикат равенства на бесконечных списках как раз не непрерывен.
Ничего не понял. Откуда вдруг взялась "непрерывность предикатов"?
> Нам же для трансфинитной индукции достаточно фундированности, так что берем множества деревьев конкретной топологии, частично упорядочивая отношением "А есть поддерево Б".
Да, так получится. Наверное.
> Нет, зачем? Индукционных переход делается чисто формальным манипулированием формулами (из одной получается другая - все, переход сделан).
Гм. Вы в курсе, что такое индукционный переход в трансфинитной индукции?
no subject
Да, все верно, я алефы с омегами перепутал.
> Это-то можно, но числовая характеристика вам понадобится просто для того, чтобы эти множества задать.
Она не нужна, просто любой способ построения можно объявить неявным (в той или иной мере) заданием такой числовой последовательности.
> Имеет, конечно. Просто если список xs бесконечен, то append xs ys = xs.
И это утверждение тоже не имеет никакого смысла. Т.к. "=" не определен на бесконечных списках. Не умеем мы бесконечные списки сравнивать :(
> Ничего не понял. Откуда вдруг взялась "непрерывность предикатов"?
Ну как откуда? Предикат - это функция, в данном случае функция от двух списков. "=", определенные для конечных списков, непрерывны, а для бесконечных - нет :(
> Гм. Вы в курсе, что такое индукционный переход в трансфинитной индукции?
Я не совсем понял, что вы подразумеваете под "что такое", но совершенно уверен - индукционный переход в трансфинитной индукции никакой непрерывности не требует. Он вообще требует более слабых условий, чем переход в математической, так что если выполняется переход для математической, то для трансфинитной он выполнен тем более (что вполне логично, т.к. математическая индукция есть частный случай трансфинитной).
no subject
Для меня когда-то стало откровением существование кардинала "алеф-омега".
> Т.к. "=" не определен на бесконечных списках. Не умеем мы бесконечные списки сравнивать
Э, нет. Это классическая ошибка, вы путаете внешнее "=" и внутреннея "==". Последнее, действительно, функция, для бесконечных списков расходящаяся, и, к тому же, определённая так, как программисту захочется. Вполне можно определить так, что 1 == 1 будет False.
А обычное "=" никто не мешает использовать. Его, возможно, не вычислить алгоритмом, но если мы хотим вести рассуждения о программах, нам оно понадобится.
> "=", определенные для конечных списков, непрерывны, а для бесконечных - нет
Ужас. Во-первых, опять та же путаница с "=" и "==". Во-вторых, функция (==) именно что непрерывна, как вообще все функции, которые можно определить в том же, скажем, Хаскеле, без обращения к unsafe-фокусам. В-третьих, "непрерывность для бесконечных списков" - вообще бессмысленное понятие.
> но совершенно уверен - индукционный переход в трансфинитной индукции никакой непрерывности не требует. Он вообще требует более слабых условий, чем переход в математической, так что если выполняется переход для математической, то для трансфинитной он выполнен тем более
Понятно, не знаете.
Переход в трансфинитной индукции таков: из предположения, что P(x) выполняется при всех x < y, выводится, что верно P(y).
Если мы делаем трансфинитную индукцию по ординалам, то пока y - конечный ординал, всё хорошо: для y=0 это просто база индукции, для ненулевого (но конечного) y это чуть слабее, чем обычная математическая индукция.
Проблема в том, что нам нужна индукция до омеги. А вот тут вас математическая индукция не спасёт. Нужно доказать, что если что-то верно для всех конечных списков, то верно и для бесконечных. И от непрерывности вам не убежать никак.
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" вообще не является синтаксически корректным высказыванием.
> что эти аксиомы не являются "определением равенства"
Именно определением они и являются. Впрочем, это уже зависит от смысла, который мы вкладываем в слово "определения". В рамках текущего обсуждения этот вопрос не актуален.