# Type Systems
## How Languages Work — The Codex Coding
**URL:** https://thecodex.expert/coding/how-languages-work/type-systems/
**Type:** concept
**Confidence:** high
**Last verified:** 2026-06-01
**Sources:** 5

---

## CANONICAL DEFINITION

A type system is a formal set of rules in a programming language that assigns a type to every expression and enforces constraints on how values of different types may be combined, with the purpose of preventing type errors — operations applied to values of incompatible types — either at compile time (static typing) or at runtime (dynamic typing).

---

## CONCEPT RELATIONSHIP MAP

**Requires first:** Binary and Number Systems · Compilation

**Enables:** Data Types · Variables · TypeScript · Rust · Python (type hints)

**Commonly confused with:** Static/dynamic mistaken for strong/weak (independent dimensions)

---

## CURIOUS LEVEL

### Static Typing

Types known at compile time. Compiler verifies all operations before producing executable. Java, C, C++, Rust, Go, Swift, TypeScript.

```java
int x = 5;
String name = "Alice";
int result = x + name;  // COMPILE ERROR — program never runs
```

### Dynamic Typing

Types attached to values at runtime. Variables can hold any type. Python, Ruby, JavaScript, PHP, Lua.

```python
x = 5
x = "Alice"   # fine
x + 10        # TypeError at RUNTIME
```

### Strong vs. Weak Typing (independent dimension)

Strong (Python): no implicit conversions — `"5" + 3` raises TypeError.
Weak (JavaScript): implicit coercions — `"5" + 3` = `"53"`, `"5" - 3` = `2`.

Matrix:
- Java: static + strong
- Rust: static + strong
- C: static + weak (implicit pointer/int coercions)
- Python: dynamic + strong
- JavaScript: dynamic + weak
- Go: static + strong (even int and int32 need explicit conversion)

### Type Inference

Compiler deduces types from context. You don't write them. Still statically typed — checked at compile time.

```rust
let x = 42;           // compiler infers i32
let name = "Alice";   // compiler infers &str
```

Rust, Go, Swift, Kotlin, Haskell all use inference. Dynamic typing ≠ type inference.

---

## EXPLORING LEVEL

### Structural vs. Nominal Typing

**Nominal**: compatible only if explicitly declared (Java `extends`, `implements`).
**Structural**: compatible if shape matches (TypeScript, Go interfaces).

```typescript
interface Printable { print(): void; }
class Document { print() { ... } }  // no "implements Printable"
function printIt(p: Printable) { p.print(); }
printIt(new Document());  // VALID — structural compatibility
```

### Gradual Typing

Mix of typed and untyped code. `any` type opts out. TypeScript: annotate incrementally. Python type hints (PEP 484): optional, checked by mypy/pyright, not enforced at runtime. Formalised by Siek & Taha (2006).

### Language Type System Summary

| Language | Static/Dynamic | Strong/Weak |
|---|---|---|
| C | Static | Weak |
| Java | Static | Strong |
| Rust | Static | Strong |
| Python | Dynamic | Strong |
| JavaScript | Dynamic | Weak |
| TypeScript | Static (gradual) | Strong |
| Go | Static | Strong |
| PHP | Dynamic | Weak |
| Haskell | Static | Strong (HM inference) |

### COMMONLY CONFUSED

- Static/dynamic ≠ strong/weak. Python is dynamic + strong. C is static + weak.
- Type inference ≠ dynamic typing. Rust infers types but is fully static.
- Weakly typed ≠ untyped. JavaScript has types; it just coerces them implicitly.

---

## DEEP DIVE LEVEL

### Formal Foundations

Simply typed lambda calculus (Church, 1940): assigns base types to terms, prevents type mismatch. Foundation of type safety.

Type safety: two properties:
- Progress: a well-typed program is a value or can take a step (not stuck)
- Preservation: if a well-typed program takes a step, result is also well-typed

Java is unsound in practice (raw types, unchecked casts, covariant arrays → ClassCastException at runtime). TypeScript intentionally unsound (`any`, type assertions). Rust (safe subset) is sound.

### Hindley-Milner Type Inference

Hindley (1969), Milner (1978): complete type inference for polymorphic type systems. Algorithm W infers the principal (most general) type of every expression without annotations. Nearly linear in practice. Basis of Haskell, ML, OCaml, F#, Rust type inference.

### Gradual Typing Formal Specification

Siek & Taha (2006): dynamic type `?` is consistent with any type. Consistency (≈) relation allows `? ≈ T` for any T. Casts between static and dynamic code inserted automatically. Type errors from untyped code detected at boundary.

### Primary Sources

- Pierce, B. C. (2002). Types and Programming Languages. MIT Press.
- Siek, J. G. & Taha, W. (2006). Gradual Typing for Functional Languages. Scheme FP Workshop.
- Milner, R. (1978). A theory of type polymorphism in programming. JCSS 17(3), 348–375.
- Rossberg, A. et al. (2010). F-ing modules. TLDI '10. ACM.
- ECMAScript 2024 Language Specification (ECMA-262). Ecma International.

---

*The Codex Coding — thecodex.expert/coding/ — Free forever — Mumbai, India*
*Last verified: June 2026 · Source confidence: high*