|
| 1 | +--- |
| 2 | +title: Improve name resolution in Liquid Haskell |
| 3 | +--- |
| 4 | + |
| 5 | +Liquid Haskell is a tool to verify Haskell programs. The programmer supplies |
| 6 | +specifications for functions and data types in special comments, and the tool |
| 7 | +produces error messages when it cannot automatically prove that the program |
| 8 | +behaves as specified. The programmer can then improve the specifications or the |
| 9 | +program until the tool reports no errors. More information is available on the |
| 10 | +[Liquid Haskell website](https://ucsd-progsys.github.io/liquidhaskell/). |
| 11 | +Similar to a type system in spirit, Liquid Haskell enrols the computer |
| 12 | +in the effort to discover |
| 13 | +[programming mistakes](https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/). |
| 14 | + |
| 15 | +Liquid Haskell has been around for a decade and is a versatile tool, but it |
| 16 | +still has a few issues which hinder the user experience. This project is to |
| 17 | +address one of these shortcomings. |
| 18 | + |
| 19 | +When analyzing a program, Liquid Haskell needs to link identifiers that appear |
| 20 | +in specifications to the entities they refer to, much in the same way that a |
| 21 | +compiler needs to link identifiers in the text of a function to the language |
| 22 | +entities that they represent. We refer to this task as name resolution. |
| 23 | + |
| 24 | +The identifiers in a specification can refer to other specifications, or they |
| 25 | +can refer to Haskell entities like functions and types. The output of name |
| 26 | +resolution tells for each identifier the module in which the referred entity is |
| 27 | +defined and the package it comes from. |
| 28 | + |
| 29 | +At the moment, name resolution in Liquid Haskell is done twice for the same |
| 30 | +specifications, and the outcomes of both passes do not always yield the same |
| 31 | +result, leading to confusing errors and tedious workarounds. This project is |
| 32 | +about having name resolution done only once. For more details please see |
| 33 | +[the github issue](https://github.com/ucsd-progsys/liquidhaskell/issues/2169). |
| 34 | +The project involves both the implementation of a solution and the writing of |
| 35 | +a blog post summarizing the achievements. |
| 36 | + |
| 37 | +As a stretch goal, this project might specify and fix the scope rules |
| 38 | +and mechanisms to use in Liquid Haskell specifications. |
| 39 | +While the intention of Liquid Haskell maintainers over time has been to |
| 40 | +imitate GHC scoping rules as much as possible, there are cases where Liquid |
| 41 | +Haskell just deviates from them. |
| 42 | +As part of attaining this supplementary stretch goal, one would need to answer |
| 43 | +questions like the following. |
| 44 | + |
| 45 | +* What names are in scope when writing the specifications of a module? |
| 46 | + |
| 47 | +* How should ambiguities be resolved when imports offer definitions with the same Liquid Haskell names? |
| 48 | + |
| 49 | +* What Liquid Haskell names are exported from modules and when? |
| 50 | + |
| 51 | +**Potential Mentors**: Facundo Domínguez |
| 52 | + |
| 53 | +**Difficulty**: Medium |
| 54 | + |
| 55 | +**Size**: 350 hours but they are flexible by adjusting the scope |
0 commit comments