The JtV type system provides static type checking with automatic inference and coercion for the 7 number systems.
Any
│
┌──────────┴──────────┐
│ │
Number String
│
┌────┴────┐
│ │
Real Complex
│
┌─┴──────────┐
│ │
Integer Rational
│
├── Int
├── Hex
└── Binary
Float ──── approximates ───► Rational
x: Int = 42 // Arbitrary-precision integer
h: Hex = 0xFF // Hexadecimal (Int representation)
b: Binary = 0b1010 // Binary (Int representation)
f: Float = 3.14 // IEEE 754 double precision
r: Rational = 1/3 // Exact fraction
c: Complex = 3 + 4i // Complex number
s: String = "hello" // UTF-8 string
u: Unit = () // No value (void equivalent)
t: Bool = true
f: Bool = false
JtV infers types from context:
x = 42 // Inferred: Int
y = 3.14 // Inferred: Float
z = 1/2 // Inferred: Rational
w = 3 + 4i // Inferred: Complex
sum = x + y // Inferred: Float (Int + Float → Float)
Γ ⊢ n : Int (integer literal)
Γ ⊢ r/s : Rational (rational literal)
Γ ⊢ f.d : Float (float literal)
Γ ⊢ a + bi : Complex (complex literal)
Γ ⊢ x : τ (if Γ(x) = τ)
Γ ⊢ e₁ : τ₁ Γ ⊢ e₂ : τ₂ τ = coerce(τ₁, τ₂)
──────────────────────────────────────────────
Γ ⊢ e₁ + e₂ : τ
Automatic promotion follows the coercion hierarchy:
Int → Float
Int → Rational
Int → Complex
Float → Complex
Rational → Float
Rational → Complex
Hex → Int
Binary → Int
// Int + Float → Float
result = 5 + 3.14 // 8.14 : Float
// Int + Rational → Rational
result = 5 + 1/2 // 11/2 : Rational
// Anything + Complex → Complex
result = 5 + (3 + 4i) // 8+4i : Complex
coerce : Type × Type → Type
coerce(Int, Int) = Int
coerce(Int, Float) = Float
coerce(Float, Int) = Float
coerce(Int, Rational) = Rational
coerce(Rational, Int) = Rational
coerce(Float, Rational) = Float
coerce(Rational, Float) = Float
coerce(_, Complex) = Complex
coerce(Complex, _) = Complex
Explicit type annotations:
// Variable annotation
x: Int = 42
y: Float = 3.14
// Function signature
fn add(a: Int, b: Int): Int {
return a + b
}
// Generic functions (future)
fn identity<T>(x: T): T {
return x
}
point: (Int, Int) = (3, 4)
rgb: (Int, Int, Int) = (255, 128, 0)
numbers: [Int] = [1, 2, 3, 4, 5]
matrix: [[Float]] = [[1.0, 0.0], [0.0, 1.0]]
struct Point {
x: Int,
y: Int
}
p: Point = Point { x: 3, y: 4 }
Functions have purity levels that affect where they can be called:
Purity Hierarchy:
Total ⊂ Pure ⊂ Impure
@total → No loops, no I/O, guaranteed termination
@pure → May loop, no I/O
(none) → May loop, may do I/O
@total fn f(): T ⊢ f callable in Data context
@pure fn g(): T ⊢ g callable in Data context
fn h(): T ⊢ h callable only in Control context
@total fn increment(x: Int): Int {
return x + 1
}
@pure fn multiply(a: Int, b: Int): Int {
result = 0
for i in 0..b {
result = result + a
}
return result
}
fn readAndProcess(): Int {
input = read() // I/O
return parseInt(input)
}
// In Data context:
data_expr = increment(5) + multiply(3, 4) // OK
// ERROR: Cannot call impure function in Data context
// data_expr = readAndProcess() // Type error!
JtV uses bidirectional type checking:
- Inference mode: Compute type from expression
- Checking mode: Verify expression has expected type
infer : Context × Expr → Type
check : Context × Expr × Type → Bool
infer(Γ, n) = Int // Integer literal
infer(Γ, x) = Γ(x) // Variable lookup
infer(Γ, e₁ + e₂) = coerce(infer(Γ, e₁), infer(Γ, e₂))
check(Γ, e, τ) = (infer(Γ, e) = τ) ∨ coercible(infer(Γ, e), τ)
- Parse: Build untyped AST
- Resolve: Resolve names and imports
- Infer: Compute types bottom-up
- Check: Verify type constraints
- Purity: Check purity annotations
Error[E101]: type mismatch
--> main.jtv:5:10
|
5 | x: Int = 3.14
| ^^^^ expected Int, found Float
|
= help: use explicit conversion: floor(3.14)
Error[E201]: purity violation in @pure function
--> main.jtv:8:5
|
8 | print(x)
| ^^^^^^^^ I/O operation not allowed in @pure function
|
= note: @pure functions cannot perform I/O
= help: remove @pure annotation or remove print call
Error[E103]: cannot coerce types
--> main.jtv:12:10
|
12 | s: String = 42
| ^^ cannot coerce Int to String
|
= help: use toString(42) for explicit conversion
────────────────── (T-Int)
Γ ⊢ n : Int
────────────────── (T-Float)
Γ ⊢ f : Float
──────────────────── (T-Rational)
Γ ⊢ a/b : Rational
────────────────────── (T-Complex)
Γ ⊢ a + bi : Complex
Γ(x) = τ
────────────── (T-Var)
Γ ⊢ x : τ
Γ ⊢ e₁ : τ₁ Γ ⊢ e₂ : τ₂ τ = coerce(τ₁, τ₂)
─────────────────────────────────────────────────── (T-Add)
Γ ⊢ e₁ + e₂ : τ
Γ ⊢ f : (τ₁,...,τₙ) → τ Γ ⊢ eᵢ : τᵢ purity(f) ∈ {Total, Pure}
──────────────────────────────────────────────────────────────────── (T-Call-Data)
Γ ⊢ f(e₁,...,eₙ) : τ
Γ ⊢ e : τ τ' = coerce(Γ(x), τ)
──────────────────────────────────── (T-Assign)
Γ ⊢ x = e : Unit
Γ ⊢ b : Bool Γ ⊢ S₁ : Unit Γ ⊢ S₂ : Unit
──────────────────────────────────────────────── (T-If)
Γ ⊢ if b { S₁ } else { S₂ } : Unit
Γ ⊢ b : Bool Γ ⊢ S : Unit
─────────────────────────────── (T-While)
Γ ⊢ while b { S } : Unit