Ivory: Numbers In Scheme
Scheme uses the asterisk *
for
multiplication, since it’s easy to type on a standard US keyboard. I
prefer the usual ×
symbol, for
clarity. Hence we’ll define ×
to
be *
, so
that both symbols will mean multiplication:
define × *) (
Numbers in Scheme can be exact
or inexact
. Ivory
is only concerned with exact
numbers,
so we’ll ignore the latter. Scheme arranges its types in a “numerical
tower”, where each level is a super-set of the ones above,
including:
integer
: Whole numbers, positive and negative.rational
: All fractions, positive and negative.real
: This supposedly includes the whole “number line”, but is actually rather silly since almost all of the “real numbers” can’t be represented.complex
: This uses a clever trick to represent square roots of negative numbers. If you’ve encountered it before, great; if not, don’t worry since Ivory does not include this level (we instead define a mezzanine inside thegeometric
level)number
: This is the top level, containing every numeric value.
These are cumulative, so an integer
like -42
is also a
rational
(e.g. you can think of
it like -42/1
), a
real
and a complex
(like -42+0i
,
if you know what that means).
This basic framework is the inspiration for Ivory.
Numbers in Racket
Racket already extends Scheme’s standard numerical tower, and pins-down some details that Scheme leaves open. In particular:
- Scheme allows levels between
complex
andnumber
, but Racket doesn’t provide any. - Racket’s foundational
number
type adds nothing else tocomplex
(they’re just synonyms) - The only
exact
numbers in Racket’sreal
level arerational
. Hence, as far as Ivory is concerned, those levels are the same.
Racket does add some “attic levels”, which are strict
subsets of integer
:
natural
is a sub-set ofinteger
without negatives. It is closed under+
,×
,gcd
,lcm
,max
,min
, etc.; as well asquotient
andremainder
excluding the divisor0
, andexpt
excluding(expt 0 0)
.zero
is a sub-set ofnatural
containing only0
. It is closed under+
,×
,gcd
,lcm
,max
,min
, etc.
Even more fine-grained structure is described
in the Typed Racket documentation (e.g. byte
is a subset of natural
between 0
and 255
) but Ivory
does not make such size-based distinctions.
Code
This post defines Racket code, including a RackCheck test suite to check the claims we make on this page. Here’s a URI containing all of the generated code:
Test results
raco test: (submod "num.rkt" test)
✓ property ×-matches-* passed 100 tests.
✓ property integer?-implies-rational? passed 100 tests.
✓ property rational?-implies-number? passed 100 tests.
✓ property natural?-implies-integer? passed 100 tests.
✓ property natural-is-closed passed 100 tests.
26 tests passed