заметки на полях (фильтрации)

[thedeemon]

На языках программирования можно ввести отношение частичного порядка "А < Б", когда с языка А на язык Б пересесть можно, и это ощущается как прогресс, а вот обратно возвращаться очень неохота и мучительно. Если не ошибаюсь, lionet в свое время заметил, что в этом отношении заметны две вершины - хаскель и лисп, с их высоты все остальные языки кажутся недостаточно хорошими. Но занятно другое: у этого отношения есть также два дна, по сравнению с которыми все другие языки выглядят превосходными, - это PHP и C++. :)

После ряда других языков мне заставить себя писать что-то на С++ очень сложно, но иногда такая необходимость возникает. Помогает сгладить моральные мучения лишь возможность найти в языке крупицы чего-то хорошего. Нынче вот взялся за новую реализацию своего фирменного super resolution движка, и что меня сейчас радует и выручает, это присутствующие в языке элементы зависимых типов. У меня код оперирует блоками разных размеров и векторами разной точности: это могут быть целые координаты в кадре низкого разрешения, в кадре высокого разрешения, а также координаты с полупиксельной и четвертьпиксельной точностью. Плюсовые шаблоны позволили описать эти вещи как семейства типов, индексированные целочисленными значениями, т.е. натурально зависимые типы получились:

#define VP_LOWRES  1
#define VP_HIRES   2
#define VP_HALF    3
#define VP_QUARTER 4

template <int Prec>
class Vec
{
public:
    int x, y;

    Vec(int vx, int vy) : x(vx), y(vy) {}
    Vec operator+(Vec<int Prec> &a) { return Vec<Prec>(x + a.x, y + a.y); }
    Vec operator-(Vec<int Prec> &a) { return Vec<Prec>(x - a.x, y - a.y); }
    Vec<Prec + 1> refine()          { return Vec<Prec + 1>(x*2, y*2); }
    ...
};

class Plane
{
    ...
    template<int W> void readBlockQP(Vec<VP_QUARTER> v, MonoBlock<W> &block);
    ...
}

В результате блоки разного размера - это разные типы, и векторы разной точности - разные типы, реально очень помогает не запутаться. Плюс компилятору подспорье: у многих циклов число итераций теперь известно статически, можно хорошо оптимизировать. В иных языках для таких вещей можно использовать phantom types, но там может быть сложнее сделать функцию refine, переводящую вектор на следующий уровень точности, в соседний слой семейства. Все-таки очень удобно, когда с параметром типа можно делать всякую арифметику и использовать его сразу на двух уровнях: типов и выражений.

К слову о зависимых типах. Одна тривиальная мысль о них мне лично оказалась весьма полезной для понимания. Мы привыкли в функциональных языках обозначать тип функции из А в В как А -> B, где А и В какие-то конкретные типы вроде Bool и Int, элементами которых служат значения вроде true и 2. Теперь добавим в систему типов еще один тип, назовем его Type, элементами которого являются типы. Тогда A -> Type будет просто типом функции, которая каждому элементу А сопоставляет какой-то тип. Это и получится зависимый тип, и именно так он и обозначается в соответствующих языках. Например, пишут B : A -> Type и говорят, что В - это зависимый от А тип, или семейство типов, индексированное значениями из А. Но эту же запись можно воспринимать и буквально - как обычную функцию, просто кодомен у нее не совсем обычный.

Comments

[thedeemon.livejournal.com]

Ничего подобного. Нас очень даже интересует получаемый тип, нельзя вместо В подставлять что угодно. Если у нас есть функция из Int в Int, мы же не можем просто проигнорировать ее работу и заменить любой другой подобного типа, заменить инкремент на декремент, скажем. B - тоже обычная функция, ее тоже нельзя заменить на другую с похожим типом. Нам важно, что она возвращает, мы ее используем при описании Пи-типов, например.

Вон в посте пример на С++, там А это int, а В это Vec<int W>. Получаются вполне конкретные типы, с ними мы потом работаем.

[sassa-nf.livejournal.com]

мне кажется, я просто не могу объяснить свою интуицию.

B : A -> Type заявляет о существовании типа, возвращаемого B. Мы не говорим, что это за тип - монада, функтор, список, вектор. Нам всё равно. Какую реализацию B дадут, такое и будет на выходе. И пример с "B это Vec<int W>" как раз и демонстрирует.

Моя аналогия рухнет, если нельзя переписать B: A->Type в виде using (X:Type, Y:Type) B: X->Y

[thedeemon.livejournal.com]

Нам может быть все равно лишь в сильно полиморфных функциях. А в иных может быть совсем не все равно, мы можем рассчитывать на конкретные типы, возвращаемые В. Вот компилирующийся и работающий пример:

B : Bool -> Type
B True = Int
B False = String

f : (x : Bool) -> B x
f True = 4
f False = "good morning"

g : Bool -> ((x : Bool) -> B x) -> String
g True f = show $ f True
g False f = f False

Тут В - зависимый тип (функция, возвращающая пространство), а f имеет пи-тип (функция, возвращающая точку в нем).

Я когда выше писал A -> Type, говорил, что А это конкретный тип, без обобщений "для любого А", может быть тут мы в разные стороны мыслями пошли.

[sassa-nf.livejournal.com]

спасибо, хороший пример. Я хотел выразить мысль, что пишем Type потому, что не можем указать "co-product of Int and String" более точно, не ссылаясь на самого себя. Но сейчас мне понятна ошибочность моей аналогии.