2014-12-20

Entry tags:

type theory

theorems for free?

So far I got a feeling, that all this consists of the following:
- given a well-pointed cartesian-closed category T with, err, subobject classifier (is not it a topos?)
- define a function from objects of T to Set
- if the function preserves points, products, exponentials, then it is a functor

Am I wrong?

Entry tags:

диахронизм

у Сороса плоховато с русским...

"Чтобы вы не выбрали, профит все равно достанется лидеру."

А я кокрастыке не знаком с таким языком; читаю - и не понимаю, чо, чо?

P.S. Такое ощущение, что все этот текст воспринимают как обычный русский.

Да хер с ним с Соросом, понятно, что если Сорос что-то и говорил, то по-английски, на худой конец - по-венгерски (тогда оно Шорош); и что вата из него делает Даллеса.

ПОСТ НЕ О СОРОСЕ, окей?

Entry tags:

беларусь

ау, Беларусь!

У вас там что, весь кислород перекрыли? А гитхаб тоже?

Ну... южная граница же не закрыта пока... или партизанскими тропами, через Чернобыль...

пост-перепост (шоб мы так жили)

Автор:

nicka_startcev

Если бы человеки были гекконами, длиной этак 10-20см, то..

1. жратва стоила бы примерно столько же за килограмм, но раз в тыщщу меньше за порцию
2. население было бы не миллиард-пять, а раз в тыщщу больше
3. успешную софтину можно было бы продать тиражом этак в тыщщу раз больше, итого доходы программистов выделялись бы еще сильнее
4. программистов было бы в сотни раз больше, а значит софт допиливался бы быстрее, был менее глючен

Entry tags:

эх

темы

темы, на которые я зря ведусь

- нужна ли программисту математика (см лурк)
- какая польза от монад/моцарта/вангога/йоги/фп/линукса и т.п. ("какой мне вред от Даннинга-Крюгера")
- есть ли жизнь в России
- негры оборзели совсем
- арабы оборзели совсем

темы, на которые я уже не ведусь
- Америке кирдык
- Украине кирдык
- Европе кирдык
- о вреде политкорректности
- глобальное потепление реально/нереально

темы, на которые я не зря ведусь
- типы и категории
- красивый код
- Архангельск, Новгород, Норвегия, Исландия
- путешествия по США
- нелегкие судьбы программистов

можно бота написать

Берем любую страницу из Теории Топосов Джонстона, или, еще лучше, из его Слона, убираем слово "топос", заменяем все на типизированную лямбду, переводим все на язык ⊢ и ⊨, так что результат будет занимать уже 30 страниц - и все, готовая статья. А если взять не страницу, а главу - то и диссертация. "Теория Типов, Включающая в Себя Теорию Множеств", "Когомологии в Теории Типов", "Построение Копределов в Типизированной Лямбде", "Рекурсия и Бесконечность в Типизированной Лямбде с Семантикой Крипке".

не расчитываю, что поймут...

Короче. Навальный, конечно, молодец. Борется с коррупцией. Нормально; другие борются с невежеством, он с коррупцией; пенять ему, что неправильно борется - это как пенять Джордано Бруно, что он в чертей верил.

Но вообще-то... вообще-то я бы скорее считал, что коррупция России полезна. Она резко снижает способности России к агрессии. Пусть уж лучше строят дома в Лондоне, чем танки в Украину посылают. Бирюков, или как его там - чем больше он разграбил, тем спокойнее живется соседям. Да хоть бы и всю армию продал.

Россия опасна и для соседей, и для собственного населения; да, часть этой опасности вызвана коррупцией, но это очень маленькая часть. Без коррупции что, они бы Крым не оккупировали бы, в Донбасс да в Грузию бы не вторглись? Еще как вторглись бы. У Гитлера коррупции было относительно немного; помогло оно ему?

Да и вообще, все ж понимают, что если у коррупционера отнять его имение, то хм... то что? Туда детский дом поселят? Или другой коррупционер купит его, на закрытом аукционе, за 100 тысяч баксов? Да что ни отними, а бабушкам да сиротам все равно ни хрена не достанется; это Россия. Достойна ли эта страна того, чтобы о ее финансовых интересах так трогательно заботились?

В сущности, это как вот если бы все дружно собрались осуждать насильника за то, что он матом некрасиво ругается.