3 ms·

Totality guarantees won't ensure a timely response. But they ensure that a function that should always return a value will always return a value. I.e. they eli

Totality guarantees won't ensure a timely response. But they ensure that a function that should always return a value will always return a value. I.e. they eliminate one source of bugs. So a default constraint on functions to be total, would be sensible and helpful. To be able to do the opposite, constrain a function or continuation to never terminate (outside of program termination), would be useful too. Albeit in much fewer contexts. Any constraint that forces implementations to match respective design intentions is good.

skybrian 2y ago
To put it a different way, a totality guarantee ensures that a function will always return a value in theory, but not in practice. To get the theoretical guarantee, you need to eliminate all possible runtime errors, including things like divide-by-zero errors. It’s kind of pain when you’re not making a theoretical argument. You might still want to eliminate all divide by zero errors. Satisfying the compiler of this using a machine-checked proof might be more trouble than it’s worth, though. It might require you to use a language whose types support proofs.
- eru 2y ago
  You don't need to eliminate all possible runtime errors. You just need to make sure they are handled and accounted for. That can take the form of something like `try_divide` that returns a `Maybe` that you need to pattern match on. Or it can take the form of trust-me-bro via the equivalant of UnsafePerformIO, where you know that something is safe and you want to let the compiler know, but you can't prove it to the compiler. You can also deal with errors by returning an `Either`. That doesn't mess with any totality guarantees.
  - skybrian 2y ago
    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 2y 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 2y 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?

skybrian 2y ago

To put it a different way, a totality guarantee ensures that a function will always return a value in theory, but not in practice. To get the theoretical guarantee, you need to eliminate all possible runtime errors, including things like divide-by-zero errors. It’s kind of pain when you’re not making a theoretical argument. You might still want to eliminate all divide by zero errors. Satisfying the compiler of this using a machine-checked proof might be more trouble than it’s worth, though. It might require you to use a language whose types support proofs.

eru 2y ago
You don't need to eliminate all possible runtime errors. You just need to make sure they are handled and accounted for. That can take the form of something like `try_divide` that returns a `Maybe` that you need to pattern match on. Or it can take the form of trust-me-bro via the equivalant of UnsafePerformIO, where you know that something is safe and you want to let the compiler know, but you can't prove it to the compiler. You can also deal with errors by returning an `Either`. That doesn't mess with any totality guarantees.
- skybrian 2y ago
  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 2y 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 2y 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?