Category: литература

Category was added automatically. Read all entries about "литература".

Vash

options = options || {}; или обращение к говнокодерам на JS

Давайте поговорим про джаваскрипт. А точнее, про омерзительную традицию, которая лезет во все библиотеки npm из тормозного насквозь jQuery: про передачу аргументов ассоциативным массивом.

Ребята, зачем так делать? Я понимаю, что упоротые по никсам программисты не получают никакого когнитивного диссонанса, говоря про unix way и single responsibility, делая программы с туевой хучей аргументов командной строки, и потом пытаясь через man man понять, как ими пользоваться, через history вспомнить, как это, блядь, делалось, и через лишний пробел в rm почистить себе весь диск. Но должны же быть адекватные люди, да?

Ребята, этот подход не модульный. Вы никогда не вынесете в опции всё, что мне хотелось бы пофиксить внутри вашей убогой библиотеки. Зачем, зачем вы продолжаете это делать? У вашего кода слишком маленький memory footprint? Он слишком мало тормозит? JIT слишком хорошо понимает, как убрать оттуда весь дохлый код, которого у вас там 90% для отдельного применения либы?

Ботайте, блин, Хаскелл, делайте комбинаторы, экспозьте API из элементарных запчастей, пусть пользователь собирает.
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