April 19th, 2007

with Cat The Cat

Мысли по поводу Epigram.

Они - создатели Epigram, - выразили отличную мысль о разделении фаз проверки типов. О том, что, в принципе, конструкторы-боксы для различения значений определенного типа могут оказаться и ненужными. "Мы просто не можем передать сюда что-то не то." Еще мысль о различении фаз можно, по-моему, понимать и как "вот здесь у нас отлично проверенные функции, но не Тьюринг полные, а вот здесь - ограниченный тип рекурсии, все вместе, во-первых, проверяемо, во-вторых, Тьюринг-полно." Как, например, в железе: каждый кусочек железа выполняет достаточно маленькую функцию, а все вместе - один большой процессор Itanium.

Проверять ограниченный тип рекурсии можно, например, model-checking или чем-то наподобие.

На этом моя мысль останавливается. ;)