[Haskell-cafe] Are bottoms ever natural?

[Joachim Durchholz]

Am 19.12.2017 um 17:51 schrieb Siddharth Bhat:
> So, I have two opinions to share on this:
> Regarding the plane example, it is wrong to attempt to graph it on a 
> plane, precisely because the domain is not the plane.

People graph partial functions all the time, e.g. the cotangent:
https://upload.wikimedia.org/wikipedia/commons/b/bf/Cotangent.svg
They simply do not graph the places where the function is undefined.

> I am confused by your assertion that it is impossible to avoid 
> divergence in mathematics: we do not define division as a *partial* 
> function. Rather we define it as a *total* function on a *restricted 
> domain*.

Which amounts to the same thing in practice.
You still need to check that your denominator is non-zero in a division. 
Whether you do that by a type check or a runtime check amounts to 
roughly the same amount of work for the programmer.

> So, what one would need is the ability to create these restricted 
> domains, which certain languages have as far as I am aware.

Yes, but type systems are usually more clunky than assertions.
You can take apart assertions if they are connected by AND, OR, etc. 
Type systems usually do not have that, and those that do are no more 
decidable, which is a no-go for most language designers.

> At that point, now that we track our domains and codomains correctly, 
> all should work out?

Not much better than what we have right now, I fear.

> I would still like an answer to interesting transformations that are 
> enabled by having purity and laziness and are not encumbered by the 
> presence of bottoms.
If you have laziness, you do not know whether the computation will 
terminate before you try, and no amount of type checking will change that.
Unless your type language is powerful enough to express the difference 
between a terminating and a nonterminating computation. Which means that 
now it's the compiler that needs to deal with potentially-bottom values, 
instead of the runtime. Which is a slightly different point on the 
trade-off spectrum, but still just a trade-off.

Regards,
Jo