ocaml re-migration

1 files changed, 0 insertions, 289 deletions

diff --git a/docs/type-hierarchy.puml b/docs/type-hierarchy.puml
deleted file mode 100644
index c53a965..0000000
--- a/docs/type-hierarchy.puml
+++ /dev/null
@@ -1,289 +0,0 @@
-@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