Sigmal Language Specification — Part 07
Open Questions Appendix (Language-Level Consolidated)
Top > Design docs > Core design > Part 07 (Appendix)
This section lists unresolved design questions and potential future extensions.
These topics are intentionally left open to preserve flexibility while maintaining the core principles of Sigmal.
1. Ownership and Memory Discipline
The precise ownership model is not yet specified.
Questions include:
- Should Sigmal define an explicit ownership system?
- Should borrowing be modeled at the type level?
- Can ownership be encoded purely structurally without adding new primitives?
- Should reference counting be a library abstraction or receive compiler assistance?
- How can deterministic destruction be guaranteed without impurity?
Any ownership model must:
- Preserve purity
- Preserve totality
- Avoid implicit mutation
- Avoid hidden runtime machinery
2. Effect Tracking at the Type Level
Effects are currently encoded explicitly via:
- Free constructions
- Capability records
- Explicit state threading
Open questions:
- Should there be a lightweight effect annotation mechanism?
- Can effect tracking be implemented without implicit inference?
- How can effect typing remain explicit while ergonomic?
- Should effect polymorphism exist?
Any effect tracking system must:
- Avoid implicit propagation
- Avoid global inference
- Preserve explicit capability discipline
- Maintain deterministic compilation
3. Law Encoding Strategy
Abstractions such as Functor and Monad do not encode laws by default.
Open questions:
- Should algebraic laws be expressible as fields?
- Should proofs be embedded directly in abstraction records?
- Should a lightweight proof discipline be provided?
- Can law-checking be assisted by tooling without altering core semantics?
The compiler does not assume any algebraic law.
4. Universe Ergonomics
Universe levels are explicit and const-normalizable.
Open questions:
- Should universe polymorphism receive surface sugar?
- Should implicit universe parameters be permitted?
- Can universe level inference remain deterministic?
- How can error messages remain comprehensible?
Any refinement must preserve:
- Stratification
- Totality
- Deterministic normalization
5. Symbol Generation Discipline
Symbols (Sym) are structural identity atoms.
Open questions:
- Should there be standardized symbol constructors (e.g., UUID-based)?
- Should symbol generation be purely library-defined?
- How are symbol collisions handled across modules?
- Should symbol representation stability be guaranteed across compilation units?
Symbols must remain:
- Deterministic
- Structural
- Free of global registries
6. Cross-Module Linking Semantics
Module resolution is external to the core language.
Open questions:
- How should cross-module ABI compatibility be verified?
- Should structural type equality be enforced at link time?
- Should module identity hashes be generated?
- How can deterministic linking be guaranteed across environments?
The resolver must remain deterministic.
7. Stable ABI Specification
Targets define ABI details.
Open questions:
- Should Sigmal define a canonical ABI description format?
- Should ABI stability be guaranteed across compiler versions?
- How should inductive layout compatibility be maintained?
ABI design must preserve semantic equivalence.
8. Optimization of Dictionary Passing
Dictionary passing is explicit.
Open questions:
- Should the compiler automatically specialize abstraction dictionaries?
- Should partial evaluation be applied aggressively?
- Can specialization preserve separate compilation?
- How can optimization remain transparent?
Optimization must not introduce implicit instance resolution.
9. Optimization of Effect Encodings
Free constructions may introduce overhead.
Open questions:
- Can fusion eliminate intermediate constructors?
- Should effect encodings receive backend assistance?
- Can handlers be compiled efficiently without sacrificing purity?
Optimizations must preserve:
- Explicit semantics
- Structural equivalence
- Determinism
10. Deterministic Builds
Deterministic compilation is a goal.
Open questions:
- Should compilation artifacts include reproducibility guarantees?
- How are symbol representations stabilized?
- How are hashes computed across platforms?
- Should the resolver configuration be embedded in artifacts?
Determinism must hold for:
- Parsing
- Type checking
- Normalization
- Code generation
11. Surface Ergonomics
Sigmal intentionally avoids reserved alphanumeric keywords.
Open questions:
- Should ergonomic sugar (e.g., sequencing notation) be provided?
- How much surface sugar is acceptable without harming clarity?
- Should pattern matching syntax be refined further?
- Can abstraction syntax be simplified further?
Surface changes must preserve:
- Deterministic parsing
- Uniform semantics
- Minimal reserved tokens
12. Verified Compilation
Sigmal’s total core invites formal verification.
Open questions:
- Should a formally verified core elaborator be produced?
- Should normalization be proven correct?
- Can the compilation pipeline be mechanically verified?
- Should a proof-carrying artifact format exist?
Such efforts must preserve:
- Structural typing
- Deterministic behavior
- Minimal runtime assumptions
13. Long-Term Direction
Sigmal aims to:
- Provide logical generality comparable to proof assistants
- Preserve practical systems-level usability
- Avoid hidden runtime complexity
- Maintain explicit abstraction discipline
Future extensions must not compromise:
- Totality
- Purity
- Explicitness
- Determinism
- Structural coherence
14. Summary
The open questions of Sigmal focus on:
- Ownership discipline
- Effect tracking
- Law encoding
- ABI stability
- Deterministic builds
- Optimization strategies
- Symbol stability
- Surface ergonomics
All future design decisions must preserve the core principles defined in Part 01.
Sigmal.org - the calculus we can build on