Uses of termination checking

Posted Feb 14, 2025 15:27 UTC (Fri) by farnz (subscriber, #17727)
In reply to: Running several checkers instead of one by taladar
Parent article: Maintainer opinions on Rust-for-Linux

Idris has both as part of its totality checker; a function can be partial (in which case it may never terminate or produce a value - it can crash or loop forever) or total (in which case it must either terminate for all possible inputs, or produce a prefix of a possibly infinite result for all possible inputs).

Idris then uses this to determine whether it can evaluate a function at compile time (total functions) or whether it must defer to runtime (partial functions). This becomes important because Idris is dependently typed, so you can write a type that depends on the outcome of evaluating a function; if that function is total, then the type can be fully checked at compile time, while if it's partial, it cannot.