# [isabelle] The theory Option

`I've been looking at theory Option for some time now, and I've been
``wondering why it isn't used more often than it is. If you're going to
``have a type with an extra element called None, an obvious use of this
``(obvious to me, anyway) would be to interpret None as "undefined."
``Division of real numbers, for example, could be a function from (real
``option) x (real option) -> real option, with x/0 = None and None/x =
``y/None = None. This is in fact exactly how floating point numbers
``work on computers today, except that there None is called NaN, which
``is an abbreviation for Not a Number.
``The advantage of this over the current system of using zero to mean
``"undefined" is that there you can't tell the difference, after the
``fact, between a zero meaning "undefined" and a real zero. Another
``advantage for me is that if I'm trying to explain Isar to
``mathematicians who are complex analysts or other non-algebraists, as
``I intend to try to do, it could take a lot of explaining to convince
``them that defining x/0 to be 0 (rather than None) doesn't lead to
``absurdities. I've done complex analysis myself (my theorem says that
``if S and S' are countable dense sets on the complex plane, there
``exists an entire function taking S onto S') so I should be believable
``when talking to complex analysts.
`Is there a good reason why this wouldn't work in practice?
--
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*