Student Projects

Are you interested in a semester/master project at LAMP? Here are potential projects that we have thought of. However, feel free to contact us about your own ideas as well.

Most of the following projects are related to Dotty, which is the next-generation Scala compiler, developed in the lab, and slated to become Scala 3.

Reimplement macros of Chisel3 in Dotty (taken)

Type: master semester project, master thesis project
Major: computer science, communication systems, data science
Supervisor: Fengyun LiuNicolas Stucki
Students: 1

Chisel3 [1] is a hardware construction language embedded in Scala. It has been used to design RISC-V chips [2]. The project Chisel3 uses a large amount of Scala 2 macros. Dotty has introduced a new macro system [3], which is supposed to be safer and more friendly to meta-programmers. The goal of the project is to reimplement the macros in Dotty and port Chisel3 to Dotty.

[1] https://github.com/freechipsproject/chisel3
[2] https://boom-core.org/
[3] http://dotty.epfl.ch/docs/reference/other-new-features/tasty-reflect.html

A Tasty Interpreter for Scala

Type: master thesis project
Major: computer science, communication systems, data science
Supervisor: Sébastien Doeraene
Students: 1

The goal of the project is to implement an interpreter for Scala based on Tasty. Tasty [1] is the standard immediate representation of Scala programs. Most Scala programs depend on classes defined in JDK, a challenge is how to deal with those dependencies. To alleviate the interop problem, we will develop the interpreter on top of Scala.js [2], which has an implementation of the most commonly used classes of JDK in Scala, and whose interop semantics with JavaScript is well-defined. The evaluation of the project will be whether the interpreter can successfully interpret all the run tests in the Dotty compiler.

[1] Tasty format
[2] https://www.scala-js.org/

Evaluating and Improving performance of generic tuples code generation (taken)

Type: bachelor semester project, master semester project, master thesis project
Major: computer science, communication systems, data science
Supervisor: Nicolas Stucki
Students: 1

High-performance computing can be achieved by generating programs specialized for a given set of parameters. Examples of tools doing that are Lightweight Modular Staging [1] and Spark [2]. In Dotty, runtime code generation is built-in and provided via the “principled meta-programming” facility [3]. The goal of this project is to compare this staging mechanism with the aforementioned tools. The axes of comparison would be both the performance and the expressivity.

Evaluating the runtime code generation system of Dotty (taken)

Type: Master semester or thesis project
Major: computer science, communication systems, data science
Supervisor: Julien Richard-Foy, Nicolas Stucki
Students: 1

Scala 2 had tuple classes from 1 to 22, in Dotty we dropped this limit and added some library level code optimizations. We currently have some optimizations that look into the type of the tuples to know their size an generate more specialized code for operation on small tuples smaller. Both the code specialization and the execution of said code should run as fast as possible.

The aim of this project is to create performance test that shows how long it took to compile and how fast the generated code runs. Then try different combinations of the optimizations to find the optimal solution.

Formal foundations for GADTs in Scala

Type: Master thesis project
Major: computer science, data science, communication systems
Supervisor: Aleksander Boruch-Gruszecki
Student: 1

In Dotty, GADTs are a special case of enums (or sealed hierarchies) that, after having pattern-matched on them, can expose additional information about type parameters to enclosing functions. See [1] for an example. Also see [2] for a similar example in Haskell, with more examples and information in [3].

In Haskell, GADTs are formally understood through type coercions of System FC(X) [4]. However, we have good reasons to believe that in DOT-related calculi, GADTs can be encoded through a combination of singleton types, intersection and a very simple form of pattern matching – pDOT [5] contains all but the last. We would like to understand whether pDOT (with small modifications) is sufficient to explain GADTs, or whether explicit support for them is necessary; and if there is a correspondence between type coercions of System FC(X) and an encoding of GADTs in pDOT.

The aim of this project is to further our understanding in the above direction. As such, multiple outcomes are equally valid:

  • showing isomorphism between (a subset of) FC(X) terms and pDOT terms
  • encoding (a subset of) Dotty enums in pDOT and showing that constraints which Dotty infers from pattern matching follow from type intersections
  • demonstrating that GADTs cannot, in fact, be encoded in pDOT; discussing why that is the case and proposing extensions which could allow encoding them

This is a very challenging, pure research topic. A large degree of self-sufficiency and a large amount of work will be necessary to achieve a good result.

[1] – https://github.com/lampepfl/dotty/blob/master/tests/pos/gadt-eval.scala
[2] – https://en.wikipedia.org/wiki/Generalized_algebraic_data_type
[3] – https://wiki.haskell.org/Generalised_algebraic_datatype
[4] – https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf
[5] – https://arxiv.org/abs/1904.07298