Physics — `.hph`
Write physics with its units. Dimensions are checked when the project builds, and every unit is converted to SI base measures before any C# exists.
A .hph file is physics written with its units. Every quantity is checked for its dimension when the
project builds, and every unit is converted to SI base measures before any C# exists — so 72 km/h and
20 m/s are the same number, 20, and a formula that adds metres to seconds does not build.
open Physis.Mechanics
fn highway(m : Mass) : Energy ↦ kinetic(m, 108 km/h)
A project gets the library by referencing MLambda.Hilbert.Physis and importing MLambda.Hilbert.targets;
.hph files are compiled by the same build step as .hb.
Quantities and measures
- A quantity literal is a number, a space, and a measure:
9.81 m/s²,3 km,1 kWh,45 deg. Write(2 m)·vto multiply a quantity by a value —2 m·vreadsvas a measure. - A parameter names its quantity:
fn speed(d : Length, t : Time) : Velocity ↦ d / t. The result annotation is optional; when present it is checked against the body. - A constant has a quantity and a value:
constant cruising : Velocity = 72 km/h. - Any measure reduces to the base. Conversion is not a function you call: every measure is a law toward kg, m, s, A, K, mol and cd, and only the base magnitude reaches the generated code.
How the reduction works
A quantity is the term quantity(x, M, L, T, I, Θ, N, J) — a magnitude and seven exponents. Each
dimension, quantity and measure declaration is a rewrite law toward that term
(km ⇝ 1000·m, m ⇝ Length, Length ⇝ quantity(1, 0, 1, 0, 0, 0, 0, 0)), and the laws of
model Dimensional in Physis.Dimensions combine two quantities:
quantity(x, p₁, …, p₇) · quantity(y, r₁, …, r₇) = quantity(x · y, p₁ + r₁, …, p₇ + r₇)
so 72 km/h ⇝ 72·(1000·m)·(3600·s)⁻¹ ⇝ quantity(20, 0, 1, -1, 0, 0, 0, 0). A sum whose two sides have
different exponents matches no law, and that is the diagnostic. A comparison a < b is checked as the
difference a − b.
The prelude
| file | holds |
|---|---|
Physis.Dimensions |
the seven SI dimensions and the laws a quantity reduces by |
Physis.Measures |
SI base and derived measures, prefixed measures, min, h, L, deg, eV, atm, bar, kWh, cal |
Physis.Quantities |
Velocity, Force, Energy, Power, Pressure, Charge, Voltage, … |
Physis.Constants |
c, h, ħ, qₑ, k_B, N_A, G, ε₀, μ₀, mₑ, mₚ, σ, g₀ |
Physis.Mechanics |
kinetic, momentum, potentials, Hooke, work, power, gravitation, drag, orbital speed, periods, driven resonance |
Physis.Electromagnetism |
Coulomb, Gauss geometries and capacitances, Ampère fields and inductances, Faraday, eddy loss, skin depth, wave impedance, Poynting |
Physis.Electromechanics |
coils and motors, magnetic circuits and reluctance actuators, coupled inductors, Steinmetz loss, piezoelectrics, motional impedance |
See the Physis reference for every constant and formula.
Diagnostics
| code | meaning |
|---|---|
| PH0001 | two different dimensions added, subtracted or compared |
| PH0002 | an exponent that is not dimensionless |
| PH0003 | sin, exp, ln, … — or a non-.hph function — given a dimensioned argument |
| PH0004 | a value, body or argument whose dimension is not the declared one |
| PH0005 | a fn parameter with no quantity |
| PH0006 | a name after a number that is not a measure |
| PH0007 | an affine measure (°C) — use K |
| PH0008 | a measure defined in terms of itself, or scaled by a non-constant |
| PH0009 | a declared name that a Dimensional law uses as a variable |
| PH0010 | a construct .hph does not check yet |
| PH0011 | an annotation that names no quantity or dimension |