Booking widget — one widget, three type systems
A hotel booking widget I wrote three times — in Vue 3 + TypeScript, in Effect-TS and in Elm — to measure how many correctness holes the TypeScript compiler leaves, what the Effect + TypeScript pairing adds, and how Elm handles it, where those holes are closed by the compiler itself.
Why
This is a small widget for booking a hotel room: picking dates in a calendar, choosing a room for the number of guests, availability on the chosen dates, computing nights and price, switching language (ru/en) and theme, the flow "select → review → confirm". There aren't many features — and that's deliberate: the goal isn't the number of screens but the quality of the code and architecture.
I built the base version in Vue 3 + TypeScript in strict mode. And then came the experiment the whole thing was set up for: I audited this version and found 13 correctness holes — places where a type allows an impossible state, a transition rests on a convention, or a rule lives in one spot of the UI and nowhere else. All thirteen compile under strict. After that I rewrote the same widget in two strongly-typed systems — Effect-TS (TEA + Effect) and Elm — and counted how many holes each closes structurally (a bad state is unrepresentable / a transition is a compile error), and how many only "in practice" (the rule is centralized in pure code but still written by hand).
The thesis I wanted to test: TypeScript doesn't guarantee a program's correctness after it compiles.
Code and live demo
- Vue 3 + TypeScript (base) — repository · live demo
- Effect-TS / foldkit (port) — repository · live demo
- Elm (port) — repository · live demo
A detailed "audit → architecture" breakdown of each of the 13 holes is in COMPARISON.md inside the port repositories.
The base widget: Vue 3 + TypeScript
The reference version is <script setup> + TypeScript in strict, on Vite. No UI libraries, no state managers, no date libraries: everything on native APIs and the Composition API.
Logic is separated from presentation. The domain (src/domain) — pure functions without a single Vue import: computing nights, choosing rooms for guests, validation, deterministic "availability" (no Math.random, so the tests are stable). The data layer is hidden behind a BookingApi port with adapters (a mock with network latency by default, an http one with DTO→domain mapping, a factory keyed on VITE_API_URL) — Dependency Inversion: to connect a real backend, one line changes, and in tests the adapter is swapped for a fake. The reactive layer is a useBooking composable via provide/inject with a typed InjectionKey: the state is small and bound to a single widget instance, so Pinia would be dead weight here. A UI kit along atomic design (UiButton, UiBadge, UiSurface, UiStepper, UiSegmented, UiStack, UiSplit): organisms like RoomCard and BookingSummary are assembled ~80% from these primitives, so one layer owns the styling of buttons and spacing.
Coverage: 47 Vitest tests (domain, adapters, store, UI kit, widget smoke) and 4 Playwright E2E (happy path in a real browser). It's on this version that I ran the 13-hole audit — it works correctly, but many invariants rest on discipline rather than on types.
The experiment: one architecture, three type systems
Both ports are built along The Elm Architecture — one immutable Model, one pure total update, effects as values. The domain, the availability data, the flow and i18n are the same. The only difference is in how the state is modeled and how transitions are expressed. The result against the 13-hole audit:
| Slice | Vue 3 + TS (base) | Effect-TS / foldkit | Elm |
|---|---|---|---|
| Holes closed structurally | — (reference, 13 open) | 9 of 13 | 12 of 13 |
| Closed "in practice" | — | 4 | 1 |
| Left open | 13 | 0 | 0 |
| Impossible states | Date | null × 2 fields are independent; the status flag is detached from validity |
sum types; Reviewing/Confirmed carry ValidBooking (smart constructor) |
the same + an opaque BookableDate: a past date can't be constructed |
| I/O boundary | as RoomDto[], as RoomId — checking is off |
Schema is the domain type: decoder and type can't diverge |
Json.Decode: bad input doesn't reach the domain |
| Dates | local getMonth/Date, risk of an off-by-one by TZ |
CalendarDate — a day without time or zone |
justinmimbs/date — a day without time or zone |
| Errors | confirm() does no effect, can't fail |
a typed channel catchTags → exhaustive messages |
the ADT SubmitError (409 → RoomTaken), a message per cause |
| Exhaustiveness | ternaries locale === 'ru' ? … silently swallow a 3rd locale |
Match.exhaustive — a new locale breaks compilation |
case over Locale — same |
| Tests | 47 Vitest + 4 Playwright | 32 (Story/Scene + property-based on fast-check) | 77 elm-test (unit / fuzz / update histories) |
Briefly, what the measurement showed. The representation and exhaustiveness holes (unrelated fields, a bare status flag, incomplete matches) both systems close cleanly — sum types and a total update make a bad state unrepresentable. Effect pulls ahead at the I/O boundary: Schema is the domain type, so the decoder and the type can't diverge (with hand-written decoders those are two separate declarations). Elm goes furthest on the audit (12 of 13) thanks to the opaque BookableDate, which makes "a past date" literally unconstructable — at the cost of wrap/unwrap ceremony at the boundaries. The single hole Elm left "in practice" is cancellation of stale requests: cancellation is a runtime effect, you can't forbid it with a type.
Decisions I made on this project
Audit the base first, then port
I didn't rewrite "by feel". First a formal audit of the Vue version against 13 concrete holes with severity and line references, and only then the ports, where each hole gets a verdict: closed structurally, in practice, or open.
Why: otherwise the comparison slides into "I just like Elm better". A checklist fixed in advance turns taste into measurement — for each of the 13 lines you can see what exactly changed and by which construct, rather than "overall it got more reliable".
An "impossible state" is checked by construction, not by a check
In the ports a valid booking exists only as a ValidBooking from a smart constructor, and it's carried by exactly those phase variants (Reviewing/Confirmed) where it's needed. "Confirmed without valid data" simply can't be assembled.
Why: in Vue the same guarantee rested on manual isValid checks in review()/confirm() and conditional rendering — that is, on the developer not forgetting. Moving the rule into the shape of the type removes a whole class of "forgot to check" without a single unit test for it.
The same data port in all three versions
Everywhere data goes through a port with mock and http adapters, switchable by a single environment variable. What changed was the decoding implementation at the boundary, not the contract "the domain doesn't know where the data comes from".
Why: the experiment should measure the type system, not a difference in data-access architecture. A shared port-adapter holds all the other variables constant — and incidentally shows that Dependency Inversion fits a Vue composable and TEA equally well.
What it shows
For me this isn't "Elm won" — each version has its price. Vue + TS gives the fastest and most familiar development, but half the invariants in it are conventions that strict doesn't highlight. Effect-TS brings structural reliability into the TypeScript ecosystem, and most of all right at the boundary with the outside world. Elm closes almost everything by construction, but demands ceremony and a separate runtime.
The main takeaway is methodological: "works and passes tests" and "an incorrect state is unrepresentable" are two different levels of guarantee. The same product, written three times, makes that difference visible and measurable rather than a matter of faith.