-
Notifications
You must be signed in to change notification settings - Fork 30
Project: DSL Type Formalisation
Rosetta supports a wide range of expressions and operations for specifying the output of a function. For example, we can define a function that either multiplies or divides two integers, depending on whether their sum is smaller than 10, by combining a conditional expression (if-then-else), arithmetic operators (+, *, /) and a comparison operator (<).
func MulOrDiv:
inputs:
a int (1..1)
b int (1..1)
output:
result number (1..1)
set result:
if a + b < 10 then
a * b
else
a / b
By combining the wide variety of available expressions, our users can effectively specify any kind of functionality. However, making mistakes is part of being human, so sometimes we might write expressions that do not make sense, especially when working on a large project. For example, suppose that by accident we would have copied over the comparison < 10 to the second operation: if a + b then a * b < 10 else a / b. For our condition, a + b, we expect a boolean value, but we get an integer, and for the result we expect a number, but we return the boolean value a * b < 10 instead.
Luckily, our system automatically validates any Rosetta code and provides immediate and direct feedback to our users when making such a mistake. In this way the user is made aware of the problem and they can resolve the issue.
Currently, every time we add a kind of expression or operation, we try to come up with validation rules to prevent misuse. However, using this process, we often miss use cases. For example, the following expression does not make any sense, but our system currently does not catch the mistake.
if [True, False] then
5 / [1, 2]
else
1 + empty
Similarly, the cardinality of expressions is often not checked thoroughly, allowing mistakes in a Rosetta model such as the following.
func ListOfThree:
output: result int (3..3)
set result: [1, 2, 3, 4]
The thesis Formalizing a Modelling Language for the Financial Industry by Simon Cockx has analyzed this problem and we intend to implement its proposed solution.
Phase 1 (explorative): enhanced validation for literals, binary operations and conditional expressions
Problem: Our validator often misses cases of invalid expressions.
Example: The following erroneous expression is not detected.
if [True, False] then
5 / [1, 2]
else
1 + empty
Solution: We intend to use a more disciplined approach for validating expressions by implementing the type system as proposed in the thesis Formalizing a Modelling Language for the Financial Industry by Simon Cockx. In this way we get a system that can actually reason about expressions, which allows us to give complete validation for our users, effectively getting rid of missed cases. As an initial proof-of-concept, we focus on literals, binary operations and conditional expressions. We will implement the type system using the Xsemantics framework.
Long-term benefits:
-
When extending Rosetta by adding new kinds of expressions, adding correct validation becomes less work and much less error-prone than the current approach.
-
We can use the type system to improve Rosetta in other ways. For example, we could provide smarter code completion for Rosetta users. Moreover, this type system would allow us to resolve some issues with code generation (i.e., type coercion).
-
literals (done)
-
list literals (done?)
-
conditional expressions (done?)
-
binary operations
-
arithmetic expressions
[Project:-DSL-Syntax-Simplifications-and-Improvements]
In this phase, we intend to complete the work done in phase 1 by covering all kinds of expressions.
https://github.com/REGnosys/rosetta-dsl/wiki/Project:-DSL-Semantics-formalization