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?
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
Not much better than what we have right now, I fear. trade-off spectrum, but still just a trade-off. Regards, Jo