6 ms·

“Finite time” isn’t much of a guarantee. A million years is finite. Totality checking is useful in language for doing proofs, where you need a guarantee that a

“Finite time” isn’t much of a guarantee. A million years is finite. Totality checking is useful in language for doing proofs, where you need a guarantee that a function always returns a value even though you never run it. In languages for doing practical calculations, a progress dialog and a cancel button are more useful than a totality guarantee. It should be easier to make complex, long-running calculations safely cancellable. (Still true with laziness, though it changes a bit. At some point you will ask for a value to be calculated.)

Nevermark 3y ago
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 3y 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 3y 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 3y 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 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
> “Finite time” isn’t much of a guarantee. A million years is finite. You are technically right, but in practice, finite time does help a lot. To quote from the Dhall documentation at https://docs.dhall-lang.org/discussions/Safety-guarantees.html#turing-completeness https://docs.dhall-lang.org/discussions/Safety-guarantees.ht... > Note that a “finite amount of time” can still be very long. For example, there are some short pathological programs that take longer than the heat death of the universe to evaluate. 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. > It should be easier to make complex, long-running calculations safely cancellable. Just send kill 9 to your program, if you want to cancel it? That seems like an entirely separate topic? (Especially if your calculation is pure, it's always safe to cancel it.)
- skybrian 3y ago
  Yes, killing the process is how cancellation of a batch job is normally done, for example in shell scripts. But it’s a heavyweight approach. Backend servers don’t use a process per request anymore and they do need ways to cancel a request. Go’s Context API handles cancellation and timeouts at the request level, but it has to be coded manually; a badly-behaved goroutine could still leak and consume resources long after it’s cancelled. So it might be nice to have automatic support at the language level, to make guaranteed cancellation happen by default. This is the approach taken with structured concurrency. To preserve the invariant that a child task doesn’t outlive the parent, there needs to be a way to kill any unneeded child tasks when a function returns early. Totality checks seem like a poor substitute when what you actually want is to prevent resource leaks. I haven’t used Dhall, but it seems like a config language has different concerns?

Nevermark 3y ago

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 3y 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 3y 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 3y 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 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

> “Finite time” isn’t much of a guarantee. A million years is finite. You are technically right, but in practice, finite time does help a lot. To quote from the Dhall documentation at https://docs.dhall-lang.org/discussions/Safety-guarantees.html#turing-completeness https://docs.dhall-lang.org/discussions/Safety-guarantees.ht... > Note that a “finite amount of time” can still be very long. For example, there are some short pathological programs that take longer than the heat death of the universe to evaluate. 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. > It should be easier to make complex, long-running calculations safely cancellable. Just send kill 9 to your program, if you want to cancel it? That seems like an entirely separate topic? (Especially if your calculation is pure, it's always safe to cancel it.)

skybrian 3y ago
Yes, killing the process is how cancellation of a batch job is normally done, for example in shell scripts. But it’s a heavyweight approach. Backend servers don’t use a process per request anymore and they do need ways to cancel a request. Go’s Context API handles cancellation and timeouts at the request level, but it has to be coded manually; a badly-behaved goroutine could still leak and consume resources long after it’s cancelled. So it might be nice to have automatic support at the language level, to make guaranteed cancellation happen by default. This is the approach taken with structured concurrency. To preserve the invariant that a child task doesn’t outlive the parent, there needs to be a way to kill any unneeded child tasks when a function returns early. Totality checks seem like a poor substitute when what you actually want is to prevent resource leaks. I haven’t used Dhall, but it seems like a config language has different concerns?