Laws and deriving

Laws record algebraic propositions. Deriving builds ordinary instances from checked derivation logic. Neither feature creates proof or optimization trust by assertion alone.

Declaring laws

law associativity(x:a, y:a, z:a) =
    combine(combine(x,y),z) === combine(x,combine(y,z));

law transitivity(x:a, y:a, z:a) =
    (x <= y) === True ==>
    (y <= z) === True ==>
    (x <= z) === True;

=== forms propositional equality. ==> is right-associative implication. A law must type-check and is inherited with its structure.

What declaration does not mean

A law declaration does not automatically:

• construct an equality proof;
• make the proposition true at runtime;
• authorize a compiler rewrite; or
• bypass floating-point exceptional cases.

Law status may be declared, tested, proven, trusted by build policy, or compiler-validated according to the semantic design. The default surface law is a well-typed, testable proposition.

Derive blocks

algebra Show(a:Type) = {
    function show(item:a) : String;
    derive {
        function show(item:a) : String =
            structuralShow(reflect(item), item)
    }
};

Reflection used by derivation is compile-time, typed, and target-neutral. TypeRep(a) identifies the checked type, while DataShape/DataCode preserve its constructor and flat field telescopes without exposing native offsets or storage. A data declaration can request the result:

type Color = Red + Green + Blue deriving Eq, Show;

Each algebra must provide valid derivation logic. The generated instance goes through ordinary member, evidence, coherence, and law checks.

For parameterized data, field requirements are inferred:

type Box(a:Type) = Box * item:a;
instance Eq(Box(a)) = derive;

The generated equality provider requires Eq(a). Closed field requirements are resolved while deriving; missing or ambiguous closed evidence is an error. An explicit requires clause must cover every requirement the recipe discovers.

Recipes may also request supporting evidence or reject generation directly:

function checkedShow(item:a) : String =
    let available = requireEvidence(Show(String)) in
    structuralShow(reflect(item), item)

requireEvidence is handled during derivation and never becomes a runtime call. rejectDerivation(error) stops generation with a structured static diagnostic. These are compile-time capabilities, not general runtime effects.

Computing data from typed codes

DataCode can also be transformed by ordinary pure Tulam helper functions:

type Source(a:Type) = None + Some * item:a;

function schema(code:DataCode(Unit, Z)) : DataCode(Unit, Z) =
    renameConstructor(
        renameConstructor(renameDataType(code, "Generated"),
            "None", "Absent"),
        "Some", "Present");

type Generated(a:Type) = schema(dataCode(reflect(Source(a))));

The computed body must return a code whose name and parameter arity match the declaration. The compiler materializes normal constructors, then runs the same positivity, coverage, type, evidence, and native gates as handwritten data. Opaque type shape and target layout cannot be inspected this way.

Classes choose semantics explicitly

implements Eq(Key) means matching class methods define class-owned equality. It does not silently switch to structural equality. Structural class behavior uses a separate instance Eq(Point) = derive and is allowed only for a sealed leaf class, where the field shape is closed.

Laws versus tests

A test observes selected values; a law states a proposition over all values in its binders. Property testing may sample a law when generator evidence exists, but successful samples are not a proof. Both remain useful and honestly named.

Common mistakes

Do not treat a declared law as Refl, an optimizer permission, or proof that floating arithmetic obeys exact field identities. Do not use runtime reflection where a compile-time DataCode is required, inspect provider layout from a derive recipe, or assume class implements derives missing behavior. A derived instance still has to satisfy ordinary typing, coherence, and law policy.

Recap

Laws preserve named propositions; deriving supplies checked implementation logic. Proof, testing, trust, and optimization eligibility remain explicit separate statuses.

Normative details: Language Reference §9.6, §10, and §11.7-11.9.