2026-03-05 00:55:40
I’ve spent the last 10 years building enterprise data pipelines and infrastructure. If there is one thing I’ve learned about moving data at scale, it’s that giving any single entity "God-mode" access to a production infrastructure and resources is a resume-generating event.
Yet, as we transition from basic SaaS wrappers into the era of Agentic Workflows, where autonomous AI agents handle customer success, procurement, and infrastructure scaling, we are making a catastrophic architectural mistake.
We are giving probabilistic agents deterministic root-level API keys.
We are handing a LangChain orchestrator a production Stripe API key, pointing it at a customer, and relying on a polite system prompt ("Please do not refund more than $50") to prevent a financial disaster.
If you are a CTO, this should terrify you. A 99.9% compliance rate in your testing sandbox is meaningless when a single 0.1% hallucination in production drops your entire CRM database.
When software breaks, the engineering instinct is to build better CI/CD pipelines. We want to run the agent through 10,000 synthetic simulations before merging the PR. We want to measure its failure rate.
But here is the hard truth about LLMs: testing an agent 10,000 times in a sandbox does not mathematically guarantee it won't hallucinate on attempt 10,001 in the real world. You cannot use deterministic DevOps pipelines to validate non-deterministic software.
In enterprise infrastructure, if you cannot cryptographically prove an agent won't execute a destructive action, you cannot deploy it. The solution isn't better testing. The solution is hard, deterministic constraints at runtime.
If AI agents are going to act as digital employees, they need their own Identity and Access Management (IAM) layer. They need an Agentic Firewall.
Instead of injecting your root API keys into the agent’s context environment, you issue the Agent a scoped, ephemeral "Proxy Token." When the agent makes a tool call, it hits an interceptor, a specialized reverse proxy sitting between the agent and the external world.
How do you actually build this without adding 2 seconds of latency to every LLM turn? You don't build it in Python. You build it at the network edge using a high-performance proxy like Envoy or Kong, augmented with a WebAssembly (Wasm) or Rust-based policy engine.
Here is what the architecture looks like in production:
The Interception Layer: The agent (running via LangGraph, CrewAI, or Agentforce) decides it needs to execute a tool call (e.g., POST /v1/refunds). It sends the HTTP request using its Agent-Proxy-Token.
The Edge Gateway (The Choke Point): The request hits your internal API Gateway (the Agentic Firewall). Before the payload is ever forwarded to Stripe or Salesforce, the gateway inspects the JSON body.
Deterministic Evaluation: The firewall evaluates the payload against a strict, human-defined policy graph. This isn't an LLM guessing if the action is safe, this is a deterministic rules engine executing in under 5 milliseconds.
The policy looks something like this:
\
agent_id: "customer_success_bot_01"
allowed_endpoints:
- path: "/v1/customers/*"
methods: ["GET"]
- path: "/v1/refunds"
methods: ["POST"]
constraints:
max_amount_usd: 50
require_human_approval_over: 20
/refunds? (Yes).
< $50? (The hallucinated amount is $50,000. Violation).
403 Forbidden: Policy Violation error back to the agent. The agent is forced to rethink its strategy or, ideally, escalate the ticket to a human operator. The real Stripe API is never touched.\
Basic API blocking (checking a JSON key for a dollar amount) is fast. But the main job of an Agentic Firewall is Semantic DLP (Data Loss Prevention) and intent evaluation.
What happens when an agent sends an email via the SendGrid API? The API endpoint (POST /mail/send) is valid, but the content of the email might contain unredacted PII, a catastrophic GDPR violation.
To solve this, the next generation of Agentic Firewalls will run parallel, hyper-fast "Guardrail Models" (like a quantized Llama-3 running locally or a specialized BERT model) that evaluate the semantic intent of outbound payloads.
Because it uses a proxy sidecar architecture, the deterministic rules execute instantly, while the semantic checks run asynchronously on the payload. If the firewall detects PII, it cryptographically masks it (replacing "John Doe" with "[ENTITY_1]") before it hits the wire, ensuring Sovereign Data Residency is never compromised, adding only 50-100ms of overhead.
\
Finally, this architecture solves the biggest legal hurdle blocking enterprise AI adoption: the audit trail.
When a human makes a mistake, you check the logs. When an AI makes a mistake, it’s a black box. By routing all agentic tool calls through a centralized firewall, you automatically generate an immutable ledger of every decision the agent made, the context it had when making it, and the payload it attempted to send.
If a regulatory body knocks on your door asking why an agent made a specific decision, you don't show them the LangChain code, you show them the cryptographic ledger from the firewall.
\
Governments and regulatory bodies are not going to tolerate "black box" agentic deployments. They will demand immutable audit logs of every AI decision and strict, deterministic data residency controls.
The companies that win the next decade won't necessarily be the ones that build the smartest agents. They will be the ones that build the infrastructure that makes those agents safe enough to actually turn on.
2026-03-05 00:49:24
Insurance is one the last major industries still operating in an archaic world. In 2026, a 25-year old who drives cautiously and hasn’t had a single incident can still be priced the same as a reckless driver simply because they share the same age bracket. A careful traveler pays for the risks of someone else’s bad habits. Modern insurance models still rely on parameters of age, zip code, and vehicle model because they were built for a world where real-time data was scarce and policies had to be static to be manageable.
An AI Agent understands intent when a user says–”I’m renting a sedan for a three-day trip”. It then evaluates real-time risk signals, negotiates coverage with providers, and activates your protection instantly by settling the payment using stablecoin rails. Therefore, instead of buying insurance, you can enter and exit protection continuously. Your traditional insurance safety net becomes elastic–expanding when risk arises, contracting when it doesn’t.
So how do agentic systems alter the course of the insurance industry?
In an agentic insurance model, the AI Agent continuously monitors and adapts to risk on the user’s behalf by leveraging contextual awareness. Agentic systems ingest real-time signals from IoT devices and telematics: vehicle speed, braking patterns, GPS location, weather conditions, road quality, etc. These signals are combined with historical behavior to form a living picture of risk—one that updates minute by minute, not once a year.
Imagine starting a long road trip. As heavy rain rolls in and traffic slows, your conversational agent intervenes with a contextual update–”I can shift your coverage to Premium for the next four hours due to heavy rain. The $5.60 one-time cost will be paid in stablecoins.” A simple “Yes’ from the user triggers immediate execution where the smart contract adjusts your coverage, payment is settled using stablecoin rails, and the agent logs the action for auditability. When the weather clears, the risk diminishes and your coverage automatically reverts.
Insurance moves from a product you purchase to a service that follows you. It is priced based on what’s happening right now, instead of who you areand behaves like a safety net that adapts to real life as it unfolds. \n
Today, entire populations operate without meaningful coverage not because they reject insurance but because traditional insurance rejects them. While annual contracts assume stability, emerging markets, gig workers and micro-entrepreneurs don’t have it. Agentic insurance reframes this narrative by asking “Can you afford $0.18 to insure this delivery for the next 42 minutes?“ instead of “Can you afford a $1,199 annual premium?“
A delivery driver in Nairobi may not afford an annual cargo policy. But insuring a single high-value package for one hour? That’s within reach. Insurance becomes granular and contextual by becoming a micro-utility that is purchased only when risk exists. The barrier to entry drops from “prove long-term stability” to “prove short-term intent.”
The deeper shift is that agentic insurance operates as a preventative model. Because your premium updates in real time, your AI agent has an incentive to actively reduce risk before a loss occurs.
If your car’s sensors detect speeding in heavy rain, your agent nudges you to slow down — not morally, but economically. \n If you’re about to leave expensive equipment unattended, the agent alerts you — not as a courtesy, but as cost optimization.
Insurance becomes a feedback loop and protection stops being something you buy and forget. Your agent acts as a risk concierge, constantly optimizing behavior to minimize exposure. Protection becomes something that follows you — adapting, negotiating, and incentivizing safer choices moment by moment. \n
“Living” insurance comes with a cost. The efficiency gains of hyper-personalized insurance depend on real-time visibility into location data, telematics, environmental sensors and financial behavior. Precision requires visibility but visibility without guardrails becomes exploitation. If insurers can see everything, they can price everything. So how do we ensure that insurers do not have a monopoly over pricing?
Enter an architectural accountability layer where users must own their data sovereignty. That means:
The insurer doesn’t need your full driving record. It only needs cryptographic confirmation that your risk score falls within an agreed band. With that, insurance becomes both hyper-personalized and privacy preserving. \n
Agentic insurance promises to close the protection gap, incentivize safer behavior, and democratize access to coverage at a global scale. But it only works if users believe the agent works for them and not for the insurer.
Hyper-personalized insurance will be realized when we build systems where precision does not require permanent surveillance and protection does not demand surrender.
In a world where your AI negotiates your coverage in milliseconds, the real premium you pay isn’t just financial. It’s informational. And that’s the trade we have to get right.
2026-03-05 00:37:02
Ensemble ML is everywhere - every blog post, every conference talk claims "combine multiple models for better results." But does it actually work in production?
I built a data quality monitoring system to find out. Three ML models (Isolation Forest, LSTM, Autoencoder) are working together. 332K synthetic orders processed over 25 days.
Here's what actually happened.
"Use ensemble methods" is the standard advice for ML in production. Combine multiple models, get better predictions, and reduce false positives.
Sounds great in theory. But I wanted to know:
So I built it. Ran it continuously. Measured everything.
Stack:
Data: Synthetic e-commerce orders with realistic quality issues injected.
Goal: Compare single model vs. ensemble. Which catches more real issues? Which has fewer false positives?
\
Started with just Isolation Forest - the standard choice for anomaly detection:
\
from sklearn.ensemble import IsolationForest
# Train on 24 hours of quality metrics
historical_data = get_metrics(hours=24)
model = IsolationForest(contamination=0.1)
model.fit(historical_data)
# Predict
is_anomaly = model.predict(current_metrics)
Week 1 Results:
The false positive rate was the killer. Every 6-7 alerts, one was wrong. Teams started ignoring alerts.
Before adding more models, I needed to understand why the single model flagged things:
\
import shap
explainer = shap.TreeExplainer(model)
shap_values = explainer.shap_values(current_metrics)
# Now I get:
# "Primary driver: validity_score = 45.2 (30% below baseline)"
This helped debug false positives. But didn't reduce them.
That's when I decided to try the ensemble approach everyone talks about.
The theory: Different algorithms catch different problems.
Model 1: Isolation Forest (40% weight)
Model 2: LSTM (30% weight)
Model 3: Autoencoder (30% weight)
Voting strategy:
\
ensemble_score = (
isolation_score * 0.4 +
lstm_score * 0.3 +
autoencoder_score * 0.3
)
# Flag if:
# - Combined score high, OR
# - At least 2 models agree
is_anomaly = ensemble_score > 0.5 or votes >= 2
\ After 25 days processing 332K orders:
Metric Single Model Ensemble Improvement
─────────────────────────────────────────────────────────────
Accuracy 93.2% 93.8% +0.6%
False Positives 15% 9.7% -35%
Real Anomalies Caught baseline +30% +30%
Inference Time <5ms <5ms same
Training Time <1 min 3 min acceptable
The big wins:
The cost:
Example 1: Isolation Forest Alone
Sudden spike in missing fields. Obvious outlier.
Example 2: LSTM Alone
Completeness scores dropping 8% over 6 hours.
Example 3: Autoencoder Alone
Unusual combination: low volume + high value + weekend.
Example 4: False Positive Reduction
Weekend pattern that's unusual but valid.
This is where ensemble shines - reducing false positives through voting.
\
YES, but with conditions:
When ensemble is worth it: You need low false positive rate (<10%). Different anomaly types exist (temporal, statistical, combinatorial) You can afford 3x training time You have enough data for 3 models
When single model is enough: False positives aren't a big problem Only one type of anomaly. Need fastest possible training. Limited data
For data quality monitoring specifically, Ensemble is worth it.
Why? False positives kill trust. Teams ignore alerts if too many are wrong. Reducing 15% → 9.7% false positives makes the system actually usable
\
Both single model and ensemble faced the same issue: concept drift.
After 2 weeks, accuracy dropped from 93% to 78%.
Solution: Statistical drift detection with auto-retraining:
\
from scipy.stats import ks_2samp
reference = get_baseline(feature, hours=24)
current = get_recent(feature, hours=1)
statistic, p_value = ks_2samp(reference, current)
if p_value < 0.01:
retrain_all_models()
This works for both single model and ensemble. Not specific to ensemble approach.
Inference (per order):
Training:
Training every 2 hours, so 3 minutes is acceptable. Inference is still <5ms, fast enough for real-time.
\ Optimization used:
python
# Run 3 models in parallel
with ThreadPoolExecutor(max_workers=3) as executor:
if_result = executor.submit(isolation_forest.predict, data)
lstm_result = executor.submit(lstm.predict, data)
ae_result = executor.submit(autoencoder.predict, data)
Without parallelization: 12ms. With: 4.8ms.
Orders Processed: 332,308
Quality Checks: 2.8M+
System Uptime: 603.7 hours (100%)
Average Latency: 4.8ms per order
Ensemble Performance:
Comparison to Single Model:
False Positives: -35% improvement
Real Anomalies: +30% more caught
Inference Time: +14% slower (acceptable)
Training Time: 4x slower (acceptable)
\
1. Ensemble DOES reduce false positives
Not by a little. By 35%. This matters a lot for trust.
2. Different models catch different things
Not marketing fluff. Actually true. IF catches outliers, LSTM catches temporal, AE catches combinations.
3. Voting is powerful
When 2/3 models say "not anomalous," they're usually right. This reduces false alarms.
4. The complexity is manageable
Three models instead of one isn't 3x the work. Maybe 1.5x once you have infrastructure.
5. But you need enough data
Each model needs reasonable training data. If you have <100 samples, single model is better.
6. Explainability still required
Ensemble without SHAP is useless. Add SHAP to all three models.
YES if:
NO if:
Single model works fine
Training time is critical
Limited data (<100 samples)
Simple anomaly patterns
\ For data quality monitoring specifically: Yes.
Why? Data quality has multiple anomaly types (missing fields, wrong formats, unusual patterns, temporal issues). Ensemble catches more with fewer false alarms.
Open source: https://github.com/kalluripradeep/realtime-data-quality-monitor
Compare single model vs. ensemble yourself:
Clone the repo and run: docker compose up -d
\
Ensemble ML isn't just hype. It actually works:
For data quality monitoring, it's worth doing.
About the Author
Pradeep Kalluri is a Data Engineer at NatWest Bank and Apache Airflow/Dbt contributor.
2026-03-05 00:20:45
Comparing classic monthly DCA with concentrated liquidity on a BTC/BTC pair using real market data from 2021–2025
In this article, I simulate a simple long-term Bitcoin accumulation strategy based on regular monthly investments using the classic Dollar-Cost Averaging (DCA) approach. The idea is straightforward: invest a fixed amount every month and steadily build a BTC position over time, without trying to predict market tops or bottoms.
For the analysis, I use real historical Bitcoin price data from 2021 through 2025. This period covers a full market cycle, including strong bull runs, deep corrections, and extended sideways phases — making it a realistic test environment rather than an idealized scenario.
Many long-term investors focus mainly on entry price and timing, but much less on what happens after they buy. A DCA plan helps you build a position, but the capital itself usually sits idle between purchases. That raises a practical question: can we make the accumulation process more capital-efficient — without turning it into a high-risk trading strategy?
I then extend the strategy by adding a concentrated liquidity (CLMM) position on a Bitcoin-denominated pair, such as cbBTC/WBTC. Instead of letting the accumulated Bitcoin sit idle, the BTC purchased through DCA is deployed into a CLMM pool on this pair. The intention is not to take on additional directional exposure — since both assets represent wrapped versions of Bitcoin — but to use market activity within the pool to gradually accumulate more BTC through trading fees.
At the end of the article, I compare both approaches under identical market conditions and analyze how much Bitcoin each strategy would have accumulated over time. The goal is not to chase unrealistic returns, but to explore whether a disciplined, slightly more active approach can meaningfully improve long-term BTC accumulation.
The core idea behind DCA is simple: stay in the market consistently. Instead of trying to time tops and bottoms, we invest the same amount at regular intervals, no matter where the BTC price is.
In the simulation, I assume:
This creates a clean baseline: a disciplined, hands-off accumulation strategy that many long-term BTC holders can relate to.
After each monthly BTC purchase, the accumulated BTC is not left idle — it is deployed into a CLMM pool. Instead, it is deployed into a concentrated liquidity (CLMM) pool on a Bitcoin-denominated pair — for example, cbBTC/WBTC.
The logic here is straightforward:
In this strategy, I do not use automatic rebalancing. In the simulation, liquidity is provided within a fixed price range of 0.9965 to 0.9989 (expressed as cbBTC/WBTC). I keep this range constant and do not “chase” the price. If the pool price stays within the range, the position remains active and earns fees. If the price moves outside the range, the position becomes inactive and stops earning fees until it returns into range — and I simply wait rather than rebalancing immediately.
There is also an interesting practical detail: when the price leaves the range, the liquidity position can become single-sided. That situation can be used to add liquidity without performing a swap, because you may already hold mostly the asset needed for the deposit.
Range breaks often happen during strong BTC price moves, especially when arbitrage and pool rebalancing do not catch up instantly. In real markets, this can occur during sharp volatility spikes, fast trend moves, or periods of temporary inefficiency.
To keep the simulation realistic, I include the following assumptions:
These numbers are not meant to “prove” a best-case outcome — they are simply consistent assumptions that allow us to compare the baseline DCA strategy against the DCA + CLMM approach.
Range selection is one of the most important parts of making CLMM work. A simple and practical starting approach is:
A narrower range usually means better fee efficiency — but also a higher chance of going out of range. Finding the “right” balance is a topic on its own, and I plan to publish a dedicated follow-up article focused entirely on how to choose ranges for BTC-based CLMM pools. Right now, I am collecting the data.
Let’s go through the charts in more detail.
This chart shows how BTC accumulates from 2021 to 2025. You can clearly see that BTC is accumulated much faster between 2021 and 2023 than after 2023. That’s not surprising — it’s mainly a consequence of rising BTC prices. With the same monthly USD investment, you simply buy less BTC when the price is higher.
\
When comparing the two curves, the first two years look very similar. The difference is small because the BTC position is still relatively small, and the fee income from CLMM doesn’t have much capital to work with yet.
Over time, as the BTC position grows, the gap becomes more visible. The CLMM strategy starts to pull ahead because the portfolio is large enough for trading fees to make a meaningful difference.
Assumptions: in the simulation, DCA + CLMM fees are modeled as an average 5% APR, and whenever a swap between cbBTC and WBTC is required, I apply a 0.02% cost to account for fees and slippage.
Below is a numerical comparison of both strategies as of the end of 2025:
It is important to note that these results are sensitive to the assumptions used in the simulation. The final outcome depends heavily on factors such as the selected price range, the actual trading volume in the pool, and the effective fee APR. Different parameters — or a different market environment — could lead to materially different results.
Charts [2] and [3] also show that, over the long term, the DCA + CLMM strategy outperforms the classic DCA approach. The difference becomes more noticeable as the portfolio grows and fee income begins to compound.
However, beyond a certain point, the total portfolio value is primarily driven by the price of Bitcoin itself. While during 2021–2022 BTC volatility was partially absorbed by the ongoing monthly investments, by 2023 the portfolio value becomes increasingly dependent on BTC price movements.
In other words, as the accumulated BTC position grows larger, market price fluctuations begin to dominate the portfolio’s USD value, regardless of the accumulation method.
One important takeaway is that the DCA + CLMM approach tends to work best during sideways markets, where price moves back and forth within a range and trading activity generates steady fee income. DCA + CLMM performance usually drops during strong directional moves — both sharp sell-offs and aggressive rallies — because positions go out of range more often and stop earning fees.
This suggests that, if the goal is to improve BTC accumulation across all market regimes, a second component may be needed — something that can keep accumulating BTC even during highly unstable, trending periods. I plan to explore such a mixed strategy in upcoming articles.
At the same time, it’s worth highlighting what this strategy is — and what it is not. DCA + CLMM can accelerate BTC accumulation, but it still relies on the same long-term mindset as classic DCA: staying invested for as long as possible and avoiding emotional reactions to volatility. For most investors, the biggest mistake is not the choice of strategy — it’s leaving the market too early.
DCA + CLMM also introduces additional risks that do not exist in pure DCA. Once you move beyond simply buying BTC and holding it, you are trusting a DeFi protocol and using wrapped BTC assets. That means you are exposed not only to smart-contract risk, but also to the custodial and issuer risks behind the BTC wrappers.
These risks can be reduced by being selective about the protocol and the wrapped BTC assets you use. Position sizing and diversification across protocols can also help reduce exposure. The most conservative option, of course, is to skip DeFi entirely and accumulate native BTC directly to a Bitcoin address — but that comes with the trade-off of giving up any yield from liquidity provision.
2026-03-05 00:02:41
How are you, hacker?
🪐 What’s happening in tech today, March 4, 2026?
The HackerNoon Newsletter brings the HackerNoon homepage straight to your inbox. On this day, An Wang Sells Core Memory Patent to IBM in 1956, and we present you with these top quality stories. From 5 Open-Source Projects for Books and Readers to Support via Kivach to EU’s AI Omnibus: Pivoting from Regulation to Active Deployment, let’s dive right in.
By @obyte [ 6 Min read ] Are you an avid reader? Heres a tour of book-focused and free tools, and how Kivach lets you support the people building them, one small donation at a time. Read More.
By @tirtha [ 12 Min read ] Your inference stack is burning money on solved problems. A storage hierarchy would fix the part youre paying for twice. Read More.
By @raysvitla [ 2 Min read ] 15% of 2026 is gone. heres what held. Read More.
By @150sec [ 6 Min read ] EU proposes AI Omnibus to delay high-risk AI rules to 2027 and centralize enforcement, reshaping how companies comply with the AI Act. Read More.
By @proofofusefulness [ 2 Min read ] Master your content with 45 days of Storyblok Growth+ for free. Build, edit, and launch websites easily without the dev headache. Enter the $5k hackathon today! Read More.
🧑💻 What happened in your world this week?
It's been said that writing can help consolidate technical knowledge, establish credibility, and contribute to emerging community standards. Feeling stuck? We got you covered ⬇️⬇️⬇️
ANSWER THESE GREATEST INTERVIEW QUESTIONS OF ALL TIME
We hope you enjoy this worth of free reading material. Feel free to forward this email to a nerdy friend who'll love you for it.See you on Planet Internet! With love, The HackerNoon Team ✌️
2026-03-05 00:00:04
2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING
4 DESIGN CONSTRAINTS AND SOLUTIONS
\ \
Specifying a consistent set of typing and computation rules for data and codata types is not difficult. In this section, we show the difficulties that arise if we also want the rules to be closed under defunctionalization and refunctionalization. That is every program that typechecks should continue to typecheck if we defunctionalize or refunctionalize any of the types that occur in it.
\ 4.1 Judgmental Equality of Comatches
Problem. For most dependently typed languages, the term 𝜆𝑥.𝑥 is judgmentally equal to the term 𝜆𝑦.𝑦, and likewise 𝜆𝑥.2 + 2 and 𝜆𝑥.4 are considered equal. Equating such terms becomes a problem, however, if we want to defunctionalize the programs which contain them. Different lambda abstractions in a program are defunctionalized to different constructors, which are then no longer judgmentally equal. Let us illustrate the problem with an example.
\ Consider the following proof that 𝜆𝑦.𝑦 is the same function from natural numbers to natural numbers as 𝜆𝑧.𝑧. We prove this fact using a third lambda abstraction 𝜆𝑥.𝑥 as an argument to the reflexivity constructor.
codata Fun(a b: Type) { Fun(a, b).ap(a b: Type, x: a): b } Refl(Fun(Nat, Nat), \x. x) : Eq(Fun(Nat, Nat), \y. y, \z. z)
\ If we defunctionalize this program, then each of these three lambda abstractions becomes one constructor of the data type. However since different constructors are not judgmentally equal, the following defunctionalized program no longer typechecks.
data Fun(a b: Type) { F1: Fun(Nat, Nat), F2: Fun(Nat, Nat), F3: Fun(Nat, Nat) } def Fun(a, b).ap(a b: Type, x: a): b { F1 => x, F2 => x, F3 => x } Refl(Fun(Nat, Nat), F1) : Eq(Fun(Nat, Nat), F2, F3)
Here is the gist of the problem: Judgmental equality must be preserved by defunctionalization and refunctionalization. This means that if we don’t want to treat different constructors of a data type as judgmentally equal, then we cannot treat all 𝛼-𝛽-equivalent comatches as judgmentally equal either.
\ It is not impossible to devise a scheme which lifts judgmentally equal comatches to the same constructors. However, we decided against this as it leads to confusing behavior. First, de- and refunctionalization would no longer be inverse transformations at least under syntactic equality. Second, such an attempt would necessarily be a conservative approximation as program equivalence is undecidable in general. In practice, that would mean that some comatches would be collapsed to the same constructor during lifting, while others would not.
\
Solution. Note that the opposite approach—never equating any comatches—doesn’t work either, since typing would then no longer be closed under substitution. For example, if 𝑓 is a variable standing for a function from natural numbers to natural numbers, then the term Refl(Fun(Nat, Nat), 𝑓 ) is a proof of the proposition Eq(Fun(Nat, Nat), 𝑓 , 𝑓 ). But we could not substitute a comatch 𝜆𝑦.𝑦 for 𝑓 , since the result would no longer typecheck. We therefore have to find a solution between these two extremes.
\ Our solution consists of always considering local comatches together with a name5 . Only comatches which have the same name are judgmentally equal, and this equality is preserved by reduction since the comatch is duplicated together with its name. Where do the names for local comatches come from? We support user-annotated labels, which allow the programmer to give meaningful names to comatches. Manually naming comatches in this way is useful as these labels can also be used by defunctionalization to name the generated constructors.
\ We enforce that these user-annotated labels are globally unique. However, as we do not want to burden the user with naming every single comatch in the program, we also allow unannotated comatches, for which we automatically generate unique names. As a result, each comatch occurring textually in the program has a unique name, but these names possibly become duplicated during normalization and typechecking.
\ 4.2 Eta Equality
Problem. For reasons very similar to the previous section, 𝜂-equality is not preserved under defunctionalization and refunctionalization. Let us again consider a simple example. In the following proof, we show that a function 𝑓 is equal to its 𝜂-expanded form 𝜆𝑥.𝑓 .ap(𝑥). In order to typecheck, the proof would need to use a judgmental 𝜂-equality for functions.
codata Fun { ap(x: Nat): Nat } let prop_eta(f: Fun): Eq(Fun, f, (\x. f.ap(x))) ⅟= Refl(Fun, f);
\ However, defunctionalization of this proof would result in the following program, where we have used an ellipsis to mark all the constructors that were generated for the other lambda abstractions in the program.
data Fun { Eta(f: Fun), … } def Fun.ap(x: Nat): Nat { Eta(f) => f.ap(x),… } let prop_eta(f: Fun): Eq(Fun, f, Eta(f)) ⅟= Refl(Fun, f);
Using prop_eta it would now be possible to show that any constructor f of Fun is equal to Eta(f). This would contradict the provable proposition that distinct constructors are not equal.
\
Solution. We do not support 𝜂-equality in our formalization and implementation. This means that we only normalize 𝛽-redexes but not 𝜂-redexes during typechecking. However, it would be possible to support judgmental 𝜂-equality on a case-by-case basis similar to the eta-equality and no-eta-equality keywords in Agda which enable or disable eta-equality for a specific record type6 . De- and refunctionalization is then only available for types without 𝜂-equality.
:::info Authors:
:::
:::info This paper is available on arxiv under CC 4.0 license.
:::
\
