Re: [Haskell-cafe] Knight Capital debacle and software correctness

Jay Sulzberger writes:

On Sat, 4 Aug 2012, Clark Gaebel wrote:

...

As far as I know, you can't check "equivalence" of _|_. Since Haskell uses _|_ to represent a nonterminating computation, this would be synonymouswith solving the halting problem.

Ah, thanks. I will attempt to think about this.

Also, one way of looking at type systems says that all these _|_s are the same (but as Clark says, there’s no way within Haskell to compare them). Haskell mangles this a little by including non-value things other than non-termination in its types. — Jón