Types at the Boundary: Gradual Guarantees, Blame, and the Cost of Enforcement

The contract carried by an annotation

Adding a type annotation can mean several different things: additional static diagnostics, a runtime obligation, a promise to an optimizer, or documentation without enforcement. A meaningful migration argument starts by identifying which interpretation the language implements. Siek and colleagues formulate the gradual guarantee to relate programs differing in annotation precision. Their contribution is a semantic criterion, rather than a claim that every language with an unknown type satisfies it. Type safety, static acceptance, and predictable annotation changes therefore need separate examination.

This manuscript argues that migration should be planned around boundaries and observations, rather than the percentage of source lines annotated. The relevant boundary may be a function call, a field access, a mutable alias, or an untranslated extension. A count of typed modules hides how often values traverse those boundaries and what evidence the checks establish. Our constructed cost model isolates this distinction while deliberately omitting machine timings. It provides a counterexample to monotonic performance improvement, not a measurement of an existing implementation. The practical question is whether an annotation preserves the intended contract under the surrounding language features and whether the chosen migration order makes enforcement affordable. A sound answer needs both a semantic statement and a workload-specific account of interaction.

Sources [1]

Precision is not subtyping

For the notation used here, a precise type is ordered below a less precise type: an integer annotation is below unknown. This is an information ordering, not automatically a substitutability ordering. A function type with an unknown argument does not simply become a subtype of every concrete function type. Ordinary function subtyping and information precision answer different questions, especially when arguments flow against the direction of a function value.

New and Ahmed reformulate graduality through observational approximation and embedding-projection pairs. The inspected abstract identifies these pairs as a compositional tool for reasoning about casts between more and less dynamic types. It does not justify transferring their theorem to arbitrary production extensions. For our analysis, the useful discipline is to name an observation before comparing programs: successful results, permitted errors, divergence, and sometimes identity are different observations. Saying that removing annotations does not introduce a new type failure is not saying that an arbitrary program becomes faster or terminates. Nor does it promise that adding an incorrect annotation succeeds. The information order is valuable precisely because it constrains what changes may follow an annotation edit; it is not a ranking of program quality. A migration report should state which observational relation is claimed and which operational behaviors remain outside it.

Sources [6]

Blame explains a failed interaction

Wadler and Findler introduce a blame calculus with positive and negative subtyping to characterize responsibility for failed casts. The inspected manuscript relates the familiar slogan about well-typed programs to the less precisely typed side of a crossing, under the calculus's definitions. This is more specific than a guarantee that every error message identifies the human who made a mistake. An implementation must preserve the relevant labels, polarity, and typing assumptions for the theorem to apply.

Consider an integer-to-integer callback supplied across a boundary. If its caller supplies a string, the argument obligation points toward the caller; if the callback returns a string after receiving an integer, the return obligation points toward the provider. A check that only establishes that the object is callable cannot establish either future behavior. This example is conceptual and does not claim to implement the complete blame calculus. It shows why higher-order checks defer obligations until use. In a service architecture, a single callback can traverse several adapters before invocation, so the label naming an immediate adapter may differ from the location where a defective value originated. Useful diagnostics need an explicitly chosen account of responsibility. Blame safety remains a semantic property, while comprehensible debugging is an additional engineering requirement deserving separate evaluation.

Sources [2]

Open-world calls change the proof boundary

The abstract of Gradual Typing in an Open World describes transient casts as a proxy-free design for Reticulated Python and reports a Coq proof for the Anthill Python calculus. It motivates use-site checks through higher-order and mutable values and through the difficulties proxies create for identity and foreign interfaces. The supported claim concerns the formalized open-world setting; it is not evidence that arbitrary native code obeys every typed invariant.

For an engineering interpretation, distinguish a trusted typed caller from an imported object whose implementation was never transformed. A boundary can inspect a list's current elements, but an untyped alias may replace an element later. Checking only once cannot establish a stable integer-list property unless the system also controls mutation, freezes the object, copies it, or validates later reads. Each response changes the operational contract. A proxy can intercept some operations but may alter observable identity; a use-site check retains identity but repeats work. This is not a universal preference for one design. It is a demand that experiments include foreign callbacks and shared aliases whenever the deployment includes them. A closed benchmark that never exercises an untransformed participant cannot establish the safety or cost of the intended open deployment.

Sources [3]

Mutable references require a temporal invariant

Siek and Vitousek's monotonic-reference proposal takes a different approach to mutable locations. The inspected abstract reports static and dynamic semantics, an Isabelle type-safety development, and primitive accesses in statically typed regions with the cost of ordinary loads or stores. Those efficiency claims belong to the proposed design and its assumptions, not to every mutable object in every gradual language.

Our interpretation is that a location's future evolution is part of its type contract. If a location becomes known to contain integers, an alias cannot later store an arbitrary string while preserving that invariant. The enforcement work can move toward refinement and writes, rather than disappearing. This movement matters to workloads with many reads and rare writes. It may be unfavorable when a flexible container is repeatedly reused for unrelated representations. The appropriate accounting unit is therefore an execution history of reads, writes, refinements, and failed updates. Counting the number of annotations says little about that history. A meaningful comparison would keep the application's required mutation behavior fixed and then ask whether each design can represent it. Rejecting a behavior that another design permits is a semantic difference, even when the rejecting implementation looks faster. Benchmark equivalence must be established before performance ratios are interpreted.

Sources [4]

Optimization evidence is configuration evidence

Vitousek, Siek, and Chaudhuri describe redundant-check elimination for transient typing and evaluate configurations involving CPython and PyPy. The abstract reports that performance depends strongly on analysis and execution environment. We do not reproduce its benchmark numbers or extrapolate them to current language releases. Its contribution here is evidence that a runtime-check design and the optimizer around it must be considered together.

An optimizer may remove a check after proving that the checked shape is unchanged along a path. That proof can fail across unknown calls, mutation, reflection, or a separate compilation boundary. A microbenchmark with an isolated arithmetic loop can consequently misrepresent a plugin-heavy application. Conversely, an implementation without optimization can misrepresent the steady-state cost of a mature design. The evaluation unit should bind source revision, annotation configuration, generated code, optimizer flags, interpreter or compiler version, and warm-up policy. Recording only an end-to-end time discards the explanatory variables needed to understand a regression. Our model uses a constant charge per crossing to make topology visible. The assumption is intentionally narrower than the cited implementation studies: it neither predicts check elimination nor represents garbage collection. Its purpose is to expose a planning error that can exist before any machine-dependent effects are measured.

Sources [5]

A boundary graph for migration planning

Represent an application as a weighted undirected graph whose vertices are modules and whose edges count interactions during a fixed workload. Undirected edges simplify exposition: a real system should retain direction and attach different charges to arguments, returns, field reads, and writes. A migration configuration assigns each vertex either typed or dynamic. Under our deliberately simple model, only edges connecting different assignments incur a contract charge. The total is the weighted cut of the configuration, multiplied by a constant cost per interaction.

This formulation immediately identifies a missing variable in annotation percentages. Two configurations with the same number of typed modules can cut completely different edges. Moreover, adding a type can create a boundary on one side of a module while eliminating one on the other. There is no algebraic reason for the total cut to decrease at every step. The example assumes all checks succeed, all workloads remain identical, and all typed-to-typed interactions have no added charge. These assumptions favor a clean interpretation but exclude many actual costs. Static optimization inside typed modules could offset boundary work; persistent wrappers could impose costs even after subsequent crossings; allocation could dominate both. Such extensions should be added as separate terms, so the graph's explanatory role remains inspectable rather than becoming a fit to unexplained timing data.

A constructed counterexample to smooth migration

Take four modules on a path with interaction weights ten, one hundred, and ten. The baseline work is one thousand abstract units, and each mixed interaction costs two additional units. Migrating contiguous prefixes produces cut weights zero, ten, one hundred, ten, and zero. The corresponding normalized costs are 1.00, 1.02, 1.20, 1.02, and 1.00. Thus the second annotation step increases the constructed cost even though it adds static information. These values are generated by the accompanying model, not observed from a gradual compiler.

At exactly two typed modules, there are six possible assignments. Typing the two middle modules cuts the two light edges, whereas typing either contiguous endpoint pair cuts the heavy edge. This makes migration order a constrained partitioning problem rather than an automatic march toward lower overhead. The model enumerates every assignment to verify minimum and maximum cut weights at each typed-module count; its first figure plots those envelopes and the prefix trajectory. A separate exhaustive check shows that complementing every assignment leaves the cut unchanged. That symmetry is a feature of this simplified undirected model, not a claim about typed and dynamic implementations. The counterexample survives any positive constant charge on the heavy edge, while its numerical magnitude depends directly on the chosen workload weights.

Repeated wrapping and bounded checks

A second constructed illustration separates boundary frequency from retained enforcement history. Suppose a value crosses the same compatible boundary repeatedly and a naive representation retains one wrapper per crossing. If every later invocation traverses the whole retained chain, the accumulated number of wrapper visits after m crossing-and-call steps is m times m plus one divided by two. A hypothetical normalized representation retaining one equivalent check performs m visits. At twenty steps, these counts are 210 and 20. The figure describes operation counts under these assumptions; it does not claim that the cited runtimes use naive unbounded chains.

The difference is useful because a snapshot of one call can hide the history that produced its representation. A realistic evaluation should record both the number of boundary crossings and the maximum retained wrapper depth, then distinguish allocation cost from invocation cost. Normalization itself requires a semantic argument: combining checks must preserve failure behavior and the intended blame information. A faster representation that changes which side is blamed is not automatically an equivalent optimization. Conversely, retaining detailed histories may be a deliberate debugging feature with a measurable cost. This model's check compares the closed-form count against explicit summation, including zero steps. It validates the arithmetic used in the illustration, while leaving the design of a semantics-preserving normalization algorithm as a separate research question.

A falsifiable migration experiment

The proposed empirical study would select applications with callbacks, container mutation, and foreign interfaces, then pre-register semantically equivalent annotation configurations. For each application, record the weighted boundary graph from a fixed input trace and estimate whether it predicts the ordering of observed overheads. Prediction should concern ranks and residual structure before a coefficient is fitted. A positive correlation found only after choosing convenient configurations would be weak evidence. The decisive failure case is a stable workload where large cut changes do not explain costs even after check elimination and internal optimization are separately measured.

Each run should verify output equivalence and expected blame outcomes before its timing contributes to a performance comparison. Include deliberately bad arguments, bad returns, and mutation through an untyped alias, since all-success traces do not exercise enforcement. Repeat runs across fresh processes and warmed executions, reporting distributions rather than a single best time. Keep failed or timed-out configurations in the report; their omission would make a difficult migration appear smoother than it is. Finally, analyze annotation order as an intervention. A proposed partition-aware order should be compared with source-order and random feasible orders, under the same annotation budget. This protocol has not been executed here. The executable supplement validates only the finite analytical examples and their stated properties.

What safety and performance do not establish

Even a verified gradual guarantee cannot show that a program implements the user's business rule. An integer-valued payment routine can still compute the wrong amount. Blame safety similarly does not prove termination, resource bounds, confidentiality, or race freedom unless the formal system explicitly includes those properties. The lesson is not that types are unhelpful; it is that a theorem should retain its quantifiers, language fragment, and observational assumptions when it becomes an engineering promise.

Our boundary model also omits heterogeneity. Some checks inspect a single tag, while others traverse data or allocate wrappers. Workload frequencies can change after optimization, and failure paths can dominate latency for hostile or malformed inputs. Real modules may not admit an independent typed or dynamic choice because of inference, imports, or mutually recursive definitions. The two-state graph cannot represent those constraints without extension. These limitations produce testable refinements: use directional edges, attach shape-specific charges, and model legal annotation dependencies. They also impose a reporting obligation. If an application cannot be transformed without changing its behavior, its configuration should be labeled unsupported rather than assigned a favorable timing. A migration strategy is useful only when its improvements preserve the contract that motivated typing in the first place.

The appropriate unit of trust

The combined argument favors a boundary-centered account of gradual typing. An annotation describes intended information, an enforcement strategy determines when that information is checked, and an operational semantics determines what observations are preserved. Performance depends on how often the relevant interactions occur and on what enforcement evidence can be reused. None of these quantities is recoverable from a percentage of annotated code alone.

For an adopting team, the concrete deliverable should be a migration map that names hot boundaries, mutable aliases, untranslated participants, and the permitted error behavior. The map can guide experiments without pretending that a graph cut proves runtime safety. A language implementer has a complementary responsibility: specify which guarantee is supported, identify extensions outside the proof, and provide diagnostics that expose retained checks and eliminated checks. Researchers can then compare comparable contracts instead of collapsing distinct designs into one speed contest. The strongest next result would combine a machine-checked semantic account with a reproducible execution study whose annotation configurations are fully available. Until that evidence exists for a particular deployment, the justified conclusion is narrower: the supplied models establish that migration cost can be nonmonotonic and history-sensitive under explicit assumptions. They identify questions to measure, while the selected sources explain why those questions belong to the semantics as well as the implementation.

Mathematical model

Reproducible analytical figures

Assumptions: Undirected interactions; Identical successful workload; No typed-internal optimization

CSV data · Vector figure

Assumptions: One wrapper added per crossing; Call traverses every retained wrapper; Normalization is hypothetical and requires semantic validation

CSV data · Vector figure

Executed finite checks

4 check groups passed. The listed cases validate this model; they are not independent experiments or system benchmarks.

• Complement symmetry of every graph cut · 16 cases. Exhaustive four-vertex assignments.
• Expected cut matches independent Bernoulli enumeration · 5 cases. Exact Fraction probabilities, including p=0 and p=1.
• Migration is nonmonotonic and envelopes contain trajectory · 5 cases. All configurations at each typed-module count enumerated.
• Wrapper formula agrees with explicit step summation · 101 cases. Includes zero; counts visits, not runtime timings.

Comparison

Proposed validation protocol

• Pin language, compiler, runtime, optimizer flags and source revision.
• Define successful results, failures, divergence and identity observations.
• Enumerate legal annotation configurations and record exclusions.
• Include callback arguments, callback returns and mutable aliases.
• Record boundary frequencies and retained wrapper depth on fixed traces.
• Run semantic conformance checks before timing each configuration.
• Compare cold-process and warm execution distributions.
• Compare partition-aware, source-order and randomized migration orders.
• Publish raw outcomes including failures and unsupported configurations.
• Use an independent checker for model arithmetic and retain all counterexamples.

Limitations

• Only a four-node graph is exhaustively enumerated.
• Cost units are constructed and do not predict a particular runtime.
• The undirected cut excludes polarity and check heterogeneity.
• ArXiv abstracts support scoped claims; proof artifacts were not rerun.
• The wrapper normalization is hypothetical and requires an independent semantic proof.
• No empirical application study or human peer review was conducted.

Open research questions

• How much of migration overhead is explained by the weighted boundary cut after check elimination?
• Which diagnostic histories can be compressed while preserving intended blame observations?
• How do mutable aliases and foreign participants change the best migration order?

Evidence and its boundaries

[1] The gradual guarantee relates annotation precision and behavior.

Not every optionally typed language satisfies it. Inspected: Abstract and introduction.

[2] Blame calculus distinguishes positive and negative blame obligations.

No general claim about human responsibility. Inspected: Abstract and introduction.

[3] Transient casts are presented with an open-world soundness result for Anthill Python.

Coq development and native interfaces not independently audited. Inspected: Author abstract.

[4] Monotonic references offer distinct reference-access costs and a mechanized type-safety development.

Abstract scope; not an implementation benchmark here. Inspected: Version-2 abstract.

[5] Transient-check optimization and execution environment affect observed performance in the authors study.

Their benchmarks were not repeated and current versions are not inferred. Inspected: Abstract.

[6] Embedding-projection pairs support a semantic account of graduality.

Logical-relations proofs were not reconstructed. Inspected: Abstract and ICFP publication note.

References

1. Refined Criteria for Gradual Typing
   Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, John Tang Boyland. SNAPL; inspected author manuscript (2015). https://jsiek.github.io/home/refined-criteria-gradual.pdf
   Source access and scope

   Abstract, introduction, selected gradual-guarantee definitions; author PDF has placeholder proceedings metadata.

2. Well-typed programs can't be blamed
   Philip Wadler, Robert Bruce Findler. ESOP 2009; author technical report (2009). https://users.cs.northwestern.edu/~robby/pubs/papers/esop2009-wf.pdf
   Source access and scope

   2009 technical report cover, abstract, introduction and higher-order blame discussion; appendix proof development not independently audited. This version replaces the earlier 2008 submission URL during team review.

3. Gradual Typing in an Open World
   Michael M. Vitousek, Jeremy G. Siek. arXiv (2016). https://arxiv.org/abs/1610.08476
   Source access and scope

   Author abstract and submission record; Coq artifact not executed.

4. Monotonic References for Gradual Typing
   Jeremy G. Siek, Michael M. Vitousek. arXiv, version 2 (2014). https://arxiv.org/abs/1312.0694
   Source access and scope

   Abstract and version history; detailed Isabelle development not audited.

5. Optimizing and Evaluating Transient Gradual Typing
   Michael M. Vitousek, Jeremy G. Siek, Avik Chaudhuri. arXiv (2019). https://arxiv.org/abs/1902.07808
   Source access and scope

   Abstract, author list, submission record; reported benchmarks not reproduced.

6. Graduality from Embedding-projection Pairs (Extended Version)
   Max S. New, Amal Ahmed. arXiv; ICFP extended version (2018). https://arxiv.org/abs/1807.02786
   Source access and scope

   Abstract and publication note; logical-relations proof not reconstructed.