Type System (SedaroTS)
Motivation
The Sedaro Platform makes modeling and simulation implementation fast and failure hard. Our Type System, SedaroTS, is critical to achieving both of these objectives.
Make Implementation Fast
The key to making implementation fast is in composable Platform Content. Our programs are rarely a greenfield implementation effort, but rather one that primarily draws from well-tested existing Content which has operational heritage. The composability of this Content along with program-specific, customer-furnished Content is core to enabling flexible modeling and simulation solutions for our customers. There are several aspects of Sedaro's approach to simulation which enable extremely high composability:
- Sedaro Query Language (SedaroQL): Query-based analytical model (i.e. State Managers) dependency definition enables maximal composability. What works in one model can easily bind to a totally different model without manual plumbing.
- Simulator Optimizations: You can imagine that a naive implementation of "throw a bunch of existing Content into a bag and run it" would yield terrible performance. The optimizations that Sedaro's Simulator does on the libraries of Content passed to it allows us humans to not need to worry about performance when we compose a simulation.
- SedaroML: Sedaro's modeling language allows for a fluid definition of what's an Agent in a simulation
Last but not least in this list is SedaroTS. In this context, SedaroTS allows all composable Content to speak the same language. In Sedaro, it's possible to compose descriptive or analytical models with different units for distance, for example, because the type system supports safe use of units via dimensional analysis. Imagine you have a thermal solver that deals in K and you want it to interoperate in simulation with heterogenous thermal subsystems with fields in units C and F - SedaroTS makes this seamless.
Make Failure Hard
The obvious reason to have a type system is, in part, to be able to statically detect type incompatibilities (i.e. type-safety). While type-safety is a goal of SedaroTS, the intention is to also enable "unit-safety". As described above, we have what we need to compose content that speaks different, compatible units within pure simulation but we are also able to extend these perks to third-parties during collaborative modeling (i.e., co-modeling) and simulation (i.e. co-simulation).
SedaroTS also allows us to escape the confines of a specific programming language and represent our data on any computer, in any language, on any planet.
Details
"Basic" Types
| Type | Type Syntax | Example Value Syntax |
|---|---|---|
| Float | f64, float, f32, ... | 1.23 |
| Int | i64, int, u64, u8, ... | 123 |
| Bool | bool | true, false |
| String | str | "foo" |
| ID | id | "foo" |
| List | [T] | [1, 2, 3] |
| Tuple | (T, ..., T) | (1, 2.0), (1,) |
| Slice | [T; N] | [1, 2, 3] |
| Tensor | #[T; N] | [1, 2, 3], #[1, 2, 3], [1 2 3; 4 5 6] |
| Map | {T: T} | {1: 1.0, 2: 4.0} |
| Optional | T? | Some(T) -> 12, None -> () |
| Set | {T} | {1, 2} |
SI Units
| Unit | Type Syntax | Base Unit |
|---|---|---|
| Angle | rad, deg | float |
| Frequency | rpm | float |
| Time | day, min, hour | float |
| Speed | mph | float |
| Length | m, km, dm, etc. | float |
| Mass | kg, g, mg, etc. | float |
| Temperature | K | float |
| Distance | m, km, nm, etc. | float |
| Imperial Distance | ft, mi, inch | float |
| Positions | eci, ecef, lla | #[f64; 3] |
Patching/Updating
A patching/updating interface exists which allows the creation of a new TypedDatum given a compatible patch TypedDatum.
>>> typed_datum = Type("(x: float, y: float, z: float)").td((1, 2, 3))
>>>
TypedDatum('((1.0, 2.0, 3.0) : (x: float, y: float, z: float))')
>>> typed_datum | Type("(z: float,)").td((4,)) # Patch interface in python is implemented as __or__ on TypedDatum
TypedDatum('((1.0, 2.0, 4.0) : (x: float, y: float, z: float))')
Note that only Products with keys can be sparsely patched. For example, (x: float, y: float, z: float) can be patched via patch type (x: float, z: float). But (float, float, float) cannot be patched via patch type (float, float). Products without field names are patched via full replacement, within the constraint that the resulting Type cannot be different following a patch.
>>> typed_datum = Type("(float, float, float)").td((1, 2, 3))
>>> typed_datum | Type("(float,)").td((4,)) # Error
>>> typed_datum | Type("(float, float, float)").td((1, 2, 4)) # OK
TypedDatum('((1.0, 2.0, 4.0) : (float, float, float))')
Syntax Precedence
Type syntax must proceed refinements. For example, if you wanted the quantity 10 of type int and refinement m for meters, you would write (10: {int | m}).
Examples
Python
# Round trip
angle_bytes = Type("f64").ser(180.0)
assert Type("f64").de_td(angle_bytes).py() == 180.0
# Conversion
typed_datum = Type("deg").de_td(angle_bytes)
assert typed_datum.py() == 180.0
assert typed_datum.convert(Type("rad")).py() - 3.14159 < 0.0001
assert typed_datum.convert(Type("{i32 | rad}")).py() == 3
# Optional type
ty = Type("deg?")
typed_datum = ty.de_td(ty.ser(None))
assert typed_datum.py() is None
typed_datum = ty.de_td(ty.ser(90.0))
assert typed_datum.py() == 90.0
# Optional type conversion
assert Type("deg?").td(180.0).convert(Type("rad?")).py() - 3.14159 < 0.0001
assert Type("deg?").td(180.0).convert(Type("{i32 | rad}?")).py() == 3
# Arithmetic with compatible types
assert (Type("deg").td(180.0) + Type("rad").td(3.14)).py() == 360.0
# Compound types
ty = Type(f"""(
power: f64,
position: eci,
angle: deg?,
)""")
typed_datum = ty.td((
100.5,
[7000.0, 0.0, 0.0],
180.0,
))
assert typed_datum['power'].py() == 100.5
assert typed_datum['power'].convert(Type("i32")).py() == 100
assert typed_datum.convert(Type("""(power: i32, position: eci, angle: rad?)""")).py()[0] == 100
assert typed_datum.convert(Type("""(power: i32, position: eci, angle: rad?)""")).py()[2] - 3.14159 < 0.0001
# Implicit optional conversion
assert Type('int').convert(Type('int?'), 1) == 1
# Update/Patch TypedDatum
# Sparse
typed_datum = Type("(x: float, y: float, z: float)").td((1, 2, 3))
typed_datum |= Type("(z: float,)").td((4,))
assert typed_datum.py() == (1.0, 2.0, 4.0)
# Full
typed_datum = Type("(float, float, float)").td((1, 2, 3))
typed_datum |= Type("(float, float, float)").td((1, 2, 4))
assert typed_datum.py() == (1.0, 2.0, 4.0)
Demo
Pretty Printing
Dynamic Inference
Dynamic Conversion
Dynamic Type Checking
TypedDatums
TypedDatums are a way to represent a Type and a Datum together, it is created with the format (Value: Type). Eg: (10: {float | m/s/s}), (10, false: (i32, bool)), or (10: i32).
Indexing
TypedDatum and Type provide indexed access via get, which accepts either a numeric index or a key.
Arithmetic Operators
TypedDatum supports arithmetic operations like addition, subtraction, multiplication, and division.