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