Volume 03: Type System

1. Introduction

This volume defines the type system of the Rethon programming language. It describes how types are identified, compared, constrained, inferred, converted, cast, composed, and used to organize values, references, protocols, generic abstractions, and nullable forms.

This document is part of the official Rethon Language Specification. It is normative rather than descriptive. Implementations, tooling, documentation systems, and other source-processing tools shall treat the rules in this volume as authoritative.

This volume does not define execution semantics, compilation strategy, ABI details, or backend-specific representation. It defines the language-level type system that later volumes and implementation strategies must respect.

Rethon is statically typed, value-oriented, protocol-oriented, and designed for native performance. The type system shall therefore prioritize compile-time safety, explicit contracts, readable source forms, and efficient specialization while remaining suitable for long-term language evolution.

2. Type System Goals

The Rethon type system shall support the following goals.

2.1 Compile-Time Safety

The type system shall detect type mismatches before execution whenever the information is available to the compiler.

2.2 Readability

Type expressions and type relationships shall be readable in ordinary source code. The type system shall not require cryptic notation for common programming tasks.

2.3 Value-Oriented Design

The type system shall support value semantics as the default mental model for ordinary data. Struct types shall therefore be first-class and efficient to use.

2.4 Protocol-Oriented Design

The type system shall support protocols as the canonical mechanism for describing shared behavior and for constraining generic code.

2.5 Native Performance

The type system shall support specialization, predictable type information, and efficient code generation opportunities without requiring the programmer to abandon high-level abstractions.

2.6 Explicit Nullability

The type system shall distinguish nullable and non-nullable forms explicitly. Absence shall not be implicit in ordinary type usage.

2.7 Long-Term Maintainability

The type system shall be clear enough to teach, stable enough to maintain, and structured enough to support a durable ecosystem.

2.8 Tooling Support

The type system shall support strong diagnostics, reliable refactoring, autocomplete, navigation, and other tooling tasks that depend on accurate compile-time type information.

2.9 Controlled Complexity

The type system shall remain expressive without becoming unnecessarily complicated. Each feature shall justify its existence in terms of language value.

3. Static Typing

Rethon shall be statically typed.

Type information shall be known and validated at compile time. A program shall not depend on runtime discovery of fundamental type information that could be determined statically.

Static typing is a foundational design choice. It is not merely a compiler convenience. It enables stronger diagnostics, safer refactoring, clearer APIs, and more predictable performance.

The language may use type inference to reduce repetition, but inference shall not reduce the language’s static guarantees. Inference is a convenience layer over static typing, not a replacement for it.

A source construct shall be type-correct only if the compiler can determine that its type usage satisfies the rules of this volume.

3.1 Type-Checked Before Execution

Every well-formed Rethon program shall be type-checked before execution or before emission of a type-correct compiled artifact.

3.2 No Dynamic Typing as the Core Model

The language shall not treat dynamic typing as the default programming model. Type information shall not be optional for ordinary code.

3.3 Predictable Type Visibility

The type of a value shall be accessible to the compiler at compile time even when the programmer does not write every type annotation explicitly.

4. Type Identity

Type identity determines when two type names refer to the same type.

Rethon shall use nominal type identity for user-defined types. A user-defined type shall be identified by its declaration, not merely by its shape.

4.1 Nominal Identity

Two user-defined types shall be the same type only if they refer to the same declared type after alias expansion and other purely lexical normalization allowed by this volume.

4.2 Built-In Type Identity

Built-in types shall have stable identity defined by the language specification.

4.3 Protocol Identity

A protocol shall have its own declared identity. A type that conforms to a protocol does not become that protocol type; it becomes a conforming type that satisfies the protocol’s requirements.

4.4 Type Aliases and Identity

A type alias shall not create a new type identity. It shall provide an alternate name for an existing type.

4.5 Structural Similarity Is Not Identity

Two types that happen to have similar fields, methods, or members shall not automatically be the same type. Similarity alone does not establish identity.

5. Type Equality

Type equality determines when two type expressions denote the same type.

5.1 Equality After Alias Expansion

Type expressions shall be considered equal if they denote the same underlying type after expanding type aliases.

5.2 Equality of Primitive Types

Primitive types shall compare equal only when they are the same primitive type.

5.3 Equality of Struct and Class Types

Two struct types or two class types shall be equal only when they refer to the same declared type.

5.4 Equality of Protocol Types

Protocol types shall compare equal only when they refer to the same declared protocol type or to the same well-defined protocol composition.

5.5 Equality of Generic Instantiations

Generic instantiations shall compare equal only when they have the same generic declaration and pairwise equal type arguments.

5.6 Equality of Nullable Types

Nullable types shall compare equal only when their underlying non-null types are equal and the nullability marker is the same.

5.7 Equality of Existential Types

Existential type equality shall be defined by the protocol composition or protocol name that defines the existential form.

6. Primitive Types

Rethon shall provide a small set of language-level primitive categories.

These types shall be treated as foundational type forms in the language specification.

6.1 int

int shall denote an integer type category.

The specification does not commit to a particular bit width in this volume.

int shall be suitable for integer arithmetic, indexing where allowed by later specification volumes, and general-purpose whole-number programming.

6.2 float

float shall denote a floating-point type category.

The specification does not commit to a particular bit width in this volume.

float shall be suitable for approximate numeric computation and real-valued arithmetic.

6.3 bool

bool shall denote the boolean type category.

bool shall represent the logical values used by conditional and comparison logic.

6.4 char

char shall denote a character type category.

char shall represent a single character value rather than a string of arbitrary length.

6.5 str

str shall denote a text type category.

str shall represent ordered textual data.

6.6 Additional Primitive Categories

Later specification volumes may define additional primitive categories if the language requires them, but such additions shall be made only with clear justification.

6.7 Primitive Type Examples

count: int = 42
ratio: float = 0.5
enabled: bool = True
initial: char = 'R'
name: str = "Rethon"

7. Value Types

A value type is a type whose values are treated as values rather than as identity-bearing references.

Value types shall be the default mental model for ordinary data in Rethon.

7.1 Value Semantics

A value type shall not imply shared object identity by default.

When a value type is assigned, passed, returned, or otherwise used in source-level expression positions, the language shall preserve value semantics. The observable meaning shall be that the value is treated as an independent value rather than as a shared identity-bearing object.

The specification does not require every operation on a value type to be physically copied in all circumstances. It requires the value semantics to remain observable and correct.

7.2 Copy Semantics

Value types shall support copy semantics in the language model.

Copying a value shall produce another value with the same value meaning. The resulting values shall be independent unless the language specification explicitly states otherwise for a particular type form.

7.3 Equality Considerations

Equality for value types shall reflect value meaning rather than identity.

A value type may define equality through later language mechanisms, but the type system shall distinguish value equality from object identity.

7.4 Examples

point: Point = Point(x: 1, y: 2)
copy_of_point: Point = point

The type system shall treat both point and copy_of_point as values of the same value type.

8. Reference Types

A reference type is a type whose values refer to identity-bearing objects.

Classes shall be the primary reference type in Rethon.

8.1 Reference Semantics

A reference type shall support reference semantics. Multiple references may refer to the same underlying object.

8.2 Identity

A reference type shall support identity as part of its conceptual model.

Identity distinguishes one object from another even when they contain the same member values.

8.3 Lifecycle Considerations

Reference types shall participate in language-level lifetime management as defined by the memory model direction established elsewhere in the specification.

The type system shall distinguish reference semantics from value semantics without requiring ordinary code to model low-level ownership mechanics explicitly.

8.4 Examples

session: Session = Session()
other_reference: Session = session

The type system shall treat both variables as references to the same class type.

9. Struct Types

Structs shall be value types.

A struct type shall be the primary type form for data-oriented, value-oriented programming in Rethon.

9.1 What Makes a Struct a Value Type

A struct shall be a value type because it is defined to support value semantics rather than identity-based reference semantics.

The crucial distinction is semantic, not merely representational. A struct exists to model data as a value.

9.2 Copy Semantics for Structs

Struct values shall support value-style copying semantics as described in Section 7.

9.3 Equality Considerations for Structs

A struct shall be conceptually suited to value-based equality. Two struct values with the same meaningful contents are expected to compare as equal when equality is defined for that struct type.

The type system itself does not define equality operators in this volume, but it shall preserve the distinction between value equality and identity.

9.4 Struct Type Examples

struct Point:
    x: int
    y: int

A Point value shall be a value type.

10. Class Types

Classes shall be reference types.

A class type shall be used when identity, shared ownership, or shared mutable state is semantically required.

10.1 Identity

A class type shall support identity as part of its meaning.

Two class values may be observationally distinct even when they contain the same member values.

10.2 Reference Semantics

Class values shall use reference semantics. Assignments and parameter passing shall preserve reference identity rather than converting class values into independent value copies.

10.3 Lifecycle Considerations

Class values shall participate in the language’s memory management model. The language shall ensure that ordinary code does not require manual memory management for common use cases.

10.4 Class Type Examples

class Logger:
    def log(message: str) -> None:
        ...

A Logger value shall be a reference type.

11. Protocol Types

Protocols shall define behavioral contracts.

A protocol type shall describe the requirements that a conforming type must satisfy.

11.1 Behavioral Contracts

A protocol shall specify behavior, not storage.

11.2 Conformance

A type shall conform to a protocol only when it explicitly adopts that protocol under the rules of the protocol model.

11.3 Protocol Types as Types

A protocol may appear in type positions where a behavioral contract is needed.

11.4 Associated Types

A protocol may declare associated types, which are named type relationships that are resolved by conforming types.

11.5 Protocol Constraint Example

protocol Comparable:
    def compare_to(other: Self) -> int

This example defines a behavioral contract. The details of Self and related semantics shall be interpreted consistently with later specification volumes.

12. Nullable Types

Rethon shall use non-null types by default.

A nullable type shall be an explicit type form that permits the None value.

None shall be the sole built-in absence-of-value literal.

12.1 Nullable Type Syntax

The preferred nullable form shall use a trailing marker such as ?.

Example:

name: str? = None

12.2 Non-Nullable Default

A plain type name shall denote a non-null type unless later specification volumes explicitly state otherwise for a particular special type.

12.3 Nullable Type Meaning

A nullable type shall represent a type that may contain either a value of the underlying type or the None value.

The language-level definition of explicit absence is part of the type system. The Standard Library Option<T> abstraction is defined separately in the error-handling volume.

12.4 Nullability Preservation

Type inference shall preserve nullability. If a value is inferred as nullable, the inferred type shall reflect that fact.

12.5 Nullability Examples

primary_name: str = "Rethon"
alternate_name: str? = None

13. Optional Values

Optional values at the language level shall be values of nullable types.

This rule governs the language type system's representation of absence. Standard Library abstractions such as Option<T> are defined separately in the error-handling volume.

The language shall not require a separate special runtime category to describe ordinary optionality at the type-system level.

13.1 Optionality Model

A value that may be absent shall be represented explicitly in its type.

13.2 Optional Handling

The type system shall distinguish between values that are definitely present and values that may be absent.

13.3 Relationship to None

The None value shall serve as the lexical representation of absence in nullable positions.

13.4 Examples

nickname: str? = None

This declaration states that nickname may hold a str value or None.

14. Type Inference

Rethon shall support type inference in a limited and explicit manner consistent with static typing.

Type inference shall reduce repetition where the type is obvious from context, but it shall not replace type annotations where annotations are required for clarity or where inference would be ambiguous.

14.1 Where Inference Is Permitted

Type inference shall be permitted for local declarations when the initializer or surrounding context determines the type unambiguously.

Examples:

name = "Brian"
age = 42
active = True

14.2 Where Explicit Annotation Is Required

An explicit annotation shall be required when the compiler cannot determine the type unambiguously from context.

Explicit annotation shall also be required in positions where type context is not available or where the language later specifies explicit annotation for API clarity.

Examples of positions that shall require explicit annotation include:

• function parameters
• protocol requirements that introduce typed members
• class and struct fields without an initializer
• public API surfaces where clarity is needed and inference alone would be insufficient

14.3 Inference and Nullability

Inference shall preserve nullability information.

14.4 Inference and Generics

Inference may be used with generics when the type arguments can be determined unambiguously from context.

14.5 Inference Limits

Inference shall not be allowed to create hidden type ambiguity that would weaken diagnostics or readability.

15. Type Compatibility

Type compatibility describes when one type may be used where another type is expected.

15.1 General Principle

A value shall be type-compatible with a target type only when the language rules permit that use without violating type safety.

15.2 Identity Compatibility

Types with different identities shall not be treated as automatically compatible merely because they are similar in structure.

15.3 Value and Reference Compatibility

Value types and reference types shall not be implicitly conflated. Their compatibility shall follow the explicit rules of the type system.

15.4 Protocol Compatibility

A type that conforms to a protocol shall be compatible with uses that require that protocol, subject to the rules of protocol conformance and existential or generic usage.

15.5 Nullable Compatibility

A non-null type shall not be treated as compatible with a nullable type in the opposite direction without an explicit rule or conversion.

15.6 Examples

let name: str = "Rethon"
let maybe_name: str? = name

The first assignment is allowed. The second assignment is allowed because a non-null value can inhabit a nullable type.

The reverse direction shall require a rule that handles the possibility of None.

16. Type Conversion

Type conversion is the process of forming a value of one type from a value of another type by a defined language rule.

16.1 Explicit Conversion

The language may support explicit conversion forms where a programmer intentionally converts one type to another.

16.2 Safe Conversion

Conversions that do not lose important semantic information should be preferred.

16.3 Narrowing and Widening

The language may distinguish between widening conversions that preserve meaning and narrowing conversions that may lose information.

16.4 Conversion and Nullability

Conversions involving nullable types shall preserve safety. A nullable-to-non-null conversion shall not happen silently.

16.5 Conversion Examples

count: int = 42
text: str = count.to_string()

The specific conversion mechanism is not defined in this volume, but the type system shall permit only conversions that are explicitly allowed by the language.

17. Type Casting

Type casting is the process of treating a value as a more specific or differently constrained type under an explicit rule.

17.1 Explicit Casting

The language shall require explicit syntax for casts when the programmer requests a cast rather than a conversion.

17.2 Safe Casts

Safe cast forms may be supported when a value may or may not match the requested type.

17.3 Invalid Casts

An invalid cast shall be diagnosed at compile time when statically detectable and otherwise handled according to the language’s later semantic rules.

17.4 Casts and Protocols

Casts involving protocols shall respect protocol conformance and the rules of existential use.

17.5 Cast Example

value: Any = 42
integer_value: int = value as int

The language shall define the semantics of as or any later cast syntax in later volumes.

18. Generic Types

Rethon shall support generic types.

Generic types shall be a first-class part of the type system.

18.1 Generic Structs

Structs may declare type parameters.

Example:

struct Pair<T, U>:
    first: T
    second: U

18.2 Generic Classes

Classes may declare type parameters.

Example:

class Box<T>:
    value: T

18.3 Generic Functions

Functions may declare type parameters.

Example:

def identity<T>(value: T) -> T:
    return value

18.4 Generic Protocols

Protocols may declare type parameters when the behavioral contract depends on them.

18.5 Value-Oriented Support

Generic types shall support value-oriented programming by allowing reusable abstractions over struct types without forcing class-first design.

18.6 Specialization Preference

Generic specialization shall be preferred where practical so that generic code can remain efficient in native code generation.

19. Generic Constraints

Generic constraints limit which types may be substituted for a type parameter.

19.1 Protocol-Based Constraints

Constraints shall be protocol-based.

A type parameter may be restricted to types that conform to one or more protocols.

19.2 Constraint Example

def max<T: Comparable>(a: T, b: T) -> T:
    ...

This example expresses that T must satisfy the Comparable protocol.

19.3 Multiple Constraints

The language may support multiple protocol constraints when a generic parameter must satisfy more than one behavioral contract.

19.4 Constraint Readability

Constraints shall be written in a form that is readable and explicit.

20. Associated Types

Associated types shall be supported.

Associated types are type relationships declared by a protocol and resolved by conforming types.

20.1 Purpose

Associated types allow protocols to describe relationships between a type and related types without requiring the protocol to be fully concrete.

20.2 Example

protocol Sequence:
    associatedtype Element
    def next() -> Element?

This example is illustrative. The exact syntax of later volumes may refine the associated-type form, but the underlying concept shall remain.

20.3 Associated Types and Generics

Associated types shall integrate with generic constraints and generic specialization.

20.4 Associated Type Limits

Associated types shall remain a type-system feature, not a storage feature. They describe relationships, not instance fields.

21. Existential Types

Existential types shall be supported at a high level as a way to store or pass values through a protocol-based interface without exposing the concrete type.

21.1 High-Level Meaning

An existential type represents some unknown concrete type that satisfies a protocol or protocol composition.

21.2 Use Cases

Existential types are appropriate when:

• the concrete type is intentionally hidden
• a heterogeneous collection needs a uniform abstract type
• an API boundary benefits from abstraction over concreteness

21.3 Relationship to Specialization

Existentials shall remain explicit and shall not replace generic specialization as the default performance-oriented model.

21.4 Existential Example

let printer: Printable = make_printer()

21.5 Explicit Existentials

Existential usage should remain explicit in source code whenever practical.

The language should avoid silently converting specialized generic code into existential forms.

Generic specialization remains the preferred model for performance-sensitive code, while existential types provide abstraction when the concrete type is intentionally hidden.

The type Printable in this position represents a protocol-based abstraction.

22. Type Aliases

A type alias shall provide an alternate name for an existing type.

22.1 Alias Semantics

A type alias shall not create a new type identity.

22.2 Alias Use

Type aliases shall be used to improve readability, express intent, or reduce repetition in complex type expressions.

22.3 Alias Example

type UserId = str

UserId shall be another name for str, not a distinct type.

23. Type Visibility Considerations

Types have visibility considerations because types appear in module boundaries, public APIs, and other language surface areas.

23.1 Visibility and API Clarity

Types that appear in public APIs shall be chosen with care because they define contracts that affect downstream code.

23.2 Visibility and Type Inference

Type inference may be used locally, but public type signatures should remain explicit where clarity is needed.

23.3 Visibility and Aliases

Type aliases shall not obscure the underlying visibility rules of the aliased type.

23.4 Visibility and Protocols

Protocols used as public behavioral contracts shall remain explicit and stable in source form.

24. Reflection Considerations

The type system shall support reflection in a way that is consistent with the language’s static and value-oriented design.

24.1 Type Introspection

Later specification volumes may define reflection facilities that can inspect type identity, nullability, generic arguments, and protocol conformance.

24.2 Reflection Boundaries

The type system shall not require runtime reflection for ordinary type checking.

24.3 Compile-Time and Runtime Visibility

Some type information may be available both at compile time and at runtime, but the type system itself shall remain defined by compile-time rules.

25. Future Extensions

This volume defines the current type-system direction for Rethon, but future specification work may extend the system in carefully controlled ways.

Possible future extensions include:

• additional primitive categories if genuinely needed
• richer pattern types
• intersection or union type forms where justified
• more explicit ownership-related type forms if advanced use cases require them
• enhanced existential syntax
• further specialization controls for advanced performance-sensitive code

Any future extension shall preserve the current direction:

• static typing
• value-oriented design
• reference types for identity
• protocol-oriented abstraction
• explicit nullability
• generic specialization where practical
• readable type expressions

26. Summary

The Rethon type system shall be static, nominal for user-defined types, value-oriented, protocol-oriented, and designed for native performance and long-term maintainability.

Primitive categories such as int, float, bool, char, and str shall provide the language’s foundational type vocabulary. Structs shall be value types. Classes shall be reference types. Protocols shall define behavioral contracts. Nullable types shall be explicit, with non-null as the default.

Type inference shall be limited and practical, used to reduce repetition without weakening explicitness or static safety. Generics shall be first-class, constrained primarily by protocols, specialized where practical, and used to support reusable value-oriented abstractions.

Type aliases, existentials, conversions, and casts shall all be defined in ways that preserve clarity and safety.

The type system shall remain readable, predictable, and durable enough to support the long-term evolution of the language.

If future changes are needed, they shall preserve the core principles of static typing, value orientation, protocol orientation, explicit nullability, and maintainable abstraction.