Refinement types

[jclark]

The idea is that you can use a limited form of expression to constrain a type. The syntax could look like this:

type positiveInt = int where self > 0;

The difficulty is that static type checking becomes very challenging. How would you tell that the type of positiveInt + positiveInt is a positiveInt? One approach is to use an SMT solver.

See paper "Semantic Subtyping with an SMT Solver" by Bierman, Gordon & Langworthy from Microsoft:

https://www.microsoft.com/en-us/research/wp-content/uploads/2010/12/icfp09i-bierman.pdf

This is probably too researchy for Ballerina at the moment, but I want to have an issue to capture the general concept.

Edited: fully static is too researchy, but we don't have to do that.

[jclark]

Better syntax:

type-definition := "type" identifier type-descriptor [type-constraint] ";"
type-constraint :="where" expression

The expression in a type-constraint is boolean expression, in which identifier is bound to a value of the type described by type-descriptor, e.g.

type PositiveInt int where PositiveInt >= 0;

The expression in a type-constraint would be required to be isolated to stop things getting too crazy.

The type-constraints would not be checked statically, but would rather be checked at specific language-defined points, including:

• when a service remote or resource method is invoked
• by the langlib xyzWithType functions (e.g. cloneWithType)
• explicitly when requested by the user using a language-defined mechanism

[jclark]

See also Refinement types in Jolie.