The last article moved text. This one moves values: WriteValue writes one value’s bytes and ReadInto reads them back, each monomorphized per type through the same generics machinery every other generic verb uses — so the transfer size is the type’s own layout, known at compile time, and nothing is guessed at run time.

The working example is examples/TypedTransfers:

make -C examples/TypedTransfers run

One record per call

type
    Quality = (Good, Suspect, Bad);

    Measurement = record
        stamp : int64;
        celsius : float64;
        grade : Quality;
        accepted : bool;
    end;

...
m.stamp := 100; m.celsius := 21.5; m.grade := Good; m.accepted := True;
WriteValue(address f, m) on fail leave;

The record travels as its 24 bytes — fields, padding, done. Reading is the mirror, through an explicit pointer:

ReadInto(address f, address m) on fail leave;

ReadInto fills the value behind address m rather than returning one, for two reasons that reinforce each other: a type parameter only in return position would give the call nothing to infer from, and the pointer keeps the transfer’s destination visible at the call site — the same consent marker every mutation in Mica carries.

WriteValue declares its value parameter const x : T — the callee’s promise never to write it. The call site does not change, and for a large plain value — a full matrix, say — the promise is also the performance: a const aggregate travels as one address into your own storage, so writing a tensor to disk copies nothing on the way to the call.

The plain constraint is the point

WriteValue and ReadInto demand that T is plain: raw fixed-size value transport. Every primitive, enumeration, subrange, and set is plain by kind; a record or fixed array is plain exactly when every part is. One string or array of field anywhere, and the instantiation does not compile.

That refusal is the design. A string is a heap-backed descriptor — its bytes are a pointer and a length, not its text. C’s fwrite(&s, sizeof s) will cheerfully write the descriptor, and the program that reads it back owns a pointer into a heap that no longer exists. In Mica that entire corruption class is unrepresentable: the program that would commit it is refused at compile time, with the constraint named. This is the same compile-time-first instinct behind the heap proofs — make the bug a type error, and the run-time never meets it.

The kingdoms hold here too: a stream error mid-transfer fails with its reason, while transferring through a closed File — or reading past the end your own AtEnd check disproved — traps, the file counterpart of the map’s missing-key trap.

A file you index like an array

Because every record travels as the same number of bytes, offset arithmetic is record arithmetic — record k starts at byte k * SizeOf(m), and Seek counts exactly that unit:

span := SizeOf(m) as int64;
total := Size(f) on fail leave;
WriteLn("  file holds %lld records", total / span);

Seek(address f, 1 * span) on fail leave;
ReadInto(address f, address m) on fail leave;

No index structure, no directory, no parsing — the layout is the address arithmetic. This is file of T, Pascal’s oldest good idea, carried by the generic machinery instead of a special file type.

One honest caveat rides with it: the layout is the platform’s layout. A record’s padding is the ABI’s business, so a file of records is a file for programs compiled against the same layout — a journal, a checkpoint, a device image; not an interchange format. Text, which the previous article fixed to UTF-8 interchange bytes, is the road between unlike systems.

Updates, honestly

The three modes are deliberately plain — read, write, append, no read-write hybrid — so correcting one record means rewriting the file with the correction in place. For three records that is three writes; for a real journal it is the copy-and-rename discipline every crash-safe store uses anyway, because a partly updated file is worse than a superseded one. The example’s last section does exactly this, then verifies through a fresh reader.

Transfers and deadlines: one thing to know

A typed transfer blocks the carrier that runs it, and it is not a suspension point: a task inside a transfer cannot be cancelled, so a ScopeDeadline armed over it cannot move on from it until the transfer returns. This is a pin, not an accident — Java’s Loom pins its carrier on file I/O the same way, and Trio’s cancel scopes act only at checkpoints — and the compiler says it to your face: a files-unit transfer inside a deadline-armed scope draws a compile-time warning, which also names the way out — move the transfer outside the deadline-armed scope, or read through the parking POSIX road, whose waits the deadline does cancel.

Next

Paths and directories — the other half of the file surface: path spellings as pure text algebra that cannot fail, and the directory walk that meets the filesystem and its failure channel.