|
|
|
|
|
|
by matt_kantor
2634 days ago
|
|
|
Hang on a minute. The only difference is that the languages you are talking about have captured "doing I/O" as something that can be statically reasoned about, but not "consuming memory" (for example). From a mathematical perspective, one is part of the axioms while another is not. One could imagine a language where all memory allocation must be done explicitly via a monad, just like how in Haskell all I/O is performed inside an IO monad. If that were the case, you could have additional static guarantees about how memory is used. That doesn't mean that languages which don't do this are somehow inherently "impure"; they are simply "pure with respect to a certain set of axioms" (which don't talk about memory usage). "The system crashed" example is fun too. All pure functions must return a value, right? Well, that's obviously not gong to be the case if the computer blows up halfway through executing a pure function. "Blowing up" might not be something your type system talks about—Haskell does to some degree (with _|_ inhabiting every type), but Idris for example has total functions which at runtime could most definitely be interrupted by a sudden explosion. They are "total" only with respect to a set of axioms which imply an execution model where computers do not explode mid-program. |
|
|
However, if you are thinking more in the direction of "you have to reason about where and how exactly your values and functions are stored", you're moving back to C, because the entire point is to disentangle the formal description of computation, from it's actual execution in the real world. If you want to deal with that, you have to do it explicitly and _by reasoning about it_ (with ST, for example). Which is what purity means.
> They are "total" only with respect to a set of axioms which imply an execution model where computers do not explode mid-program
"There is a chance that the computer blows up" is one of those things that have little bearing when reasoning about programs, it's just not in the domain of discourse. It certainly has no formal bearing on the notion of totality, mathematics just doesn't deal with cases such as "what if everyone who counted to 5 suddenly died", it deals with the counting itself. When the chance is actually high, for example radiation in space flipping bits, I'm pretty sure you want to handle that elsewhere.
It's not hard to imagine a fault-tolerance system gaining a lot from dependent types, however, with their ability to prove that your code follows a defined protocol.