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. 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 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 { 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
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.