Non-total functions are treated as constants at the type level?

1
votes

In Type-Driven Development with Idris, ch 6, he says

  • Type-level functions exist at compile time only ...
  • Only functions that are total will be evaluated at the type level. A function that isn't total may not terminate, or may not cover all possible inputs. Therefore, to ensure that type-checking itself terminates, functions that are not total are treated as constants at the type level, and don't evaluate further.

I'm having difficulty understanding what the second bullet point means.

  • How could the type checker claim the code type checks if there's a function that isn't total in its signature? Wouldn't there by definition be some inputs for which the type isn't defined?
  • When he says constant, does he mean in the same sense as in the docs, like 
    one: Nat
one = 1
    is a constant? If so, how could that enable the type checker to complete its job?
  • If a type-level function exists at compile time only, does it ever get evaluated if it's not total? If not, what purpose does it serve?
1
typecheckingidris

1 Answers

2
votes

Partial type-level functions are treated as constants in the Skolem sense: invocations of a partial function f remain f with no further meaning.

Let's see an example. Here f is a partial predecessor function:

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

If we then try to use it in a type, it will not reduce, even though f 3 would reduce to 2:

bad : f 3 = 2
bad = Refl

When checking right hand side of bad with expected type f 3 = 2

Type mismatch between 2 = 2 (Type of Refl) and f 3 = 2 (Expected type)

So f is an atomic constant here, standing only for itself. Of course, because it does stand for itself, the following still typechecks:

good : f 3 = f 3
good = Refl