Home

Awesome

Semantic Subtyping for Ballerina

This is an experimental implementation of semantic subtyping for the type system of the Ballerina programming language, implemented in Ballerina.

The algorithm here is based on the work of Giuseppe Castagna and Alain Frisch, implemented in CDuce. I have found the most accessible paper to be:

Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers), G. Castagna, 2020

Section 4 of the above paper has a description of the algorithms.

There is also a tutorial by Andrew M. Kent, which is great for getting started:

Down and Dirty with Semantic Set-theoretic Types (a tutorial)

The implementation currently handles a subset of Ballerina type system:

Most of the code is in modules:

The JSON representation of types is Lisp-like, and documented in the file schema.bal.

Running the program checks the type relationships asserted in tests.json. This is a JSON file that contains an array of tests; each test is a triple [R, T1 T2], where R is a string specifying the relationship that holds between T1 and T2, as follows:

The program can be built with the Swan Lake Alpha5 version of Ballerina.

There is a list of everything still to be done to handle the whole type system. There are also implementation notes.