The project will start by formalising the Simply Typed Lambda Calculus (STLC) as a minimalistic language that will be used to implement the type inference algorithms. The STLC will be based on the languages formalised in the papers and will include the core concepts of the type inference algorithms.
A natural choice for the implementation of the STLC would be Haskell, as it is a functional programming language that is well-suited for implementing type inference algorithms with support for pattern matching, but Scala may be more appropriate considering the fact that it allows for side-effects that can be useful for optimising the algorithms. Additionally, Scala also has good support for Monads (and other functional programming constructs) that leaves the doors open for us to re-engineer (or refactor) work-lists to possibly uncover a monadic structure.
The parser for the STLC is planned to be implemented using a parser combinator library, such as fastparse or Parboiled2 in Scala, to allow for easy extensibility and maintainability. The parser will be used to parse the input programs and convert them into an abstract syntax tree (AST) that can be used by the type inference algorithm. Moreover, such libraries provide a high-level of abstraction that allows for easy composition of parsers and error handling.
The REPL could then be implemented using the parser and the defined syntax for the STLC. The REPL will allow users to interactively enter programs and see the type inference results in real-time. This will help in testing the type inference algorithm and providing immediate feedback to the user.
If time allows, the team would also work towards implementing the extra objectives such as an elaboration to a target calculus or the addition of other advanced features mentioned above. Although the details of their implementation are not yet clear, the team will discover and implement them as the project progresses.
However these are not essential for the core functionality of the project, they would provide additional value to the project and help in understanding the practical implications of the algorithms.