Skip to content

Project: DSL Type Formalisation

SimonCockx edited this page Aug 17, 2022 · 14 revisions

Context: validation of expressions

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.

Problem: validation is currently implemented ad hoc, resulting in missed issues

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).

Completed

  • literals
  • list literals
  • conditional expressions
  • binary operations
  • arithmetic expressions

Phase 2: Syntax Simplifications and Improvements

Project:-DSL-Syntax-Simplifications-and-Improvements

Phase 4: Complete type validation for all Rosetta expressions

In this phase, we intend to complete the work done in phase 1 by covering all kinds of expressions.