Type Systems — Cross-Language Comparison

Type Systems — Cross-Language Comparison

• Type: cross-cutting comparison
• Languages covered: 51 (see _index)
• Last updated: 2026-05-07

TL;DR

• The “static vs dynamic” dichotomy is dead — the real spectrum is dynamic → gradual → static-nominal → static-structural → static-with-classes/traits → dependent, with several orthogonal axes (variance, inference power, totality, linearity).
• Hindley-Milner (and its descendants ML, Haskell, OCaml, Roc, Gleam) gives you full inference + parametric polymorphism. Most modern type systems are HM with extensions bolted on.
• Type classes / traits (Haskell, Rust, Scala, Swift) are the modern way to do ad-hoc polymorphism without subtype inheritance — they replace OO method dispatch with constraint-based dispatch.
• Dependent types (Idris, Agda, Lean, Coq/Rocq) blur the boundary between types and values; types can compute, theorems can be proved. Cost: harder to write, slower to typecheck, fewer engineers.
• Gradual typing (TypeScript, Hack, Dart strict) lets you migrate from dynamic to static incrementally — you pay nothing to start, and you opt into safety where you want it.
• Set-theoretic types (Elixir, TS unions/intersections) treat types as sets and use set operations (∪, ∩, complement) as first-class type constructors.

The spectrum

DYNAMIC ──────────── GRADUAL ─────── STATIC NOMINAL ─── STATIC STRUCTURAL ── HIGHER-KINDED ── DEPENDENT
  |                      |                |                    |                  |              |
Bash/Tcl              TypeScript       Java/C#              Go (interfaces)     Haskell        Idris/Agda
Smalltalk             Python+mypy      Kotlin/Swift         OCaml records       Rust traits    Lean/Coq
Common Lisp           Ruby+RBS         C++ classes          Scala               Scala
Erlang/Elixir         Hack             Dart strict          F#                  Swift protocols
Perl/Lua/PHP          Elixir set-th    Crystal              TS structural       OCaml functors
Tcl/R                 Clojure spec     Pony                                     Common Lisp MOP
Prolog                                 Nim/Zig
                                       Odin/V/Roc/Gleam

Categories

1. Untyped (or “everything is a string”)

The interpreter does not distinguish types in the language; values carry tags but the language doesn’t have a checker.

• Bash — strings only; type discipline is by convention.
• Tcl — “everything is a string” historically; internal representations are typed but the language is untyped.

2. Dynamically typed — strict

Types are checked at runtime; mismatches throw immediately.

• Python — strong + dynamic. Optional typing module + mypy/pyright/pyrefly. PEP 695 (3.12) added explicit type-parameter syntax; PEP 749 deferred annotations (3.14).
• Ruby — strong + dynamic. RBS + Sorbet for gradual typing.
• Perl — values have a “context” (scalar/list/boolean) more than a type.
• R — dynamic; vectors are core, scalars are length-1 vectors.
• Julia — dynamic dispatch with an expressive type system — methods specialize by argument types via multiple dispatch; type annotations are optional and used for dispatch, not safety.
• Lua — 8 fundamental types; tables are everything.
• Smalltalk — dynamic; everything is an object; typing is conventional.
• Prolog — terms are dynamically typed; mode declarations (Mercury) add static checking.

3. Dynamically typed — weak

Implicit conversions everywhere. Famous for surprise.

• JavaScript — == coercion infamy. Use ===. ES2020+ has nullish coalescing, optional chaining.
• PHP — modern PHP (8.x) is dramatically less weak; type declarations + strict_types help.

4. Optional typing — gradual, retrofitted

Started dynamic; added an optional static layer. The static checker is non-mandatory.

• Python + mypy/pyright — annotations are runtime-introspectable but not enforced by CPython. Strict mode possible.
• Ruby + RBS/Sorbet — RBS files are sidecar; Sorbet inlines T.let/T.cast.
• PHP — type declarations on params/returns/properties + declare(strict_types=1).
• Clojure — clojure.spec for runtime contracts; core.typed (defunct) for static.
• Common Lisp — declare + the give the compiler hints; SBCL emits warnings on mismatch.
• Lua — Luau (Roblox) adds a static type checker on top.
• Elixir — set-theoretic types in 1.18+ (gradual + structural; novel design by José Valim and Giuseppe Castagna).

5. Gradual typing — first-class

The language was designed gradual from the start; types are a primary feature.

• TypeScript — gradual layered on JavaScript. Conditional/mapped/template-literal types. As of TS 6+ and the TS 7 Beta (“Corsa”, Go-based compiler) of 2026-04-21, performance is dramatically improved.
• Dart — sound gradual: dart-strict checks fully; dynamic is opt-in.
• Hack — Facebook’s PHP gradual fork (mention only; not in our 51).

6. Static — nominal, mostly inferred locally

Types are declared at boundaries; locals get inferred. Class identity matters (subtyping is by name, not shape).

• Java — nominal classes + interfaces. Generics with use-site variance (? extends, ? super). Records + sealed (Java 17+); pattern matching maturing.
• [[Languages/csharp|C#]] — nominal; covariant/contravariant generic parameters declared at definition. Records, init-only setters, primary constructors (C# 12+).
• Kotlin — nominal; declaration-site variance (out, in); reified generics in inline functions.
• Swift — nominal classes/structs; protocols (structural-ish — see category 8).
• Go — nominal types but interface satisfaction is structural (no implements). Generics added in 1.18 (2022); type inference is intentionally limited.
• Dart strict — nominal, sound subtyping.
• Crystal — nominal + strong inference; union types pervasive.
• Pony — nominal + structural interfaces; types carry reference capabilities.
• C++ — nominal classes + concepts (C++20) for constraint-based generic dispatch.
• Zig — nominal structs/unions/enums; comptime blurs the line at compile time.
• Odin — nominal; where clauses constrain procedures.
• V — nominal + interfaces.
• Nim — nominal + concepts (structural constraints) + generics.
• Ada — strongly nominal; subtypes have ranges/discriminants; protected types.
• Pascal (Object Pascal) — nominal; interfaces are nominally typed but structurally compatible.
• C — nominal but extremely weak; pointers can alias; void * escapes.

7. Static — Hindley-Milner / let-polymorphism

Full type inference; you almost never write a type. Polymorphism via parametric (generics) is the norm.

• OCaml — the canonical HM. Module functors. GADTs since 4.x. First-class modules.
• [[Languages/fsharp|F#]] — HM + .NET interop. Computation expressions, units of measure, SRTP.
• Haskell — HM extended with type classes, kind polymorphism, type families, GADTs.
• Roc — HM + abilities (typeclass-equivalent) + opaque types.
• Gleam — HM + targets BEAM and JS. No higher-kinded types — intentional.
• Elm — (mention; not in 51) HM with no typeclasses (intentional minimalism).

8. Static — type classes / traits / protocols

Ad-hoc polymorphism via constraints. Methods dispatched not on inheritance but on satisfaction of a constraint.

• Haskell — type classes (the original). Higher-kinded; constraint kinds.
• Rust — traits + associated types. Coherence enforced (orphan rules). No HKTs (workarounds via GAT).
• Scala — Scala 3’s given/using is the modern face; was implicits in Scala 2. Type classes via implicit/given.
• Swift — protocols + protocol extensions; primary associated types since Swift 5.7. Existential types (any P) and opaque types (some P).
• Idris — interfaces (typeclass-equivalent).
• Agda — instance arguments (typeclass-equivalent).
• Lean — typeclasses with rich resolution.

9. Static — structural typing

Type identity is shape-based; if two types have the same fields/methods, they’re compatible.

• TypeScript — purely structural (objects + functions match by shape).
• Go — interfaces are structural; no explicit implements.
• OCaml — object types are structural; module signatures are mostly nominal.
• Scala — refinement types ({type T = X}) and structural types (slow at runtime due to reflection).
• Pony — interfaces are structural; traits are nominal.

10. Static — variance polymorphism

Generic parameters can be marked covariant/contravariant.

• Declaration-site variance: [[Languages/csharp|C#]] (out T, in T), Kotlin (out T, in T), Scala (+T, -T).
• Use-site variance: Java (? extends, ? super).
• Invariant by default: Rust, Go, TypeScript (with bivariance escape hatches).

11. Static — refinement / liquid types

Subtypes constrained by predicates: {x: Int | x > 0}. Decidable subset of dependent types.

• Haskell (Liquid Haskell, plugin) — extends GHC with refinement types.
• Ada / SPARK — subtype predicates + GNATprove for static verification.
• Scala (community: refined library) — refinement DSL.

12. Static — linear / affine / quantitative

Track usage-count: 0 (erased), 1 (use exactly once), ω (unrestricted).

• Idris (2) — Quantitative Type Theory. The flagship example.
• Rust — affine (use-at-most-once) via the borrow checker. Closely related but no first-class linearity in types.
• Haskell — -XLinearTypes since GHC 9.0.
• Agda — 0/1/ω quantities (Agda 2.6+).
• Pony — reference capabilities are a uniqueness/sharing discipline; not “linear” but related.
• Clean — uniqueness types (mention; not in 51).

13. Static — dependent types

Types can depend on values. The type Vec n (vector of length n) lets the compiler verify that head : (n > 0) → Vec n → A won’t run on empty vectors.

• Idris (2) — full dependent types + QTT. Type-driven development workflow.
• Agda — full dependent types. Cubical Agda for HoTT.
• Lean (4) — dependent types + tactic-based proofs. mathlib4 is the largest formalized math library in any system.
• Coq (Rocq) — dependent types via Calculus of Inductive Constructions; Ltac/Ltac2 for tactics. Used in CompCert, Four-Color theorem, Feit–Thompson.

14. Static — set-theoretic types

Types are sets; type operations (∪, ∩, complement) are first-class.

• Elixir — set-theoretic gradual types (1.18+, Castagna et al.).
• TypeScript — union/intersection types are similar in spirit (less rigorous theory).
• CDuce — academic (not in 51).

15. SQL’s type system (its own thing)

Three-valued logic (true / false / unknown=NULL); each engine has its own type set.

• SQL — the standard defines core scalar types (integer, varchar, date, etc.); each dialect extends. JSON is a 2023 addition. Type coercion rules are dialect-specific (Oracle empty-string-is-NULL is the famous trap).

Per-language quick reference

Language	Family	Inference	Polymorphism	Notable
Python	Dynamic + gradual	n/a (annotations)	structural via duck typing	mypy/pyright; PEP 695 syntax
JavaScript	Dynamic, weak	n/a	n/a	ES2025; coercion footguns
TypeScript	Gradual structural	strong	parametric + structural	TS 7 Beta (Corsa, Go-based)
Java	Static nominal	local (var)	parametric + use-site variance	Records, sealed, pattern matching
C	Static (weak)	none	macros only	void *, undefined behavior
C++	Static nominal	strong	templates + concepts (C++20)	SFINAE → concepts
[[Languages/csharp|C#]]	Static nominal	local (var)	parametric + decl-site variance	Source generators, records
Go	Static nominal+structural	weak	parametric (1.18+)	structural interfaces
Rust	Static nominal + traits	strong	parametric + traits	Affine types; lifetimes; coherence
Swift	Static nominal + protocols	strong	parametric + protocols	Existentials + opaque types
Kotlin	Static nominal	strong	parametric + decl-site variance	Reified generics; null safety
Ruby	Dynamic + gradual	n/a	duck typing	RBS + Sorbet
PHP	Dynamic + gradual	n/a	structural duck typing	strict_types declare
Scala	Static nominal + structural + traits	strong	parametric + given/using	Scala 3 match types, opaque types
Dart	Static gradual sound	strong	parametric	Null safety, mixins
Elixir	Set-theoretic gradual	weak	pattern matching	Castagna et al. type system 1.18+
Haskell	Static HM + classes	full	parametric + classes + HKTs	GADTs, type families, -XLinearTypes
Clojure	Dynamic + gradual via spec	n/a	protocols + multimethods	core.async; spec
[[Languages/fsharp|F#]]	Static HM	full	parametric + classes	SRTP; units of measure
Lua	Dynamic	n/a	duck typing	Luau static layer
R	Dynamic	n/a	S4/R6 method dispatch	NSE + tidy eval
Julia	Dynamic + multiple dispatch	optional	multiple dispatch	type system used for dispatch, not safety
Zig	Static nominal	strong	comptime polymorphism	comptime is the meta-system
Nim	Static nominal + concepts	strong	parametric + concepts	macros + templates
Crystal	Static nominal	strong	union types pervasive	union types are inferred
OCaml	Static HM	full	parametric + functors + classes	First-class modules; GADTs
Perl	Dynamic	n/a	duck typing	Modern: native class (5.38+)
Erlang	Dynamic	n/a	pattern matching	Dialyzer success-typing
Racket	Dynamic; Typed Racket sibling	n/a	dispatch via prefab structs	Typed Racket has full HM
Common Lisp	Dynamic + declarative	n/a	CLOS + multimethods	declare/the for hints
Scheme	Dynamic	n/a	dispatch on tags	R6RS optional types
Fortran	Static nominal	none	parameterized derived types (PDT)	Strong typing for arrays
COBOL	Static nominal	none	n/a	PICTURE clauses
Ada	Static nominal + SPARK refinements	local	generics + variance	Subtype predicates
Pascal	Static nominal	none/limited	generics	Strong typing tradition
Prolog	Dynamic	n/a	dispatch on terms	Mercury adds static + modes
Tcl	Untyped (string-typed)	n/a	n/a	Internal types invisible
Groovy	Dynamic + @CompileStatic	strong (when static)	duck or static	dynamic by default
Bash	Untyped	n/a	n/a	strings only
PowerShell	Dynamic + .NET types	strong (typed mode)	.NET-flavored	Type-constrained params
SQL	Static + 3VL	n/a	n/a	NULL = unknown; dialect-specific
V	Static nominal	strong	interfaces + generics	Sum types
Odin	Static nominal	weak	parametric + where constraints	No subtype-OO
Roc	Static HM + abilities	full	parametric + abilities + opaque	Tags (open/closed)
Gleam	Static HM	full	parametric only	No HKTs (intentional)
Pony	Static nominal + structural + refcaps	strong	parametric + traits + interfaces	6 reference capabilities
Idris	Dependent + linear (QTT)	strong	parametric + interfaces	Type-driven development
Lean	Dependent	strong	parametric + typeclasses	Hygienic macros + elaboration
Coq (Rocq)	Dependent (CIC)	strong	parametric + typeclasses	Prop / Set / Type universes
Agda	Dependent + quantitative	strong	parametric + instance args	Cubical Agda; reflection
Smalltalk	Dynamic	n/a	dispatch on receiver	doesNotUnderstand:

Decision rubric

Pick dynamic when iteration speed beats compile-time safety: scripts, glue code, scientific exploration, REPL-driven prototyping. Python, Ruby, Common Lisp, R.

Pick gradual when you have a large dynamic codebase you want to migrate, OR when you want safety where it matters but not everywhere. TypeScript, Sorbet, Python+mypy.

Pick static nominal when you have many engineers, long-lived code, OO domain models. Java, C#, Kotlin, Swift.

Pick HM-style ML when expressivity per syntax matters and you don’t need OO inheritance. OCaml, F#, Haskell, Roc, Gleam.

Pick traits/typeclasses when you want zero-cost abstraction with constraint-based polymorphism. Rust, Haskell, Swift protocols, Scala 3 given/using.

Pick dependent types when correctness must be proved, not tested. Lean, Coq/Rocq, Idris, Agda. Realistic adoption: protocol verification, compilers, security-critical kernels, math formalization. Not realistic: web apps.

Pick refcaps / linearity when data-race freedom or resource correctness must be statically guaranteed. Pony for actor-model concurrency. Idris/Linear Haskell for resource-typed APIs (filehandles that can’t be double-closed).

Edge cases & nuances

• TypeScript’s structural typing is the famous source of “looks-the-same-but-isn’t” bugs — branded/nominal types via phantom fields are the workaround.
• Java’s generic erasure vs C#/.NET’s reified generics — same surface syntax, dramatically different runtime model. C# can typeof(T) at runtime; Java can’t.
• Go’s generics (since 1.18) are deliberately conservative; no HKTs, no variance, weak inference. The design rejects most of the FP type-theoretic tradition.
• Scala 3 is the Swiss Army of static types — you can write Java-flavored, ML-flavored, dependently-typed-lite, or set-theoretic code. The cost is a learning cliff.
• Rust’s lifetimes are not types in the value sense — they’re erased at compile time. They’re closer to a separate proof system that runs alongside type checking.
• Julia’s multiple dispatch is dynamic but the type system is rich (parametric + abstract + concrete + invariant generics) — used for dispatch and the JIT specialization, not for safety.
• Elixir’s set-theoretic types (1.18+) is the most novel mainstream type system in years — sound gradual + structural + intersection/union/negation.
• Coq’s rename to Rocq (May 2025) doesn’t affect the type system; same Calculus of Inductive Constructions.
• HM inference is not decidable in the presence of higher-rank types — Haskell’s RankNTypes requires explicit annotations. OCaml’s first-class polymorphism does too.

Cross-references

For per-language detail on type system depth, see each note’s Intermediate and Advanced sections. The 51 individual notes are linked from _index.

Citations

• Pierce, Types and Programming Languages (TAPL) — the canonical textbook.
• Pierce et al., Software Foundations — interactive in Coq/Rocq.
• Castagna et al., “Set-Theoretic Types for Polymorphic Variants” — the Elixir 1.18 type system theory.
• Brady, Type-Driven Development with Idris — QTT and dependent types intro.
• TypeScript Handbook: https://www.typescriptlang.org/docs/handbook/2/
• Rust Reference (type system): https://doc.rust-lang.org/reference/types.html
• The 51 per-language notes in _index are the underlying source.