Indexed Types / Constraint Domain System for C# #9865
Unanswered
xtofs
asked this question in
Language Ideas
Replies: 2 comments 14 replies
-
|
I know units of measure have come up a couple of different times but I don't see a single discussion used as the source of truth. Most point back to "roles" as being a solution: |
Beta Was this translation helpful? Give feedback.
1 reply
-
|
For physical measurements, it's trivial to put together struct wrappers which satisfy all of the requirements: ensuring that values of different units don't intermingle, applicable operations (like distance divided by time equals speed, etc.); I fail to see how a language feature is needed at all for them. |
Beta Was this translation helpful? Give feedback.
13 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
Indexed Types: A Constraint Domain System for C#
Abstract
This document proposes a compiler extension for C# that enables lightweight indexed types - a generalization of F#'s units-of-measure system.
The core idea is to attach compile-time indices to types, making values with different indices incompatible by default. For example, a
Quantity<Length>cannot be added to aQuantity<Time>— the compiler rejects such operations. However, controlled compatibility is possible through operations that transform indices: dividingQuantity<Length>byQuantity<Time>yieldsQuantity<Velocity>, where the resulting index is computed from the operands.The key innovation is allowing users to define custom constraint domains where types can be indexed by elements from user-defined algebraic structures. The compiler performs constraint solving during type inference, then erases all index information before code generation, resulting in zero runtime overhead.
1. Introduction
1.1 Motivation
Many programming domains benefit from tracking additional type-level information that doesn't affect runtime behavior:
Current approaches in other languages using phantom types or type-level programming are verbose and are challenges by proper type inference. This proposal introduces a systematic way to add such tracking with minimal syntactic overhead.
1.2 Design Goals
Zero runtime cost: All index information erased before code generation
Automatic inference: Type checker solves constraints automatically
User extensibility: Users can define new domains without compiler changes
Natural syntax: Leverage existing C# syntax and operators
Type safety: All checking happens at compile time
1.3 Relationship to Existing Work
This proposal generalizes Andrew Kennedy's units-of-measure system from F#, making it:
2. Core Concepts
2.1 Indexed Types
An indexed type is a type parameterized by an index from a constraint domain:
Where:
index DimensionDomainis a constraint marking it as an index parameter2.2 Constraint Domains
A constraint domain defines:
Normalize()method for canonical representation (see below)The Normalize Method (Optional)
After evaluating an index expression, the compiler checks if the index type defines a
Normalize()method. If present, it is called to reduce the result to a canonical form before type unification.Normalization is required when:
2/4and1/2)Normalization is not needed when:
Dimension(0, 1, 0)has only one representation for "Length"SecurityLevel(2)has only one representation for "Secret"For a detailed example where normalization is essential, see Appendix A.
Example Domain (no normalization needed):
2.3 Index Expressions
Index expressions appear in type positions and use the operations defined on the index type:
The compiler translates these to actual operations on the index type.
3. Syntax Extensions
3.1 Index Parameter Constraints
Type parameters can be constrained as indices using the
indexkeyword in where clauses:This follows the familiar C# pattern:
3.2 Index Expressions in Constraints
Index expressions can appear in where clauses.
The syntax is:
where T : index Domain(expression), naming the domain and writing the expression in familar C# expression syntax:3.3 Syntax Variations
Several syntactic forms for index expressions:
3.4 Alternative: Expression After Colon
For brevity, the domain could be inferred from context:
This is terser but potentially ambiguous. The full form index Domain(expr) is clearer.
4. Type Inference and Constraint Solving
4.1 Constraint Generation
When the compiler encounters operations on indexed types, it generates index constraints:
4.2 Constraint Solving
The compiler solves constraints by:
Normalizemethod)To solve:
TResult where TResult : index DimensionDomain(Length / Time)The
Dimensiontype is already in normal form (integer exponents), so no normalization step is needed. For an example where normalization is required, see Appendix A: Normalization Example.4.3 Type Erasure
After type checking, all index information is erased:
// After erasure (runtime type)
5. Example: Units of Measure
5.1 Domain Definition
5.2 Quantity Type
5.4 Type Aliases for Readability
6. Example: Information Flow Security
6.1 Domain Definition
6.2 Classified Data Type
6.3 Usage Example
7. Example: Effect System
7.1 Domain Definition
7.2 Effectful Computation Type
7.3 Usage Example
10. Compiler Implementation
10.1 Required Compiler Changes
The implementation requires modifications to several compiler phases:
10.2 Error Messages
Appendix A: Normalization Example
Some index types require normalization to ensure equivalent values are recognized as equal during type unification. This appendix demonstrates a
Fractiondomain where normalization is essential.A.1 The Problem
Consider a domain for tracking fractional scaling factors. Without normalization,
Fraction(2, 4)andFraction(1, 2)would be considered different types, even though they represent the same value:A.2 Domain Definition with Normalize
A.3 Constraint Solving with Normalization
To solve:
TResult where TResult : index FractionDomain(Half * Half)where
Half = Fraction(1, 2)Another example showing normalization in action:
To solve:
TResult where TResult : index FractionDomain(TwoFourths * Half)where
TwoFourths = Fraction(2, 4)andHalf = Fraction(1, 2)With normalization, both
Fraction(1,2) * Fraction(1,2)andFraction(2,4) * Fraction(1,2)resolve to the same canonical formFraction(1, 4), enabling correct type unification.A.4 Usage Example
References
Kennedy, Andrew J. Dimension Types. PhD thesis, University of Cambridge, 1996.
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf
Kennedy, Andrew. "Types for Units-of-Measure: Theory and Practice." Central European Functional Programming School (CEFP 2009), Lecture Notes in Computer Science, vol. 6299, Springer, 2010.
https://link.springer.com/chapter/10.1007/978-3-642-17685-2_8
Scala 3 Documentation. "Opaque Type Aliases."
https://docs.scala-lang.org/scala3/book/types-opaque-types.html
Note: Scala 3's opaque types provide zero-cost type distinctions but without algebraic operations on indices. They prevent mixing of types but don't support computing result types from operations (e.g., Length / Time → Velocity).
Beta Was this translation helpful? Give feedback.
All reactions