On the Difference Between a Type System and the Illusion of One - Divisions by zero
On the Difference Between a Type System and the Illusion of One In the manner of
those who have suffered enough to have opinions The article being addressed here
is a charming introduction to TypeScript
[https://sitr.us/2026/04/06/big-ideas-of-typescript.html/]. The author is
clearly intelligent, writes well, and has taken genuine care to explain what
TypeScript offers. We should be grateful for their effort. We should also be
honest about what they have described: not a type system, but a type-shaped
sticker applied to the outside of a runtime that will cheerfully betray you the
moment your back is turned. Let us be precise about what we mean. And then let
us be precise about PureScript. I. “Types are erased.” Yes. That’s the problem.
The article states this plainly, as if it were a feature: “During compilation
types are erased so you can’t do anything with them at runtime.” There it is.
The foundational confession. In a language with a genuine type system – Haskell,
Agda, Idris, PureScript – erasure is a property we prove holds for certain type
information that is no longer needed because the compiler has discharged the
proof obligation at compile time. The program is correct by construction. The
types are erased because they have done their work. In TypeScript, erasure is a
design constraint imposed by the host runtime. The types are erased because
JavaScript doesn’t know they exist, and JavaScript doesn’t care, and at 2am when
your production system is on fire, neither will you. The “conversation with the
compiler” described so warmly ends the moment you ship. After that, you are on
your own, talking to a runtime that never heard a word of it. In PureScript, the
compiler does not merely check your types. It uses them to generate correct
code. Typeclass instances are resolved at compile time, not by runtime
dictionary lookup accidents. Row types are checked to exhaustion. The compiled
JavaScript output is semantically faithful to the typed source in ways that
TypeScript, constrained to preserve JavaScript’s semantics, simply cannot
guarantee. II. Structural Typing: A Feature That Eats Itself Consider what the
article is actually telling you when it celebrates structural typing with
“Classes are suggestions”: class Rectangle { constructor(public width: number,
public height: number) {} area() { return this.width * this.height } } const
myRect: Rectangle = { width: 6, height: 2, area: function() { return this.width
* this.height }, } myRect instanceof Rectangle is now undefined behavior – or
rather, defined to be false, which will surprise exactly the people who most
need not to be surprised. The article notes: “This might be true or false! We
don’t have enough information to know at this point.” This is not expressive
power. This is type unsafety with good PR. You have told your compiler a fact –
rect: Rectangle – that the compiler knows is not necessarily true, and then
shrugged. PureScript’s nominal newtype system, combined with smart constructors,
makes this class of error inexpressible. You cannot construct a value of type
Newtype a except through the provided constructor. The type and its inhabitants
are in correspondence. That is what types are for. The excess property checking
“gotcha” – where updateRecord( id: 1, name: “Jesse” }) is rejected but the
intermediate-variable version is accepted – is not a “useful feature once you
understand it.” It is a special-case heuristic bolted on top of an unsound
system to catch a narrow class of common errors while leaving the underlying
unsoundness intact. You are patching bullet holes while the hull is open to the
sea. III. Untagged Unions: Nominality in Disguise, Done Worse The article is
quite pleased with untagged unions: ``` type Tree<T> = Node<T> Leaf<T> | Empty
type Node<T> = { tag: “node”, leftSubtree: Tree<T>, rightSubtree: Tree<T>,
value: T type Leaf<T> = tag: “leaf”, value: T } type Empty = { tag: “empty” }
``` Do you see it? This is a reinvention of nominal tagged unions – Haskell’s
data, PureScript’s data – accomplished by manually threading string literal
discriminants through record fields, relying on the type checker to notice that
“node” “leaf” | “empty” is exhausted by the switch. This is ADTs with training
wheels, where you the programmer must maintain the invariant that no one
constructs { tag: “node”, leftSubtree: undefined and hands it to your function
wearing a Node<T> mask. In PureScript: data Tree a = Node (Tree a) (Tree a) a |
Leaf a | Empty depth :: forall a. Tree a -> Int depth (Node l r _) = 1 + max
(depth l) (depth r) depth (Leaf _) = 1 depth Empty = 0 The compiler knows these
are the only inhabitants of Tree a. Not because you wrote tag: “node”. Because
the constructor is the proof. Pattern matching is exhaustiveness-checked against
the actual type definition, not against a set of string literals you manually
synchronized with a union type. Add a new constructor, get a compile error
everywhere you forgot to handle it. In PureScript, the absence of a case is a
type error. In TypeScript, it is a type error only if you remembered not to
write default. The safety is opt-in and manual. That is not a type system. That
is documentation that compiles. IV. Type Classes: The Feature TypeScript Cannot
Have The article is commendably honest in its conclusion: “If there is one
feature I miss from other languages it is ad-hoc polymorphism which you see in
Rust as traits, and in Haskell as type classes. But that is a feature that is
only possible with a compiler that uses type information to write a compiled
program. That’s contrary to TypeScript’s nature.” Yes. Exactly. And this is not
a minor omission. Type classes are how you write code that is provably correct
across an entire family of types, where the compiler resolves the correct
implementation at compile time based on types that are known at compile time.
This is how you implement Functor, Applicative, Monad, Foldable, Traversable –
the entire algebraic backbone of principled functional programming. TypeScript
gives you structural subtyping instead, which means you can write functions that
accept “anything with a .map method.” But you cannot say: this type is a lawful
Functor, and here is the proof that fmap id = id holds for it, and I am calling
code that requires a lawful Functor. TypeScript has no mechanism for expressing
or checking laws. You write interface Functor<F> map: … } and you hope. Hope is
not a type. PureScript’s type class system lets you write: class Functor f where
map :: forall a b. (a -> b) -> f a -> f b instance Functor Maybe where map f
(Just a) = Just (f a) map _ Nothing = Nothing When you write map show, the
compiler selects the unique correct instance for the type at hand, verified to
satisfy the structural interface, resolved without any runtime dictionary
gymnastics visible to the programmer. This is not available in TypeScript. It
cannot be made available in TypeScript. The article says so themselves. V.
Conditional Types: Turing-Complete Regret The article presents conditional types
as TypeScript’s crown jewel: type Flatten<T> = T extends any[] ? T[number] : T
Type-level computation! How exciting. Except: TypeScript’s type-level language
is not a well-behaved lambda calculus. It is a Turing-complete term rewriting
system whose evaluation is not guaranteed to terminate, whose error messages
when it does not terminate are incomprehensible, and whose interaction with
union distribution, inference sites, and higher-kinded patterns produces
behaviors that the TypeScript team themselves describe as “by design” when users
file bugs. The article cheerfully suggests you experiment with recursive
type-level programs in the Playground. This is the type theory equivalent of
saying “you can do surgery with a butter knife if you’re careful.” You can. It
does not follow that the tool is fit for purpose. PureScript has a kind system.
Types have kinds. Maybe :: Type -> Type. Either :: Type -> Type -> Type. Type
classes can be parameterized by type constructors of specific kinds. This is not
advanced wizardry – it is the basic discipline that allows you to write class
Functor (f :: Type -> Type) and mean it. TypeScript does not have first-class
type constructors (the article acknowledges this in a footnote). You cannot
abstract over Array as a type constructor and pass it to a function that works
for any Functor. You can only write out the concrete specializations. Every
time. By hand. While pretending this is composability. VI. Dependent Types: What
PureScript Reaches For, What Haskell Struggles With, and What TypeScript Cannot
Imagine Here we must be precise, because the claim matters. Haskell has been
attempting to admit dependent types for two decades. The machinery accumulated
in this effort – DataKinds, TypeFamilies, GADTs, RankNTypes, TypeInType,
singletons – is remarkable engineering. It is also a horror to use. The
singletons library, which generates singleton types to lift values to the type
level, requires Template Haskell and generates code that would cause a
reasonable person to reconsider their career. There is extensive literature on
the difficulty of grafting dependent types onto a language whose surface syntax
and elaboration strategy were not designed for them. PureScript, designed a
generation later by Phil Freeman with full knowledge of what Haskell had
learned, made different choices. PureScript has row polymorphism – a form of
type-level record manipulation that allows you to reason about which fields a
record has, statically, without the full weight of dependent types but with much
of their practical benefit: ``` – A function that requires a record with at
least a name field greet :: forall r. { name :: String r -> String greet rec =
"Hello, " <> rec.name [http://rec.name] ``` This is not merely structural
typing. The row variable r is universally quantified, and the constraint name ::
String r is not erased. It is used by the compiler to verify that every call
site provides the required field, while permitting the record to have any
additional fields the caller provides. TypeScript approximates this with
generics and extends, but awkwardly, without the theoretical foundation that
makes the approximation reliable. Can you write a vector type indexed by its
length in PureScript, where append has type Vect m a -> Vect n a -> Vect (m + n)
a and this is checked statically? With Nat-kinded types and appropriate
constraint machinery, yes, and the resulting code is readable. In TypeScript?
You can approximate it with numeric literal types and conditional types and it
will work for small concrete sizes and fall apart into never inference
nightmares the moment you abstract over the lengths. In Haskell, you can do it
properly, but you will need the singletons library, fourteen language
extensions, and a stiff drink. PureScript occupies a sweet spot: principled
enough to express the patterns correctly, without the geological strata of
backward compatibility that makes Haskell’s dependent types so difficult to
reach. VII. The Decisive Complaint The article concludes: “TypeScript is
JavaScript, with the types written in the source file instead of in your head.”
This is exactly right, and it is exactly the problem. TypeScript’s aspiration is
to describe JavaScript programs. PureScript’s aspiration is to replace the need
for a certain class of JavaScript programs entirely, by being a language in
which correctness is expressible, checkable, and mandatory. TypeScript will tell
you, if you’re lucky and you’ve set up your generics just right, that you passed
the wrong kind of object to a function. PureScript will tell you that your
effect types don’t line up, that you forgot to handle the Nothing case, and – if
you reach for the right libraries – that your state machine transition is
illegal in the current state. TypeScript’s types disappear at runtime.
PureScript’s types have already done their work by then, so they don’t need to
stay. The difference is not expressiveness. Both languages have impressive
type-level machinery. The difference is soundness, principled design, and what
the type system is willing to promise you. TypeScript promises: “We’ll catch the
obvious stuff.” PureScript promises: “If it compiles, here is what we can
guarantee about its behavior.” Only one of those is a type system. The other is
a very sophisticated linter. We should be grateful for linters. We should not
confuse them for proofs.
Boyd Stephen Smith Jr.
Functional Programming India
paintgoblin
ultimate_worrier
harryprayiv