In the process of incorporating subtyping in relation algebra, an algorithm was found to derive the subtyping relation from the program to be checked. By using domain analysis rather than type inference, this algorithm offers an attractive visualization of the type derivation process. This visualization can be used as a graphical proof that the type system has assigned types correctly. An implementation is linked to in this paper, written in Haskell. The algorithm has been tried and tested in Ampersand, a language that uses relation algebra for the purpose of designing information systems.
|Title of host publication||Relational and Algebraic Methods in Computer Science (15th International Conference, RAMiCS 2015, Braga, Portugal, September 28-October 1, 2015)|
|Editors||W. Kahl, M. Winter, J.N. Oliveira|
|Publication status||Published - 2015|
|Name||Lecture Notes in Computer Science|
Joosten, S. M. M., & Joosten, S. J. C. (2015). Type checking by domain analysis in Ampersand. In W. Kahl, M. Winter, & J. N. Oliveira (Eds.), Relational and Algebraic Methods in Computer Science (15th International Conference, RAMiCS 2015, Braga, Portugal, September 28-October 1, 2015) (pp. 225-240). (Lecture Notes in Computer Science; Vol. 9348). Springer. https://doi.org/10.1007/978-3-319-24704-5_14