Vash

Ненавижу никсы

В продолжение к. Ставим из хакеджа либу для написания клиентов для selenium.

C:\Documents and Settings\*>cabal install webdriver
Resolving dependencies...
Configuring network-2.4.1.0...
cabal: The package has a './configure' script. This requires a Unix compatibility toolchain such as MinGW+MSYS or Cygwin. (какого хера? я под виндой!)
Configuring unix-2.6.0.1... (ваще упоролись такие зависимости делать?)
cabal: The package has a './configure' script. This requires a Unix compatibility toolchain such as MinGW+MSYS or Cygwin.
cabal: Error: some packages failed to install:
HTTP-4000.2.8 depends on network-2.4.1.0 which failed to install.
filesystem-trees-0.1.0.3 depends on unix-2.6.0.1 which failed to install.
network-2.4.1.0 failed during the configure step. The exception was: ExitFailure 1
unix-2.6.0.1 failed during the configure step. The exception was: ExitFailure 1
webdriver-0.5.0.1 depends on unix-2.6.0.1 which failed to install.

Офигенно. Нужен msys. Ищем солюшн. Вторая линка сдохла. Устанавливая msys с первой ссылки, я понял, что ненавижу никсы вдвойне, ибо

C:\msys\1.0\postinstall>..\bin\sh.exe pi.sh
This is a post install process that will try to normalize between your MinGW install if any as well as your previous MSYS installs if any.  I don't have any traps as aborts will not hurt anything. Do you wish to continue with the post install? [yn ] y
Do you have MinGW installed? [yn ] y
Please answer the following in the form of c:/foo/bar.
Where is your MinGW installation? C:/Program Files/Haskell Platform/2012.4.0.0/mingw
pi.sh: line 22: [: too many arguments
I could not find C:/Program Files/Haskell Platform/2012.4.0.0/mingw/bin/gcc.exe (который там, естественно, есть).

Необходимость писать косые в другую сторону простить можно. Но посоны, я попробовал и с двойными кавычками, и по-всякому, ну не работает это говнище. Оно чо, пробелы в пути разобрать не может? Ну хер с вами, но зачем папку postinstall удалять сразу после завершения скрипта? Чтобы я ещё и исправить бажные sh-скрипты не мог? Если чо, переставить платформу в другое место не могу, у меня от неё Agda зависит.

Короче говоря, спасибо никсам за это ощущение восьмидесятых. Пойду багтрекеры пинать.
Vash

Обобщённые стрелки

Предупреждение: дальше по тексту зачастую будет утверждаться какое-нибудь X, однако никаких исследований по этому поводу не проводилось никем и никогда. Поэтому вопросы вроде "c чего ты взял, что Х -- обобщённая стрелка", скорее всего, останутся с ответом "потому что попой чую" или вовсе без оного.

У вас есть некоторый язык программирования.
Вы хотите в нём воспользоваться имеющимся синтаксисом для некоторой хитрой цели.
К примеру, вы кодогенерируете джаваскрипт.
Вам нужен, таким образом, способ перегрузки оригинального синтаксиса.
Существуют языки, где вы можете получить AST некоторого фрагмента кода, поменять его и сделать обратно кодом. Например, Лисп, Хаскелл и Скала.
Такую возможность называют "макросы", саму дисциплину -- метапрограммирование.
Писать AST вручную, если мы что-нибудь генерируем, неприятно.
Нам хотелось бы иметь возможности из почти исходного синтаксиса генерировать неполные AST (c дырками).
Такая возможность называется квазиквотированием.
Но что-либо серьёзное в этом ключе написать всё равно сложно.
Не вполне понятно, в каком именно месте здесь включается типизация, например.
Удостовериться, что данный фрагмент кода генерирует AST с корректными типами всегда, невозможно.
Для этого придётся проводить что-то вроде статического анализа над генерирующим AST кодом.
Учитывая, что используется оригинальный язык, а он обычно Тьюринг-полон, получаем неразрешимую задачу.
Доказывать корректность таких кодогенераторов в общем случае сложно.
Это "вжжж" неспроста.
Рассмотренный ранее подход к метапрограммированию называется интенсиональным.
Существуют ещё и не-интенсиональные подходы, и я знаю из них только один.
Обобщённые стрелки.
Для них в общем случае нужна поддержка интерпретатором или компилятором.
Программа при трансляции переводится в язык из небольшого набора комбинаторов.
Пользователю предоставляется возможность эти комбинаторы переопределять на некотором фрагменте кода.
Чтобы всё было в порядке, комбинаторы поставляются с набором аксиом, которым они должны удовлетворять.
Теперь к подробностям.
Разные программы требуют различного набора комбинаторов.
Если в программе есть несколько переменных, её представление требует комбинаторов, которые работают с парами (типами-произведениями), например, first : (a -(x)> b) -> ((a, c) -(x)> (b, c)). Этот first должен удовлетворять кое-каким аксиомам.
Если одна переменная может использоваться дважды, нужен dup : a -(x)> (a, a).
Если в языке есть литералы целых, нужно что-то вроде int : () -(x)> Int.
Чтобы появился этот (), нужен ещё набор примитивов типа uncancel_l : a -(x)-> ((), a), uncancel_r : a -(x)> (a, ()).
Ну вы поняли идею, да? Шинкуем язык на комбинаторы и типа всё.
На самом деле, мы можем нашинковать исходный язык на комбинаторы многими способами.
Например, если в языке мы можем объявлять рекурсивные функции, то мы можем добавить комбинатор fix, он же loop.
В то же время, если бы в нашем языке была возможна только "хорошая" убывающая рекурсия по натуральным числам, мы могли бы объявить в качестве примитива natrec.
Но ничто нам не мешает иметь и то, и другое одновременно.
Просто данный код будет транслироваться в потенциально разные наборы комбинаторов в зависимости от того, акие комбинаторы мы перегрузили в данном фрагменте кода.
Например, факториал будет иметь возможность транслироваться в natrec, если мы запускаем его в доказанно завершимом контексте, или fix, если мы запускаем его в контексте трансляции в JS.
И ещё: наборы комбинаторов это type class'ы.
Ознакомиться с классическими можно, изучив (необобщённые) стрелки: Arrow, ArrowChoice, ArrowApply, ArrowLoop
Этих наборов целая решётка.

Чтобы добавить возможность трансляции кода в новый набор комбинаторов, в общем случае нужно менять компилятор.
В редких случаях достаточно будет обычных определений (если примитивы стрелки это обычные функции).
Ситуацию можно улучшить, если добавить в язык поддержку (более мощного, но опасного) классического интенсионального метапрограммирования, с которого начался рассказ.
Тогда самые коварные стрелки, которые не требуют менять синтаксическую структуру языка (примитивы стрелки выглядят как обычные функции за исключением того, что не типизируются, например. к таковым относится стрелка ранк-н типизации).
Чтобы максимально усилить такой подход, есть смысл добавить в язык mixfix-нотацию, а, возможно, и позволить определять новые типы абстракций (кроме лямбда-абстракции есть ещё дифференцирование, пределы, решение уравнения относительно производной, мю-типы и пр.)

Стрелки (необобщённые) были разработаны, в том числе, для создания эффективных парсеров (Swierstra & Duponchel). Дело в том, что стрелка a ~> b это что-то вроде функции a -> b или около того, но она дополнительно может хранить какие-нибудь данные.
data Something a b = Something AdditionalData (a -> [b])
Это, кстати, позволяет решить одну очень больную проблему для других языков.
Представьте себе, что вы можете произвести некоторые затратные вычисления при запуске программы, а потом пользоваться результатами. Например, посчитать таблицы синусов для дальнейшего использования в генерации объёмных сферических объектов или меш нужной детализации по функции, как это делают в демо-сценах
Вы затем хотите вынести этот функционал в библиотеку и обнаруживаете, что не знаете, стоит ли вам вызывать эти вычисления (обычно в конструкторе соотв. класса), так как вы не знаете, будут ли они использованы в пользовательском коде.
Можно сделать это в стиле синглетона, но это породит +1 if (и лишние +5% прочистки конвеера), а также в исполнимый файл может попасть код, который никогда не будет вызван (оптимизатор может его и удалить, но он не тотальный, задача поиска мёртвого кода неразрешимая же).

Самое главное: обобщённые стрелки позволяют создать действительно универсальный язык.
Обычно когда в языке X не хватает Y, кто-нибудь берёт и делает X+Y.
Например, с чего бы от С++ ответвляться всяким PHP?
Нужна была весьма специфическая среда для кода (хорошие встроенные строки, например).
В то же время, несмотря на почти идентичность синтаксиса, в язык были внесены изменения.
Теперь библиотеки для С++ нельзя просто так взять и использовать в PHP и наоборот.
В случае языка со встроенными обобщёнными стрелками нужно было бы просто создать подходящую стрелку, которая работает с server state, session state и чем-нибудь там ещё.
Скорее всего, для такой стрелки не понадобилось бы даже менять компилятор.
Вся кодовая база была бы доступна. Весь старый синтаксис бы работал.

Впрочем, если такой язык написать, то можно будет решить проблему вавилонской башни посредством кодогенерирующих инстансов соответствующих стрелок.
Собственно, ваш покорный слуга шёл к этому 7 лет (из них 6.5 вокруг да около сабжа; нельзя просто так взять и самому придумать обобщённые стрелки, их должен придумать кто-то другой, а кто-то третий -- рассказать), и собирается это таки сделать :)
Интуиции в таком подходе к разработке ЯП мне сильно не хватает, и достать её, в общем-то, особо негде.

Ещё немного интуиции могут дать списки того, за что могут отвечать классы и инстансы обобщённых стрелок.
Классы:
"жонглирование" переменными
использование переменной более одного раза
неподвижная точка / цикл
определение функции
выведение типа
императивные включения (присваивания, ссылки)
рефлексия (получение имён типов и переменных)

Инстансы:
хост-язык (этот инстанс неявно скармливается функции main)
парсеры
кодогенераторы (fix генерирует рекурсивные вызовы, let генерирует заголовки функций, ...)
    CUDA
    шейдеры
    JS, CSS, HTML, PHP
    С++
    заголовки .h для dll сразу из определения функций
    VHDL и Verilog
    электрические схемы (цифровые и аналоговые)
    изображения (векторная графика, генеративное моделирование, SVG)
специализатор (упрощает pow(x, 2) до \x -> x * x)
инлайнер
оптимизаторы
неявное распараллеливание
трансляторы

Хотелось бы поблагодарить ребе akuklev за разъяснение мне этого дела, камрада tomotom за то, что не устаёт слушать мой больной бред и гуру sharpc за лучи ненависти к ФП и стратегию "заткнись и пиши" :)
Vash

PEG Lexer + PEG Parser

Что-то руки до ЖЖ вообще не доходят.
Вот, налабал тут гибрид слона и бегемота.
Да, я в курсе, что в Parsec есть своя собственная шняга для лексеров.
Гляжу сейчас как это можно сделать в духе катаморфизмов, алгебр и модульных интерпретаторов, ЕВПОЧЯ.
Vash

PEG не масштабируются

Если я хочу в одном языке иметь как let v = e in e, так и переменные с именами вроде letlet, мне нужно написать
'let' (' ' var ... | \w+ ...)
и обрабатывать оба варианта выбора как разные конструкции (let или переменная). Зашибись полезная вещь эти ваши PEG.

Пруф:
http://pegjs.majda.cz/online
start = "let" / "let" "let"
> letlet
< Line 1, column 4: Expected end of input but "l" found.
Строки-то один раз читаются. Вот и говорю я, зашибись полезны эти ваши PEG.
Vash

(no subject)

Сводятся ли все неразрешимые задачи к проверке на равенство двух бесконечных последовательностей натуральных чисел?
Vash

Set : Set

Наконец-то относительно разобрался с сабжем.
Возьмём некоторую систему типов, в которой
1) типы описывают области определения функций-суждений (_+_ не работает с Tree)
2) можно делать функции, которые работают над всеми суждениями, т.е. Set : Set (для любого P(.) верно, что существуют A и B, такие что P(A) = P(B))
3) суждения = типы
В ней мы можем сформулировать парадокс Жирара и доказать False. Впрочем, я с этой конструкцией так и не разобрался, даже в упрощённом виде. Существует два подхода к тому, чтобы заставить соответствие Карри-Ховарда работать в такой системе. Мартин-Лёф выбросил пункт 2 (т.е. Set : Set), а Коканд выбросил пункт 3, и в CoC верно, что Prop : Prop, но Prop != Set. Так что через Prop : Prop доказать False таки нельзя. Фух.

Список литературы.
http://plato.stanford.edu/entries/type-theory/
http://mathoverflow.net/questions/18089/what-is-the-manner-of-inconsistency-of-girards-paradox-in-martin-lof-type-theory
Vash

Ассоциативность

Думаю, вы уже слышали про "два подхода" к ассоциативности из математики и программирования. Недавно пришлось решать одну задачу, и стало ясно, что подход на самом деле один.

"Неассоциативность" (пр-е)
a :- b :- c писать нельзя, потому что по умолчанию это не a :- (b :- c) и не (a :- b) :- c

"Левоассоциативность" (пр-е)
a - b - c = (a - b) - c

"Правоассоциативность" (пр-е)
a : b : c = a : (b : c)

"Ассоциативность" (математика)
Это левоассоциативность и правоассоциативность одновременно.
a + b + c = (a + b) + c
a + b + c = a + (b + c)
=>
(a + b) + c = a + (b + c)

Таким образом, ассоциативность как свойство это пара из двух булевых констант.

Как это можно использовать? Для печати AST выражений, например. Есть проблема: в выражении не один оператор. Нам понадобятся ещё и приоритеты. Обозначим свойства оператора op:
1) priority(op) : Integer
2) left_assoc(op) : Bool 
3) right_assoc(op) : Bool.

Приоритет и ассоциативность образуют вместе что-то вроде лексикографического порядка, где приоритет идёт "раньше в слове".
В левой(правой) позиции от наружного оператора мы можем записать внутренний оператор без скобок, если либо у внутреннего оператора приоритет больше, либо если приоритеты равны, и оба оператора лево(право)ассоциативны.

Пусть P[|...|] это функция печати AST. Из вышесказанного следует, что её нужно реализовать так.
test(assoc, op1, op2) = priority(op2) > priority(op1) || priority(op2) == priority(op1) && assoc(op1) && assoc(op2)
op1( P[| op2(a, b) |], c ) =
        a op2 b op1 c, если test(left_assoc, op1, op2)
        (a op2 b) op1 c, иначе
op1( a, P[| op2(b, c) |] ) =
        a op1 b op2 c, если test(right_assoc, op1, op2)
        a op1 (b op2 c), иначе
Под нотацией "op1( P[| ... |], c )" подразумевалось, что нам известен контекст, в котором происходит печать, т.е. какой оператор стоит снаружи. В настоящем коде его нужно передать явно.

Приложение.
Из знакомства с теорией типов или логикой или чем-там-ещё многие знают, что a -> b это ba и подчиняется тем же законам.
Также известно, что (->) это (по хорошему, если мы хотим "каррирование" (независимо от его смысла в данной теории)) правоассоциативная операция. a -> (b -> c) = (cb)a = cba
Из этого можно сделать вывод: чтобы возведение в степень вело себя "правильно", следует задавать его левоассоциативным, а не как в Python.
Vash

Ошибки в дизайне С++?

1) Как создать динамический массив на стеке?*
2) Как через new запросить столько байтов на куче, чтобы через placement new можно было разместить там массив int'ов из N элементов? Другими словами, как посчитать количество байт, требуемое на заголовок, создаваемый new []?*

* Конечно же, всё по стандарту.