Q: Is there some magic that GEP (the program) is doing that the exported code is not?
A: Yes, there is a lot of magic in GEP. It was made by best magicians from Gryffindor, Hogwarts using latest developments in alchemy and wizardry. It contains traces of unicorn blood, dragon eggs and jobberknoll feathers. Voodoo is actively used too, so each time you generate C++ code in GEP Bjarne Stroustrup loses a hair.

(с форума про один из наших продуктов)

С четырьмя ядрами можно не только делать ошибки в четыре раза быстрей, но и сообщать о них слаженным хором:

:)

Я в предыдущем посте всех обманул, а меня никто не поправил опять. Я сказал, что если на коммутирующей диаграмме между двумя объектами есть стрелки туда-сюда, то они получаются изоморфизмами. Однако ж нифига, и вот простой контрпример. Возьмем объект А и его произведение с самим собой АхА:

По определению произведения из АхА есть стрелки fst и snd в А, и для любого объекта (например, А), из которого тоже есть стрелки f и g в А (например, f=g=id), есть уникальная стрелка pair(f,g) из этого объекта (А) в АхА, такая, что fst . pair(f,g) = f и snd . pair(f,g) = g, т.е. fst . pair(id,id) = id.
В CPL pair(id,id) имеет тип *a -> prod(*a,*a), а fst имеет тип prod(*a,*b) -> *a, и их композиция fst . pair(id,id) равна id, это нам дает определение произведения. Но вот обратная композиция pair(id,id) . fst нифига не равна id. А значит, определение изоморфизма не вывполнено, и А не изоморфен АхА, что и следовало ожидать. Так что построение стрелок на CPL туда-сюда еще не доказывает изоморфность, нужно явно показать, что обе их композиции равны соответствующим id. Упомянутые в прошлом посте изоморфизмы, дающие арифметические законы, остаются в силе, просто обоснования там неполные, не хватает кое-каких доказательств.

А мы продолжаем передачу "теоркат для самых маленьких", в которой я рассказываю сам себе постигнутые азы. Сегодня мы увидим, как из нескольких категорных определений внезапно следуют привычные законы арифметики и как частный случай - арифметика типов. Теория категорий - это такая абстракция над теориями: мы берем какие-то теории, видим в них некоторые сущности и связи между ними, абстрагируемся от содержания (внутренней структуры) этих сущностей, концентрируясь лишь на связях между ними, и так получаем категорию (сущности становятся непрозрачными объектами, связи - стрелками между ними). Довольно разные теории при таком абстрагировании могут нам дать очень похожие категории, и доказав нечто один раз на уровне категорий, мы автоматически получаем множество теорем - по теореме для каждой из вписывающихся в эту категорию теорий. Так чуть ниже парой строк на CPL мы докажем, что

lcm(a, gcd(b,c)) == gcd(lcm(a,b), lcm(a,c))   (a,b,c - натуральные числа)
(a, Either b c) == Either (a,b) (a,c)         (a,b,c - типы данных в Хаскеле)
A & (B | C) == (A & B) | (А & C)              (A,B,C - логические высказывания)

и еще примерно 9213 теорем похожего вида.
( Read more... )

А у нас новый год! Вместо салатов, телевизора и водки - водные пушки, ковшики и шланги. Вместо санок и лыж - пикапы и байки. Четыре или пять дней гуляний, но самый обливальный день сегодня. Сфоткал сегодня рядом с домом:



( и еще чуть-чуть )

Познавательно и с юмором. Часовая лекция суперструнщика Мичио Каку о том, что нас ждет в будущем:
http://youtu.be/219YybX66MY

Пользуясь хорошей погодой и свежей версией Panorama Maker'a, понаделал круговых панорам нашей деревни.







еще несколько штук...

Вот в каких ужасных условиях приходится работать! :)

Лемму Йонеды называют самой сложной тривиальной вещью в математике. Сегодня мы попробуем закодировать ее на Окамле и понять ее связь с продолжениями (continuations). Лемма эта из теории категорий, я буду объяснять на пальцах, не слишком строго. В категории у нас есть коллекция объектов (порой очень большая, настолько, что это даже не обязательно множество) и коллекция стрелок между ними, также называемых морфизмами. Знакомый нам пример категории - где объекты это типы данных, а стрелки - функции между ними. Функтором называется отображение одной категории в другую (или в ту же, тогда это эндофунктор), сохраняющее структуру - "рисунок" стрелок. Он всякому объекту из первой категории сопоставляет некоторый объект из второй, и стрелки переносит соответственно. Конструкторы типов, вроде списка или дерева, - примеры (эндо)функторов в знакомой нам категории. Функтор "список" ('a list) отображает типы вроде int и string в типы вроде int list и string list, а функции вроде int -> string превращает в функции вроде int list -> string list. Такие вещи очень просто записываются на хаскеле, но сегодня я хочу использовать окамл, все-таки он наследник categorical abstract machine language. На окамле функтор в общем виде можно так, например, описать:

module type Functor = sig 
  type 'a t 
  val fmap : ('a -> 'b) -> 'a t -> 'b t 
end 

Это сигнатура модуля, "интерфейс". Реализуя его для конкретных конструкторов типов, вроде списка или дерева, мы получим конкретные функторы.

Если мы в некоторой категории С возьмем произвольный объект А, то ( Read more... )

Понравился кадр, что сделал на днях. Вид с острова на материк. Тут до материка 30 км: