No title

Anonymous Coward 2018-03-03 22:11:09.910544 UTC

Ненавижу писать длинные технические сообщения в вк. Вот то ли дело в Slack -- там тебе даже
Markdown есть, очень удобно, хотет в вк. Ну не суть, будет тут.

Так вот, идея довольно простая (и, говорят, невероятно боянистая и на практике особо не едет, но извините).
Расширим систему типов так, чтобы каждый тип представлял из себя пару -- <t, s>, где t -- старый честный тип,
а s -- множество утверждений в некоторой системе формальной логики и арифметики.
Например, обычный старый тип int будет представлен как <int, {}>, то есть старый тип и пустое множество утверждений.
А вот такой int, который может хранить только положительные значения будет иметь тип <int, {_ > 0}>
(где _ -- крайне неудачное рабочее название для self, то есть самого себя). Дальше на это можно навернуть
безумную теорию зависимых типов и сделать, например, вот такую функцию:

fun (x: <int, {}>, y: <int, {_ > x}>)

Такая функция принимает только такие пары интов, где второй больше первого. Полезно? Ну пока как-то непонятно.
Проще, конечно, смотреть на примерах.

Пример первый, тупой (и непонятно, зачем нужный):

fun factorial(n: <int, {_ >= 0}>): <int, {_ > 0}> {
    if (n == 0) return 1;
    return n * factorial(n - 1);
}

Что  тут происходит? Функция факториала принимает обязательно неотрицательное число (и это должно быть доказано на этапе
компиляции, что оно неотрицательное). Например, factorial(read_int()) не должен компилироваться, потому что read_int() 
может вернуть любой int, то есть имеет тип <int, {}>, а factorial принимает <int, {_ >= 0}>. Первое не является подтипом
второго (является надтипом, на самом деле), поэтому это не компилируется. Тогда как работает этот пример? Пусть нам на вход
дали правильный n >= 0. Сначала проверим n == 0. Если да, то вернем 1. К слову, мы еще обязались возвращать строго положительные
числа, потому что возвращаемый тип функции factorial это <int, {_ > 0}>. Почему тогда мы можем вернуть 1? Какой вообще тип
имеет константа 1? А она имеет очень увлекательный тип, <int, {_ == 1}>. Ну правда же? Конечно да. Так вот, такой тип
является подтипом <int, {_ > 0}>. А значит мы можем вернуть значение такого типа из функции factorial. Круто? Ну такое.
Что происходит, если n != 0? А тут происходит магия, которая называется smartcast. Компилятор бесконечно умный (ну-ну), поэтому
он понимает, что если он знал, что n >= 0, а при этом n != 0, то n >= 1. Потом он вычисляет значение n - 1 и выводит у него какой тип?
А вот такой: <int, {_ >= 0}>, потому что n был >= 1, а мы вычли единицу. И поэтому теперь мы можем вызвать factorial от 
значения n - 1! Это уже довольно круто, на самом деле. Это аналог того, что в котлине называется smartcast, когда компилятор может
вывести, что раз проверка n == 0 не прошла, то на самом деле n имеет другой, более точный тип. Ну вот, а так как мы знаем, что
n >= 1, при этом factorial(n - 1) > 0, то их произведение больше 0 и подходит под то, что мы можем вернуть. Какой-то такой
академический бесполезный пример. 

На этом моменте, наверное, стоит отметить, что две вещи, которые я обожаю в языках (компиляторах) больше всего это системы типов
и статические оптимизации. В моих глазах идеальный язык -- это когда с помощью системы типов можно выразить произвольно мощные
ограничения на значения, чтобы любая неправильная программа падала при компиляции, и эта самая система типов позволяла
оптимизатору красивый абстрактный код оптимизировать очень и очень эффективно. То есть моя мечта -- писать высокоуровневый
абстрактный код с кучей сложных идей, а чтобы компилятор все это убирал и делал очень низкоуровневый и оптимизированный код.
И вот для этого можно использовать мою идею. 

Пример второй, простой, полезный:

fun <T, size> safe_get(a: list<T, size>, index: <int, {_ >= 0, _ < size}>): T {
	return a[index];
}

Пусть у тебя есть листы фиксированного размера (можно и не фиксированного, но сложнее). Как тебе защититься от 
OutOfBounds проблем? Я знаю как минимум два решения:
	1. Runtime-assert'ы, которые падают, если не попало в границы -- Java way, OutOfBoundsException, безопасно, медленно
	2. Положить на это большой (или не очень) хер -- C++ way, undefined behaviour, безумно, зато быстро

Новая система типов позволяет дать больше обоим мирам, взяв из них самое лучшее. Посмотрим на функцию safe_get.
К слову, вот и зависимые типы пригодились. Она имеет такой хитрый тип, что индекс должен лежать в пределах размера
листа. Чтобы её вызвать, нужно статически доказать, что индекс именно такой. Я предлагаю как минимум 3 способа
это сделать.

Метод 1. Явные ручные проверки

	if (i >= 0 && i < a.size)
		elem = safe_get(a, i);

	Тут компилятор использует smartcast, потому что ты руками проверил. Хорошее напоминание для программиста,
	что что-то надо проверить.

Метод 2. Мамой клянусь!

	Так как мы все живем в реальном мире и иногда либо компилятор недостаточно умен, чтобы что-то вывести, 
	либо ты пишешь наколеночный Hello World и тебе насрать на какие-то там проверки, предлагается ввести
	оператор "мамойклянусь", также называемый как true assertion или как-то так. Выглядит это примерно так:

	{i >= 0 && i < a.size}
	elem = safe_get(a, i);

	Такое оператор просто вносит априорную информацию в тип и все, без каких-то проверок. Упадет это уже
	внутри get, или не упадет вовсе, такой вот UB. Просто забей на проверки и работай, зараза, как-то так.

Метод 3. "Я, конечно, мамой клянусь, но ты это, проверь сам и брось что-нибудь", так же известный, как assert

	Иногда хочется поведения как в джаве, чтобы что-нибудь громко рухнуло в рантайме, если предположение не выполнилось.
	Так вот это очень круто вписывается в модель smartcast'ов и таких типов, потому что ты можешь написать такой
	assert, который проверяет условие, падает, если оно не выполнено и вносит его в систему типов. Примерно вот так:

	{i >= 0 && i < a.size}!
	elem = safe_get(a, i)

	Удобно? Нормально.

В итоге такой подход позволяет реализовать любой из путей, которые были в языках раньше, но дополнительно позволяет
иногда статически элиминировать такие проверки, например: если у тебя есть контейнер, который внутри делегирует
к другому контейнеру и так далее, у тебя по пути может быть несколько раз проверки. Если у тебя такая система типов,
то тебе проверка нужна ровно 1 раз, а потом все передается внтури системы типов.

Так, это пара таких средне-жизненных примеров. Разумеется, мотивация основная такая -- безопасность при отсутствии
рантайм проверок. То есть быстро и надежно, утопия, класс.

Дальше начинаются среднедикие идеи примерно такого рода. Компилятор не может вывести все на свете. На самом деле
он вообще сильно ограничен. Но человек -- нет. Поэтому надо дать программисту писать доказательства прямо
внутри кода, чтобы выводить дополнительные утверждения на типах. Да, получается какой-то Coq или Agda слегка.
Выглядит это как-то так. Если в факториале компилятор не справился понять, что n - 1 >= 0, то можно написать так:

fun factorial(n: <int, {_ >= 0}>): <int, {_ > 0}> {
    if (n == 0) return 1;
    {{
    	n >= 0
    	n != 0
    	n >= 1
    	n - 1 >= 0
    }}
    return n * factorial(n - 1);
}

Набор утверждений, которые являются кусками доказательства, и которые легко проверить программным верификатором
(мы такое писали, это правда несложно). Тогда можно будет доказывать более сложные вещи и писать аккуратные библиотеки,
которые скорее всего не будут падать, особенно если все аккуратно доказывать.

Так, вдохновение закончилось. Я могу еще немного позатирать про подтипы, nothing, пересечение типов, объединение типов,
Self-типы и даже что-нибудь про вызов функций, но это все явно стоит делать не сразу и не сейчас)

Это я все к тому, что я бы это хотел в какой-то форме впилить в компилятор.