Все только проснутся, а я уже вопрос задал.
Вот, почитываю про программирование на Epigram и статью Simply easy! про зависимые типы.
Меня сильно смущает утечка абстракции.
Например, тип tail: ∀α::*,β::Nat, tail :: Vec α (Succ β) -> Vec α β
Succ обязан быть конструктором значения Nat. А если я намереваюсь использоваться позиционную запись? Еще того хуже, если я собираюсь использовать произвольный тип, приводимый к целым числам?
По идее, тип tail в этом случае должен быть какой-то такой: ∀α::*,β::*, tail :: Vec α (fromInt (toInt β+1)) -> Vec α β
А это, как я понимаю, невозможно.
Что означает большое препятствие на пути их использования.
Второе препятствие, поменьше, это сообщения об ошибках.
Меня сильно смущает утечка абстракции.
Например, тип tail: ∀α::*,β::Nat, tail :: Vec α (Succ β) -> Vec α β
Succ обязан быть конструктором значения Nat. А если я намереваюсь использоваться позиционную запись? Еще того хуже, если я собираюсь использовать произвольный тип, приводимый к целым числам?
По идее, тип tail в этом случае должен быть какой-то такой: ∀α::*,β::*, tail :: Vec α (fromInt (toInt β+1)) -> Vec α β
А это, как я понимаю, невозможно.
Что означает большое препятствие на пути их использования.
Второе препятствие, поменьше, это сообщения об ошибках.
