On Wednesday, 19 July 2017 at 14:52:28 UTC, Timon Gehr wrote:
On 19.07.2017 16:47, Moritz Maxeiner wrote:
On Wednesday, 19 July 2017 at 14:32:24 UTC, Timon Gehr wrote:
On 19.07.2017 14:13, Moritz Maxeiner wrote:
On Wednesday, 19 July 2017 at 11:35:47 UTC, Timon Gehr wrote:
a value of type bottom can be used to construct a value for
any other type.
AFAIK from type theory, bottom is defined as having no
values (so one can't reason about the relationship of such
non-existent value(s) to values of other types).
https://en.wikipedia.org/wiki/Principle_of_explosion
I am aware, but once a statement (and its negation) can be
inferred from the same (false) proposition, one isn't
reasoning anymore - and more importantly its not useful w.r.t.
explaining what the bottom type is.
I disagree with both of those statements, but I'm not sure how
any of this relates to the true sentence I wrote that you
seemed to criticize.
The sentence I quoted states you can use a value of type bottom
to construct a value of any other type; this means the existence
of such a value of type bottom becomes an implicit premise. As
the bottom type is defined as having no values that premise does
not hold, i.e. you can infer both
"a value of type bottom can be used to construct a value for any
other type."
and
"a value of type bottom cannot be used to construct a value for
any other type."
from it (principle of explosion, as you quoted). My original
criticism was meant to convey that I do not consider the quoted
sentence as being helpful w.r.t. explaining what the bottom type
is (which the rest of the post I quoted the sentence from did
quite well).
