4 ms·

Cute, but why should one care about ⊥, aka bottom, aka nontermination [0]? Let's write programs that terminate... [0] https://wiki.haskell.org/Bottom https://w

by pacala 8y ago

Cute, but why should one care about ⊥, aka bottom, aka nontermination [0]? Let's write programs that terminate... [0] https://wiki.haskell.org/Bottom https://wiki.haskell.org/Bottom

d_ 8y ago
Most functions we write are indeed total.
klodolph 8y ago
We care deeply about ⊥ because in our terminating programs there are often sub-expressions that do not terminate. Without ⊥, we cannot reason effectively about Haskell. You can require that all of your functions are total and still end up caring about ⊥.
- catamorphismic 8y ago
  Can you give a practical example of such nonterminating subexpressions?
dustingetz 8y ago
Proof of termination is closely related to : "Now suppose there were a hypothetical language with a stronger guarantee: if two programs are equal then they generate identical executables. Such a language would be immune to abstraction: no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected." http://www.haskellforall.com/2014/09/morte-intermediate-language-for-super.html http://www.haskellforall.com/2014/09/morte-intermediate-lang... A more practical reason to care is that if a user-generated expression is proven to be pure and to terminate, then we can evaluate it without fear of getting hacked, denial of service, etc. Imagine a new type of iphone, IDE or web browser where a shitty app/plugin can't lag up your experience.
- g___ 8y ago
  You need more than termination to protect against a denial of service; you need to know that a function terminates promptly. Most denial-of-service attacks are about functions that run slowly (e.g. O(N^2) or exponential).
- lmm 8y ago
  > A more practical reason to care is that if a user-generated expression is proven to be pure and to terminate, then we can evaluate it without fear of getting hacked, denial of service, etc. Imagine a new type of iphone, IDE or web browser where a shitty app/plugin can't lag up your experience. Nontermination alone isn't enough, since in some provably-terminating languages it's still very possible to write expressions that will take a very long time to evaluate in some implementations. Concretely, "catastrophic backtracking" regular expressions can be true regular expressions (and therefore provably terminating), but in naive implementations their runtime will be exponential in the input length. But it's a start, and the same techniques could hopefully lead to languages in which expressions naturally come with upper bounds on their evaluation time.
  - danidiaz 8y ago
    Some linear type systems garantee that functions defined in them have polynomial time complexity: http://www.cs.cmu.edu/~fp/courses/15816-s12/misc/hofmann03ic.pdf http://www.cs.cmu.edu/~fp/courses/15816-s12/misc/hofmann03ic... http://www.kurims.kyoto-u.ac.jp/~terui/lalcjournal.pdf http://www.kurims.kyoto-u.ac.jp/~terui/lalcjournal.pdf It appears however that the ones developed so far are awkward to "program" in.
- Kutta 8y ago
  > no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected This is an unfortunate glaring false statement in the Morte documentation. Correctness of refactoring and code abstraction is understood to be with respect to semantic (extensional) equivalence, while normalization only works up to beta-eta equivalence. It can't eliminate abstraction in general. Examples in Morte which suggest otherwise use hand-crafted forms of Church-encoded operations which are known to fuse, but there are many equivalent definitions which don't fuse, and which are actually more natural to write. Converting non-fusing definitions to fusing definitions is equivalent to supercompilation, which is generally undecidable, and thus can be implemented only up to some approximation.
OtterCoder 8y ago
It's kind of funny, looking at these halting discussions as a backend web programmer. At the heart of it, all I do all day is try to write nonterminating programs in an environment where the entire universe seems hell bent on terminating the event/polling loop. It's kind of perverse when you think about it.
- ben509 8y ago
  That's why I love containers... you definitely write your code to not leak resources, but if there's any unexpected state, your recovery strategy is to report the error, bail, and the whole container is blown away.
  - lmm 8y ago
    You shouldn't need something as "big" as containers for that - ordinary user processes would work. (Erlang takes this model even further, to actors within a single unix process).
    - ben509 8y ago
      That's a nice in theory, but it's insufficiently imaginative. The unexpected state can be out of memory, out of disk, persistent network failures, etc. And you need to be able mitigate bugs that make it to prod. Okay, your code never lets bugs into prod, but your dependencies may have issues, or you might have an unexpected conflict with the underlying OS. If you can limp along with a buggy configuration that's causing some containers to go down, you can often get a patch in place without having a total outage.
      - lmm 8y ago
        > That's a nice in theory, but it's insufficiently imaginative. The unexpected state can be out of memory, out of disk, persistent network failures, etc. Well sure, but if that's your threat model then don't you need to restart whole VMs/machines rather than individual containers? I've always felt like containers fall between two stools (at least for languages/ecosystems that have a good way of packaging programs with dependencies - I appreciate that they make sense as a deployment solution for e.g. Python): their isolation guarantees aren't as reliable (at least in practice) as full VMs/unikernels, but you pay most of the price in terms of not being able to use normal IPC mechanisms.

by pacala 8y ago

Cute, but why should one care about ⊥, aka bottom, aka nontermination [0]? Let's write programs that terminate... [0] https://wiki.haskell.org/Bottom https://wiki.haskell.org/Bottom

d_ 8y ago

Most functions we write are indeed total.

klodolph 8y ago

We care deeply about ⊥ because in our terminating programs there are often sub-expressions that do not terminate. Without ⊥, we cannot reason effectively about Haskell. You can require that all of your functions are total and still end up caring about ⊥.

catamorphismic 8y ago
Can you give a practical example of such nonterminating subexpressions?

dustingetz 8y ago

Proof of termination is closely related to : "Now suppose there were a hypothetical language with a stronger guarantee: if two programs are equal then they generate identical executables. Such a language would be immune to abstraction: no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected." http://www.haskellforall.com/2014/09/morte-intermediate-language-for-super.html http://www.haskellforall.com/2014/09/morte-intermediate-lang... A more practical reason to care is that if a user-generated expression is proven to be pure and to terminate, then we can evaluate it without fear of getting hacked, denial of service, etc. Imagine a new type of iphone, IDE or web browser where a shitty app/plugin can't lag up your experience.

g___ 8y ago
You need more than termination to protect against a denial of service; you need to know that a function terminates promptly. Most denial-of-service attacks are about functions that run slowly (e.g. O(N^2) or exponential).
lmm 8y ago
> A more practical reason to care is that if a user-generated expression is proven to be pure and to terminate, then we can evaluate it without fear of getting hacked, denial of service, etc. Imagine a new type of iphone, IDE or web browser where a shitty app/plugin can't lag up your experience. Nontermination alone isn't enough, since in some provably-terminating languages it's still very possible to write expressions that will take a very long time to evaluate in some implementations. Concretely, "catastrophic backtracking" regular expressions can be true regular expressions (and therefore provably terminating), but in naive implementations their runtime will be exponential in the input length. But it's a start, and the same techniques could hopefully lead to languages in which expressions naturally come with upper bounds on their evaluation time.
- danidiaz 8y ago
  Some linear type systems garantee that functions defined in them have polynomial time complexity: http://www.cs.cmu.edu/~fp/courses/15816-s12/misc/hofmann03ic.pdf http://www.cs.cmu.edu/~fp/courses/15816-s12/misc/hofmann03ic... http://www.kurims.kyoto-u.ac.jp/~terui/lalcjournal.pdf http://www.kurims.kyoto-u.ac.jp/~terui/lalcjournal.pdf It appears however that the ones developed so far are awkward to "program" in.
Kutta 8y ago
> no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected This is an unfortunate glaring false statement in the Morte documentation. Correctness of refactoring and code abstraction is understood to be with respect to semantic (extensional) equivalence, while normalization only works up to beta-eta equivalence. It can't eliminate abstraction in general. Examples in Morte which suggest otherwise use hand-crafted forms of Church-encoded operations which are known to fuse, but there are many equivalent definitions which don't fuse, and which are actually more natural to write. Converting non-fusing definitions to fusing definitions is equivalent to supercompilation, which is generally undecidable, and thus can be implemented only up to some approximation.

OtterCoder 8y ago

It's kind of funny, looking at these halting discussions as a backend web programmer. At the heart of it, all I do all day is try to write nonterminating programs in an environment where the entire universe seems hell bent on terminating the event/polling loop. It's kind of perverse when you think about it.

ben509 8y ago
That's why I love containers... you definitely write your code to not leak resources, but if there's any unexpected state, your recovery strategy is to report the error, bail, and the whole container is blown away.
- lmm 8y ago
  You shouldn't need something as "big" as containers for that - ordinary user processes would work. (Erlang takes this model even further, to actors within a single unix process).
  - ben509 8y ago
    That's a nice in theory, but it's insufficiently imaginative. The unexpected state can be out of memory, out of disk, persistent network failures, etc. And you need to be able mitigate bugs that make it to prod. Okay, your code never lets bugs into prod, but your dependencies may have issues, or you might have an unexpected conflict with the underlying OS. If you can limp along with a buggy configuration that's causing some containers to go down, you can often get a patch in place without having a total outage.
    - lmm 8y ago
      > That's a nice in theory, but it's insufficiently imaginative. The unexpected state can be out of memory, out of disk, persistent network failures, etc. Well sure, but if that's your threat model then don't you need to restart whole VMs/machines rather than individual containers? I've always felt like containers fall between two stools (at least for languages/ecosystems that have a good way of packaging programs with dependencies - I appreciate that they make sense as a deployment solution for e.g. Python): their isolation guarantees aren't as reliable (at least in practice) as full VMs/unikernels, but you pay most of the price in terms of not being able to use normal IPC mechanisms.