CODEWITHSUNDEEP
idris
bbarker
bbarker

Reputation: 13088

Does Idris have non-terminating terms?

On the Unofficial FAQ on the official Idris wiki (official in that it is on the language's git repo), it is stated that

in a total language [e.g. Idris] we don't have undefined and non-terminating terms so we need not worry about evaluating them.

However, the following definition for ones (using List instead of Stream) certainly seems non-terminating:

ones: List Int
ones = 1 :: ones
-- ...
printLn(head ones) -- seg fault!

So, I'm not sure if the wiki entry is mistaken, or if I misunderstand the context. Note the Stream workaround is already described in the Idris tutorial.

Upvotes: 3

Views: 184

Answers (1)

HTNW
HTNW

Reputation: 29193

Idris is only total if you ask it to be total. You may write one of %default total, %default covering, or %default partial (the default), and all declarations afterwards will take on the given totality annotation:

%default total

-- implicitly total
ones1 : List Int
ones1 = 1 :: ones1
-- ERROR: ones1 is not total

-- total
ZNeverHeardOfIt : Nat -> Nat
ZNeverHeardOfIt (S n) = n
-- ERROR: missing cases in ZNeverHeardOfIt

covering
natRoulette : Nat -> Nat
natRoulette Z = Z
natRoulette (S n) = natRoulette (S (S n))
-- covering means all possible inputs are covered by an equation
-- but the function isn't checked for termination
-- natRoulette has cases for all inputs, but it might go into an infinite loop
-- it's morally equivalent to just partial, as a function that loops forever
-- on an input isn’t very different from one missing the case
-- it just gets the compiler to complain more

partial
ones : List Int
ones = 1 :: ones
-- no checks at all
-- Idris, being strict, needs to evaluate ones strictly before it can evaluate ones.
-- Oh wait, that's impossible. Idris promptly vanishes in a segfault.

Upvotes: 5

Related Questions