I had an email from a student asking why Idris supported partial functions, saying that it was surprising that a dependently typed language supported partial functions, because types are supposed to be precise specifications and you can’t be sure you have a precise implementation if your functions aren’t total. This is a very good question, and my answer was quite long, so following these academic blogging tips, I’ll reproduce my answer here. The tl;dr version is that, while I agree totality is important and I aim to make all of my programs total (I don’t think I’ve ever wanted to write a function with neither terminates nor produces results occasionally, after all) it’s a bit more complicated than that in practice.
I’m going to use “total” in a fairly informal sense here. By “total function” I mean either:
- A function which terminates for possible inputs, or
- A function which is guaranteed to produce some output before making a recursive call
In particular, this means you can still write an interpreter or operating system, for example. That is, you can write programs which run forever, but at least they achieve something while doing so.
It is a good idea to aim to make all of your functions total, as David Turner argues – when functions are total, you really can believe that “well-typed programs don’t go wrong” because you know you’re going to get an answer eventually (or in the case of coinductive functions, you know you’re going to keep making progress). And, indeed, dependent types can help you achieve that goal because you can use the extra structure the types give you as additional evidence for the termination checker. Here is a nice example.
Then, of course, some programs are really proofs, that you never actually run but which do demonstrate some properties of other functions. In this case, it’s vitally important that they are total, to guarantee that you haven’t missed any cases, or relied on circular reasoning, and so every possible input leads to a proof object.
Having said all that, Idris still supports partial functions, for two main reasons.
Firstly, you can divide programs in general into two categories:
- Programs you haven’t finished writing yet
- Programs which are complete
The first category is significantly larger than the second. Even more so if you replace “Programs” with “Applications”.
In the case that your program isn’t finished yet, you don’t want your type checker shouting at you that it’s not finished, because you already know, but you still might want to test it (sometimes we like to run our programs, as well as read and write them, after all). You might want to try running a program even with an incomplete proof, to help you develop an intuition for how the proof might work, or even to see if there are test cases which might invalidate your hypothesis. Alternatively, you might have a nice natural recursive algorithm which is not obviously structurally recursive (the functional version of quicksort is an obvious example of this) and not want to hold up the development of the rest of your application while you develop the termination proof.
The fact that programs spend most of their lives in an unfinished state is one reason people are interested in gradual types, and why a recent GHC extension allows you to run programs with type errors. You don’t want to release software with type errors (or, in the case of an Idris program with an associated correctness proof, release software with an incomplete proof) but it might be convenient during development.
Secondly, I don’t believe it’s a language’s job to tell a program what level of precision their programs’ types should have. Rather, a language and its features are there to help a programmer do their job. If I want the language to help me write a totally correct program with a precise specification, then I certainly want a totality checker, but if I’m just writing a quick script to do a simple task, maybe I’d rather just get the job done. I would like the library code the script invokes to be total, but I might not be so bothered about the script itself, at first.
Related to this, remember that there’s more you can do with dependent types than prove functional correctness. Just being able to give types to more programs is already a benefit which doesn’t require programs to be total. Dependent types can help you write generic libraries – the Eff library is a developing example of this, as are embedded domain specific languages in general – where the library user is making use of dependent types without necessarily being aware of it.
Idris aims to be a general purpose programming language, rather than a theorem prover, so aims to support all uses of dependent types, or even to support programming with conventional types if that’s all you need, so the default is to support partial functions. If the goal was primarily to be a theorem prover, I think the opposite choice would have been appropriate. Whatever happens, though, functions are always checked for totality, and you can make partial functions a compile-time error by default with the “–total” flag.
If you want complete safety, you certainly have to work for it, and depending on your application that may be important. Sometimes, though, you just want to get things done. In that case, Idris will let you – but at least the type system and totality checker make it clear what assumptions you have made to do so.