September 26th, 2007

with Cat The Cat

Все только проснутся, а я уже вопрос задал.

Вот, почитываю про программирование на Epigram и статью Simply easy! про зависимые типы.

Меня сильно смущает утечка абстракции.

Например, тип tail: ∀α::*,β::Nat, tail :: Vec α (Succ β) -> Vec α β

Succ обязан быть конструктором значения Nat. А если я намереваюсь использоваться позиционную запись? Еще того хуже, если я собираюсь использовать произвольный тип, приводимый к целым числам?

По идее, тип tail в этом случае должен быть какой-то такой: ∀α::*,β::*, tail :: Vec α (fromInt (toInt β+1)) -> Vec α β

А это, как я понимаю, невозможно.

Что означает большое препятствие на пути их использования.

Второе препятствие, поменьше, это сообщения об ошибках.
with Cat The Cat

Ха!