Tuple-Set Constraints and Ambiguous Constraint Solving in MLscript

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering

Final Year Thesis Oral Defense

Title: "Tuple-Set Constraints and Ambiguous Constraint Solving in MLscript"

by

AU Heung Tung

Abstract:

MLscript is a programming language supporting subtyping, first-class unions, 
intersections, and ML-style type inference. On the other hand, it performs 
approximation when interpreting the intersection between function types. In 
this project, we extend the type system of MLscript with tuple-set constraints 
to retain more precise types and solve ambiguous constraints. Then, we encode 
function overloading using intersection types in MLscript.

A tuple-set constraint attaches a set of tuples containing bounds to types. 
Tuples with unsatisfiable constraints are pruned after receiving bounds on type 
variables. It allows types to depend on each other and can express bounds on 
them more precisely to avoid approximation. We formalize the approach and 
present an algorithm for establishing the tuple-set constraint on an overloaded 
function. We also implement a constraint-solving algorithm and modify the type 
simplifier in MLscript.

This project presents an approach to expressing and solving ambiguous 
constraints. It adds support for function overloading with precise typing in 
MLscript. The proposed tuple-set constraints may also be applied to achieve 
refined pattern matching in an inferrable way as an alternative to match types.


Date            : 27 April 2024 (Saturday)

Time            : 11:30 - 12:10

Venue           : Room 3494 (near lifts 25/26), HKUST

Advisor         : Dr. PARREAUX Lionel

2nd Reader      : Dr. SHEN Jiasi