13Implementation

Pack a polymorphic value

Read the type path first

Begin with the signature of bitsOf, not its TODO. The argument has unknown type t; the return has width n; and Bits#(t, n) promises a canonical mapping between them. Then read the editable declaration of encoded and the unchanged return. Finally, inspect mkTop: the public run calls the function with one four-bit value and displays the resulting bits.

Before editing, predict what must be known at that call. Its argument fixes a concrete t, the matching Bits instance fixes n, and the body must preserve the representation supplied by that instance. The ? placeholder may permit an unspecified hardware value, but it cannot establish that observable mapping.

Edit only the declaration marked TODO. Keep the polymorphic signature, proviso, return statement, package, and mkTop intact.

Reason about the minimal repair

Do not branch on possible types or assume that every t is four bits. The proviso exists so the body can use one representation operation for any supported type. Assign its result to encoded; the declared Bit#(n) checks that the packed width is the width associated with t.

After editing, Run should show the same four bits as the sample argument. That sample proves one instantiation. The explanation must also account for why the unchanged definition can instantiate at other widths.

Observable completion contract

A complete implementation obeys the Bits instance at every call:

• False and True map to their one-bit representations;
• a UInt#(3) returns exactly three bits with the same packed pattern;
• a Bit#(4) returns all four input bits unchanged;
• the body contains no fixed-width assumption or complement operation.

Progressive hints

Transfer experiment

After the sample works, add two typed locals in mkTop, one Bool and one UInt#(3), and display separate calls. Predict the return width of each before compiling. Remove the experiment afterward; its purpose is to verify that the same definition is instantiated independently at each type.