Ну даёт!

Я просто оставлю это здесь: https://pigworker.wordpress.com/2015/01/05/linear-dependent-types/

Нет, я не могу просто оставить, я чуток прокомментирую. Конор МакБрайд положительно был стукнут молотом Тора и из его гениального мозга посыпались звёзды. И ещё вот это (https://pigworker.wordpress.com/2015/01/01/irish-induction-recursion/), и вот это (https://pigworker.wordpress.com/2015/01/02/coinduction/). Ну блин, ну он даёт, ну надо же так, а. Взял и всё разложил по полочкам. Когда я это всё читать-то буду, ночью я и так работаю, выкопать откуда-то ночь ночи? Я как-то сомневаюсь, что смогу нормально заснуть, пока не вкурю хотя бы про линейные зависимые типы.