Why does Idris need mutual?

Question

Why does Idris require that functions appear in the order of their definitions and mutual recursion declared with mutual?

I would expect Idris to perform a first pass of dependency analysis between functions, and reorder them automatically. I have always believed that Haskell does this. Why is this not possible in Idris?

Answer 1

In the tutorial it says (emphasis mine):

In general, functions and data types must be defined before use, since dependent types allow functions to appear as part of types, and their reduction behaviour to affect type checking. However, this restriction can be relaxed by using a mutual block, which allows data types and functions to be defined simultaneously.

(Agda has this restriction as well, but has now removed the mutual keyword in favour of giving types then definitions.)

To expand on this: when you have dependant types, the automatic dependency analysis à la Haskell would be difficult or impossible, because the dependancy order at the type level may very well be different than the dependancy order at the value level. Haskell doesn't have this problem because values can not appear in types, so it can just do the dependancy analysis and then typecheck in that order. This is what the Idris tutorial is getting at about the reduction behaviour of values being required for the type checking.

I do not know whether the problem is even solvable in general with dependant types (you lose Hindley-Milner, for one thing), but I bet it wouldn't be efficient even if it were.