This is part 3. Part 2 read a program whose variables each had one type and stayed there. Real programs move values between types constantly, and that is where languages quietly differ: what happens to a number that will not fit where it is being put, and whether you were told.

Mica’s answer is one rule with two halves. A value moving to a wider type is promoted on its own, because nothing can be lost. Every conversion that can lose something is written down as an explicit as cast. Nothing narrows silently — but nothing traps either, which is the part worth understanding properly.

The example is examples/Cast. Keep it open.

make -C examples/Cast run
Cast — promotion and explicit casts

Widening happens on its own
  int32 literal into int64:     42
  int32 value into int64:       1000
  float32 value into float64:   2.500000

Narrowing is written down
  127 as int8:                  127
  -42 as int16:                 -42
  3.14159265359 as float32:     3.1415927410
  ... widened back to float64:  3.1415927410

What a narrowing cast costs
  3000 as int8:                 -72
  300 as uint8:                 44

The example, walked

Widening needs nothing

i64v := 42;

source := 1000;
i64v := source;

Both assignments put a 32-bit value into a 64-bit variable, and neither one says anything about it. Every int32 value is an int64 value, so there is nothing to decide and nothing to lose. Writing a cast here would add a word that says only what the two types already say.

Note that the second one is a variable, not a literal. It is the types that decide whether a conversion is safe, not whether the compiler can see the value.

Floating point works the same way — with one wrinkle:

f32v := 2.5 as float32;
f64v := f32v;

The second line is a plain promotion. The first needs a cast, and the reason is that 2.5 is a float64 — a fractional literal is double precision unless you say otherwise, so putting it in a float32 is already a narrowing.

Narrowing is written down

i8v := 127 as int8;
i16v := -42 as int16;

as is the explicit cast, and it is required whenever the destination is narrower than the source. Both values above fit comfortably, so nothing is lost — but the cast is still there, and that is deliberate. A reader scanning this file never has to work out where a value quietly changed width; the places where it could have are the places where as appears.

What float32 does to π

f32v := 3.14159265359 as float32;
f64v := f32v;
  3.14159265359 as float32:     3.1415927410
  ... widened back to float64:  3.1415927410

A float32 holds roughly seven decimal digits. π arrives with far more, and the cast keeps what fits: 3.1415927. The second line is the one to look at. Widening back to float64 does not restore the lost digits — it only gives the value room to be printed. A cast changes a value’s type; it cannot recover its history.

What a narrowing cast costs

i64v := 3000;
i8v := i64v as int8;
  3000 as int8:                 -72

3000 does not fit in an int8, and Mica neither refuses this nor traps at runtime. The cast keeps the low eight bits of the two’s-complement representation: 3000 is 0x0BB8, the surviving byte is 0xB8, and read as a signed int8 that is −72.

This is the design worth being explicit about. Mica does not stop you from narrowing a value that does not fit — it stops you from doing it by accident. The information loss is real, it is defined rather than undefined, and it is visible in the source at the exact point it happens.

One place the rule is stricter: constants. When both operands of an expression are compile-time constants, the exact value exists at compile time — so an expression that overflows the type it computes in is refused outright, on every tier, with the exact value and the width that would hold it named in the message. A named constant’s value never moves with the optimization tier.

The unsigned case truncates identically and reads the surviving bits as unsigned: 300 is 0x012C, the byte that survives is 0x2C, and that is 44.

Try it

1. Delete a cast. Remove as int8 from the 3000 line, so it reads i8v := i64v;, and rebuild:

analyzer error 5143: incompatible data types in assignment to i8v: int64 to int8

The compiler will not narrow on your behalf. A conversion that can lose information exists in this program only where you can read it, and this message is that rule holding its ground. Put the cast back.

2. Predict a truncation, then check it. Change 3000 to 200 and work out the answer before you build: 200 is above int8’s maximum of 127, so it wraps to 200 − 256. Rebuild:

  3000 as int8:                 -56

−56, as predicted. (The label still says 3000 — it is a fixed string in the WriteLn beside the calculation. Change it too, and notice that nothing in the language kept those two in step for you.)

3. Find where float32 gives up. Change the printed precision on the π line from %.10f to %.20f and rebuild:

  3.14159265359 as float32:     3.14159274101257324219

Line those digits up against π itself — 3.14159265358979… — and they agree to 3.1415927 and then part company. What follows is not π and not noise: it is exactly what the stored 32-bit value means, printed in full. Nothing invented those digits and nothing rounded them away; they were simply never π’s.

What the compiler proved

Every conversion in this program that could lose information is visible in the source, because the compiler refuses to perform one you did not write. Every conversion that cannot lose information happened without ceremony. And the narrowing that does lose information has a defined result rather than an undefined one, so the answer is the same on x86-64 and ARM64 — you saw the same −72 whichever machine you ran it on.

What Mica takes from you here is the ability to be surprised. What it does not take is the ability to truncate deliberately, which systems code needs.

Next

Choices and repetition — part 4: the two ways a program decides and the three ways it repeats, each loop stating what it knows before it runs. Every example behind the series lives in the tutorial repository, in learning order, each with a header that says what it teaches.