Нецелые функции рассматриваются как константы на уровне типа?

Question

В Type-Driven Development with Idris , ch 6, он говорит:

• Функции уровня типов существуют только на времени компиляции . ..
• Только общие функции будут оцениваться на уровне типа. Функция, которая не является полной, может не завершиться или не охватить все возможные входы. Следовательно, чтобы гарантировать, что проверка типов завершается, функции, которые не являются итоговыми, обрабатываются как константы на уровне типа и не вычисляются дальше.

Мне трудно понять, что означает второй маркер.

• Как может средство проверки типов утверждать, что тип кода проверяет, есть ли функция, которая не является полной в своей подписи? Разве по определению не было бы некоторых входов, для которых тип не определен?
• Когда он говорит «константа», имеет ли он в виду в том же смысле, что и в документы , например,

  one: Nat
  one = 1
  

  константа? Если да, то как это могло позволить средству проверки типов завершить свою работу?
• Если функция уровня типа существует только во время компиляции, будет ли она когда-либо оцениваться, если она не полная? Если нет, то какой цели он служит?

Answer 1

Частичные функции уровня типа обрабатываются как константы в смысле Сколема: вызовы частичной функции f остаются f без дальнейшего значения.

Давайте посмотрим на пример. Здесь f - это частичная функция-предшественник:

f : Nat -> Nat
f (S x) = x

Если мы затем попытаемся использовать ее в типе, она не уменьшится, даже если f 3 уменьшится до 2:

bad : f 3 = 2
bad = Refl

При проверке правой стороны плохого с ожидаемым типом f 3 = 2

Несоответствие типов между 2 = 2 (Тип Refl) и f 3 = 2 (Ожидаемый тип)

Итак, f - это константа atomi c, обозначающая только себя. Конечно, поскольку это означает само за себя, следующие проверки типов по-прежнему:

good : f 3 = f 3
good = Refl