Принцип Маркова это невыводимое в интуиционистской логике предикатов утверждение, которое тем не менее выполняется в вычислительной/конструктивной интерпретации оной ( Read more... )

Создатель языка Haskell, сэр Simon Peyton Jones сейчас занимается новым поделием под названием Verse Core. Я немного получше сегодня разобрался в этой штуке, и мне кажется понимаю как вкладывать новшества этой штуки в обыкновенные языки программирования ( Read more... )

Вот бывают в программировании типы с параметром, например тип List - это списки, у которых элементы типа T.

Функция, которая может работать со списком любого типа элементов, тоже имеет параметрический тип:

reverse(list : List) : ListВ языках вроде Java параметром типа может быть только тип. Но когда система типов покруче, бывает что в качестве ( Read more... )

Я тут болею, последние ночи я очень плохо спал. И вчера наконец вкурил давным-давно лежавшую во вкладках статью по математике, которая была мне очень важна ( Read more... )

§ Зачем нужны ординалы ( Read more... )

(Этот же текст с нормальным форматированием и хайлайтингом: https://gist.github.com/akuklev/53cf44920f1ad4b0edd7d56d7ce312daRead more... )

Я поздравляю нас всех с невероятно успешным первым запуском космического корабля Starship. На слове “поздравляю” фейсбук показывает красивый фейерверк, что особенно подходит к случаю - фейерверк тоже был, на высоте 38 километров. Но дело не в фейерверке, а в том, что было до него - успешный старт и полёт Starship'а до самой стадии разделения ( Read more... )

Очень давно, примерно 2002-2003 ко мне попала нестандартная запись «Лесного оленя», она мне жутко понравилась аранжировкой, необычным подбором инструментом, соло-импровизациями в середине и в конце и голосом одной из двух исполнительниц, причём той из них которая в полный голос поёт только в припеве (отдельно его можно услышать, например на 121-123 ( Read more... )

Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning ( Read more... )

Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что так ведь так не с любой толпой ( Read more... )