Initial version of Insect 'book'

book/.gitignore

@@ -0,0 +1 @@
+book

book/book.toml

@@ -0,0 +1,9 @@
+[book]
+authors = ["David Peter"]
+language = "en"
+multilingual = false
+src = "src"
+title = "Insect - scientific calculator with full support for physical units"
+
+[output.html]
+mathjax-support = true

book/src/SUMMARY.md

@@ -0,0 +1,39 @@
+# Summary
+
+[Introduction](./introduction.md)
+
+# User Reference
+
+## Basics
+
+- [Number notation]()
+- [Unit notation]()
+  - [List of supported units]()
+- [Operators and their precedence]()
+- [The conversion operator]()
+- [Builtin functions and constants]()
+  - [Trigonometric]()
+  - [Date and time]()
+  - [Statistics]()
+  - [Physical constants]()
+- [User-defined variables]()
+- [User-defined functions]()
+
+## Advanced features
+
+- [Unit Declarations](./unit-declarations.md)
+- [Dimension Declarations](./dimension-declarations.md)
+- [Syntax]()
+
+# Command line tool
+
+- [Installation]()
+- [Usage]()
+
+# Web version
+
+- [Usage]()
+
+# Notes for developers
+
+- [Type system](./type-system.md)

book/src/dimension-declarations.md

@@ -0,0 +1,33 @@
+# Dimension declarations
+
+New (physical) dimensions can be introduced with the `dimension` keyword. Similar to [units](./unit-declarations.md), there are base dimensions (like *length*, *time* and *mass*) and dimensions that are derived from those base dimensions (like *momentum*, which is *mass* · *length* / *time*). Base dimensions are simply introduced by declaring their name:
+```
+dimension Length
+dimension Time
+dimension Mass
+```
+Derived dimensions need to specify their relation to base dimensions (or other derived dimensions). For example:
+```
+dimension Speed = Length / Time
+dimension Momentum = Mass * Speed
+dimension Force = Mass * Acceleration = Momentum / Time
+dimension Energy = Momentum^2 / Mass = Mass * Speed^2 = Force * Length
+```
+In the definition of `Force` and `Energy`, we can see that *alternative definitions* can be given. This is entirely optional. If specified, the compiler will make sure that all definitions are equivalent.
+
+## Custom dimensions
+
+It is often useful to introduce 'fictional' physical dimensions. For example, we might want to do calculations with
+screen resolutions and 'dot densities'. Introducing a new dimension for *dots* then allows us to define units like `dpi` without sacrificing unit safety:
+```
+dimension Dot
+
+@aliases(dots)
+unit dot: Dot
+
+unit dpi = dots / inch
+
+fn inter_dot_spacing(resolution: Dot/Length) -> Length = 1 dot / resolution
+
+inter_dot_spacing(72 dpi) -> µm  # 353 µm
+```

book/src/introduction.md

@@ -0,0 +1,12 @@
+# Introduction
+
+> *"You see, Vergon 6 was once filled with the super-dense substance known as dark matter, each pound of which weighs over 10,000 pounds."* — Futurama, S1E4
+
+Insect is a high precision scientific calculator with full support for physical units. You can use
+it for simple mathematical computations like
+```
+1920/16*9
+2^32
+sqrt(1.4^2 + 1.5^2) * cos(pi/3)^2
+```
+

book/src/type-system.md

@@ -0,0 +1,95 @@
+# Type system
+
+Insect is a language with a special type system that treats *physical dimensions* as types.
+A type checker infers types for every expression in the program and ensures that everything is correct in terms of physical dimensions, which implies correctness in terms of physical *units*.
+For example, the expression `2 meter` has a *type* of `Length`.
+The expression `3 inch` *also* has a type of `Length`.
+The combined expression `2 meter + 3 inch` is therefore well-typed.
+On the other hand, `2 meter + 3 second` is ill-typed, as `3 second` is of type `Time`.
+
+The type system is *static* which means that the correctness of an Insect program is verified before the program starts executing.
+Note that certain *runtime* errors (like division-by-zero) can still occur.
+
+## Algebra of types
+
+
+Types in Insect can be combined in various ways to produce new types.
+In its most general form, a type can be thought of as a product of physical (base) dimensions \\( D_k \\) with exponents \\( \alpha_k \in \mathbb{Q} \\):
+\\[ \prod_k D_k^{\alpha_k} \\]
+For example, the type *Energy* can be represented as *Mass¹ × Length² × Time⁻²*.
+
+### Multiplication
+
+This naturally allows us to *multiply* types (by combining the factors of both products into a single product).
+We can use the `*` operator to construct types for physical dimensions that are products of two or more (base) dimensions. For example:
+```
+dimension Time
+dimension Current
+dimension Charge = Current * Time
+```
+
+### Exponentiation
+
+We can also raise units to arbitrary powers \\( n \in \mathbb{Q} \\), by simply multiplying each \\( \alpha_k \\) with \\( n \\). The syntax uses the `^` exponentiation operator:
+```
+dimension Length
+dimension Volume = Length^3
+
+dimension Time
+dimension Frequency = Time^(-1)
+```
+
+### Division
+
+Once we have multiplication and exponentiation, we can define the *division* of two types as
+```
+TypeA / TypeB ≡ TypeA * TypeB^(-1)
+```
+This is mostly for convenience. It allows us to write definitions like
+```
+dimension Power = Energy / Time
+```
+
+> **Note:** When we talk about products of types in this section, we mean actual, literal products.
+> Type theory also has the notion of *product types* which denote something else: compound types — like tuples or structs — that are built by combining two or more types. If we think of types in terms of the sets of all possible values that they represent, then product types represent the Cartesian product of those.
+
+## Type inference and type annotations
+
+The type checker can infer the types of (most) expressions without explicitly declaring them. For example,
+the following definition does not mention any types:
+```rs
+let E_pot = 80 kg × 9.8 m/s² × 5 m
+```
+However, it is often helpful to specify the type anyway. This way, we can make sure that no mistakes were made:
+```rs
+let E_pot: Energy = 80 kg × 9.8 m/s² × 5 m
+```
+The type checker will compare the inferred type with the specified type and raise an error in case of inconsistency.
+
+Function definitions also allow for type annotations, both for the parameters as well as the return type. The following example shows a function that takes a quantity of type `Length` and returns a `Pressure`:
+```rs
+let p0: Pressure = 101325 Pa
+let t0: Temperature = 288.15 K
+
+let gradient = 0.65 K / 100 m
+
+fn air_pressure(height: Length) -> Pressure = p0 · (1 - gradient · height / t0)^5.255
+```
+
+
+## Generic types
+
+Insects type system also supports generic types (type polymorphism).
+These can be used for functions that work regardless of the physical dimension of the argument(s).
+For example, the type signature of the absolute value function is given by
+```rs
+fn abs<D>(x: D) -> D
+```
+where the angle brackets after the function name introduce new type parameters (`D`).
+This can be read as: `abs` takes an arbitrary physical quantity of dimension `D` and returns a quantity of the *same* physical dimension `D`.
+
+As a more interesting example, we can look at the `sqrt` function. Its type signature can be written as
+```rs
+fn sqrt<D>(x: D^2) -> D
+```
+Alternatively, it could also be specified as `fn sqrt<D>(x: D) -> D^(1/2)`.

book/src/unit-declarations.md

@@ -0,0 +1,70 @@
+# Unit Declarations
+
+New units of measurement can be introduced with the `unit` keyword. There are two types of units: base units and derived units.
+
+A new **base unit** can be defined by specifying the *physical dimension* it represents. For example, in the
+ [International System of Units (SI)](https://en.wikipedia.org/wiki/International_System_of_Units), the *second* is the base unit for measuring times:
+```
+unit second: Time
+```
+Here, `Time` denotes the physical dimension. To learn more, you can read the [corresponding chapter](physical-dimensions.md). But for now, we can just assume that they are already given.
+
+**Derived units** are also introduced with the `unit` keyword. But unlike base units, they are defined through their relation to
+other units. For example, a *minute* can be defined as
+```
+unit minute: Time = 60 second
+```
+Here, the `: Time` annotation is optional. If a dimension is specified, it will be used to verify that the right hand side expression (`60 second`) is indeed of physical dimension `Time`. This is apparent in this simple example, but can be useful for more complicated unit definitions like
+```
+unit farad: Capacitance = ampere^2 second^4 / (kilogram meter^2)
+```
+
+
+## Prefixes
+
+If a unit may be used with metric prefixes such as `milli`/`m`, `kilo`/`k` or `mega`/`M`, we can prepend the unit definition with the `@metric_prefixes` decorator:
+```
+@metric_prefixes
+unit second: Time
+```
+This allows identifiers suchs as `millisecond` to be used in calculations. See the section below how prefixes interact with aliases.
+
+Similarly, if a unit should be prependable with *binary* (IEC) prefixes such as `kibi`/`Ki`, `mebi`/`Mi` or `gibi`/`Gi`, you can
+add the `@binary_prefixes` decorator. A unit might also allow for both metric and binary prefixes, for example:
+```
+@binary_prefixes
+@metric_prefixes
+unit byte = 8 bit
+```
+This allows the usage of both `mebibyte` (1024² byte) as well as `megabyte` (1000² byte).
+
+## Aliases
+
+It is often useful to define alternative names for a unit. For example, we might want to use the plural form `seconds` or the commonly
+used short version `s`. We can use the `@aliases` decorator to specify "long" aliases and the `@aliases_short` to define "short" ones:
+```
+@metric_prefixes
+@aliases(meters, metre, metres)
+@aliases_short(m)
+unit meter: Length
+```
+The reason we distinguish between long and short forms is that they interact differently with prefixes. The unit name itself and all
+long aliases can be prefixed with the long versions of prefixes (..., `milli`, `kilo`, `mega`, `giga`, ...). On the other hand, short aliases can only be prefixed with the respective short versions of the prefixes (..., `m`, `k`, `M`, `G`, ...). The definition above
+allows all of following expressions:
+```
+millimeter
+kilometer
+
+millimeters
+kilometers
+
+millimetre
+kilometre
+
+millimetres
+kilometres
+
+mm
+km
+...
+```