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 mica-container/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

A typed file over a pipe, a FIFO, a terminal or a socket can wait for another party, and its transfers wait the way the POSIX road’s do: a task waiting in one parks, its carrier runs other tasks meanwhile, and a ScopeDeadline armed over it cancels the wait without taking a byte from the stream. A regular file never waits for another party, so its transfers simply run at the storage’s speed. One rule follows from the parking: a transfer stands outside a synchronized statement, as a POSIX-road read does, because a task never parks while it holds a mark.

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.