path: root/docs/type-hierarchy.puml

@startuml type-hierarchy
!theme plain
title Type System: Stratified Universes & Types as Relations

package "Universe Stratification" {
  class "Universe₀" as U0 {
    Base values
    Examples: 3, -5, 3.14, true, "hello"
    The set of all runtime values
  }

  class "Universe₁" as U1 {
    Type relations (classify values)
    Examples: natural, integer, real, boolean
    Each type is a relation over Universe₀
    Type relations are infinite relations
  }

  class "Universe₂" as U2 {
    Type of type relations
    The classifier of type relations
    Prevents self-reference paradoxes
  }

  class "Universe₃" as U3 {
    Meta-type level
    Type : Universe₂ : Universe₃
  }

  U0 : Universe₁
  U1 : Universe₂
  U2 : Universe₃
  U3 : Universe₄

  note right of U1
    **Stratification prevents Russell's Paradox**
    Type relations live in Universe₁
    and classify values in Universe₀.
    A type cannot contain itself.

    natural : Universe₁
    3 ∈ natural (3 ∈ Universe₀)
    But: natural ∉ natural ✗ (universe mismatch)
  end note
}

package "Supertypes (Universe₁)" {
  class Number {
    Membership: number[X] where X : Universe₀
    Definition: Union of all numeric types
    number[X] :- natural[X]; integer[X];
                 rational[X]; real[X].
    Allows polymorphism over numeric types
    Universe level: Universe₁
  }

  class Scalar {
    Membership: scalar[X] where X : Universe₀
    Definition: Atomic (non-composite) values
    scalar[X] :- number[X]; boolean[X]; string[X].
    Universe level: Universe₁
  }
}

package "Numeric Type Relations (Universe₁)" {
  class Naturals {
    Membership: natural[X] where X : Universe₀
    Criteria:
    - X is erlang:integer()
    - X >= 0
    Cardinality: aleph_zero
    Generator: 0, 1, 2, 3, ...
    Universe level: Universe₁
  }

  class Integers {
    Membership: integer[X] where X : Universe₀
    Criteria:
    - X is erlang:integer()
    Cardinality: aleph_zero
    Generator: 0, 1, -1, 2, -2, ...
    Universe level: Universe₁
  }

  class Rationals {
    Membership: rational[X] where X : Universe₀
    Criteria:
    - X is (P, Q)
    - integer[P], integer[Q]
    - Q ≠ 0
    Cardinality: aleph_zero
    Generator: Stern-Brocot tree
    Universe level: Universe₁
  }

  class Reals {
    Membership: real[X] where X : Universe₀
    Criteria:
    - X is erlang:float()
    Cardinality: continuum
    Generator: IEEE 754 floats
    Universe level: Universe₁
  }
}

package "Other Primitive Types (Universe₁)" {
  class Strings {
    Membership: string[X] where X : Universe₀
    Criteria:
    - X is erlang:string()
    Cardinality: aleph_zero
    Ordering: by length, then lexicographic
    Universe level: Universe₁
  }

  class Booleans {
    Membership: boolean[X] where X : Universe₀
    Criteria:
    - X is erlang:boolean()
    - X ∈ {true, false}
    Cardinality: 2
    Universe level: Universe₁
  }
}

package "Constrained Type Relations (Universe₁)" {
  class PositiveIntegers {
    Definition: positive_int[X] where X : Universe₀
    Criteria:
    - integer[X]
    - X > 0
    Relation: positive_int ⊆ integer
    Universe level: Universe₁
  }

  class BoundedInt {
    Definition: bounded_int[X, Min, Max]
    where X : Universe₀
    Criteria:
    - integer[X]
    - Min ≤ X ≤ Max
    Relation: bounded_int ⊆ integer
    Universe level: Universe₁
  }

  class NonEmptyStrings {
    Definition: non_empty_string[X]
    where X : Universe₀
    Criteria:
    - string[X]
    - length(X) > 0
    Relation: non_empty_string ⊆ string
    Universe level: Universe₁
  }
}

package "Composite Type Relations (Universe₁)" {
  class Complex {
    Definition (Karuta-style):
    complex[X] where X : Universe₀
    complex[X] :-
      X is (A, B),
      real[A], real[B].

    Interpretation:
    - (A, B) where A is real part
    - B is imaginary part
    Relation: complex ⊆ real × real
    Universe level: Universe₁
  }

  class Employee {
    Definition:
    employee[X] where X : Universe₀
    employee[X] :-
      X is (Name, Age, Salary),
      non_empty_string[Name],
      positive_int[Age],
      positive_int[Salary].

    Relation: employee ⊆ string × ℕ⁺ × ℕ⁺
    Universe level: Universe₁
  }
}

' Universe stratification relationships
U1 --> U0 : classifies values in
U2 --> U1 : types type relations
U3 --> U2 : meta-level

' All type relations live in Universe₁
U1 ..> Number : contains
U1 ..> Naturals : contains
U1 ..> Integers : contains
U1 ..> Rationals : contains
U1 ..> Reals : contains
U1 ..> Booleans : contains
U1 ..> Strings : contains
U1 ..> Scalar : contains

' Type relation hierarchy (within Universe₁)
Number <|-- Naturals : ⊇
Number <|-- Integers : ⊇
Number <|-- Rationals : ⊇
Number <|-- Reals : ⊇

Number <|-- Scalar : ⊇
Booleans <|-- Scalar : ⊇
Strings <|-- Scalar : ⊇

' Subset relations among numeric types
Naturals .up.|> Integers : ⊆
Integers .up.|> Rationals : ⊆
Rationals .up.|> Reals : ⊆

' Constrained types
Integers .down.|> PositiveIntegers : ⊇
Integers .down.|> BoundedInt : ⊇
Strings .down.|> NonEmptyStrings : ⊇

' Composite types (also in Universe₁)
Number .down.|> Complex : number × number
Complex : (view: pair of numbers)

Scalar .down.|> Employee : scalar × scalar × scalar
Employee : (view: string × nat × nat)

note right of Complex
  **Views as Type Relations:**
  Types can be defined as relational views
  over other type relations.

  Example using supertype:
  complex[C] :- C is (R, I),
                number[R], number[I].

  Or more specifically:
  complex[C] :- C is (R, I),
                real[R], real[I].

  Views can use supertypes for flexibility!
  All views live in Universe₁.
end note

note left of Number
  **Core Principle:** Every type is a relation
  Type checking = membership checking in relations
  T1 <: T2 iff T1 ⊆ T2 (subset relation)

  **Supertypes enable polymorphism:**
  A function can accept number[X] and work
  with naturals, integers, rationals, or reals.

  **Universe Levels:**
  All type relations: Universe₁
  All values: Universe₀
  Type of types: Universe₂

  **Erlang Type Mapping:**
  natural → integer() + (≥ 0)
  integer → integer()
  rational → {integer(), integer()}
  real → float()
  string → string()
  boolean → boolean()
end note

note bottom of U0
  **Avoiding Russell's Paradox:**

  Like F*, Domino uses predicative universe
  stratification. The key invariant:

  Type u#i : Type u#(i+1)

  In Domino:
  - Values (3, "hello", true) : Universe₀
  - Type relations (natural, string) : Universe₁
  - Type : Universe₂

  This prevents:
  natural ∈ natural (universe mismatch!)

  A type relation cannot be a member of itself.
  All type relations classify values in Universe₀
  but exist at Universe₁.
end note

@enduml