3 ms·

You're talking about error handling in practical programs. When I started out writing "theoretical guarantee," I meant in a proof, written in a proof language.

You're talking about error handling in practical programs. When I started out writing "theoretical guarantee," I meant in a proof, written in a proof language. Reporting an error to a function's caller isn't really a thing in a proof. A function proves that if any input exists, its result exists. Returning an error means "an error might exist." We don't want to return that, we want to eliminate the error from our proof, so that it proves that the result exists for any input. Returning an 'Ether' type might be useful in a proof, but a 'Maybe' type seems dubious. We already assume that 'None' exists, so proving that 'None' might exist is useless. We don't have the same concerns in proofs and practical programs.

eru 3y ago
No, no, this entirely pragmatic _and_ theoretically sound. In a practical program you want to know that you in finite time you either get one of the declared errors, or you get a positive result. Using an `Either` type allows even a relatively weak type system to be of use here. There's no 'error' in your proof: your proof can't do anything about eg running out of disk space. Now, using an `Either` type for things like division-by-zero is a bit of a cop-out, and a compromise foisted on us by a weak type system. And you are right that in something like Agda you would hopefully never have to stoop so low. (Though even there, you can't proof everything. Eg if your program enumerates differences between adjacent prime numbers, you can't prove that it will (or won't) run out of 2s.)
- skybrian 3y ago
  I feel like we're talking past each other somehow but I'll give it one more try. In previous post you quoted the Dhall documentation: > The main benefit of evaluation being finite is not to eliminate long-running programs but to make them significantly less probable. In practice, you will discover that you will rarely author a configuration file that takes a long time to evaluate by accident. This might be practical advice, but it's not theoretically sound. It's drawing a conclusion that wasn't proven. Isn't it kind of weird to write proofs without caring about the result of the proof?

eru 3y ago

No, no, this entirely pragmatic _and_ theoretically sound. In a practical program you want to know that you in finite time you either get one of the declared errors, or you get a positive result. Using an `Either` type allows even a relatively weak type system to be of use here. There's no 'error' in your proof: your proof can't do anything about eg running out of disk space. Now, using an `Either` type for things like division-by-zero is a bit of a cop-out, and a compromise foisted on us by a weak type system. And you are right that in something like Agda you would hopefully never have to stoop so low. (Though even there, you can't proof everything. Eg if your program enumerates differences between adjacent prime numbers, you can't prove that it will (or won't) run out of 2s.)

skybrian 3y ago
I feel like we're talking past each other somehow but I'll give it one more try. In previous post you quoted the Dhall documentation: > The main benefit of evaluation being finite is not to eliminate long-running programs but to make them significantly less probable. In practice, you will discover that you will rarely author a configuration file that takes a long time to evaluate by accident. This might be practical advice, but it's not theoretically sound. It's drawing a conclusion that wasn't proven. Isn't it kind of weird to write proofs without caring about the result of the proof?