Type Inference Zoo

Welcome to Type Inference Zoo! This project is dedicated to implementing a variety of type inference algorithms. It serves as a personal project, as I am trying to understand the type inference algorithms well by implmenting them. Considering that it might be helpful for those who are also exploring type inference algorithms, I am glad to make them avaliable online.

🗿🗿🗿 There are indeed animals (implementations) in the zoo, not only references to animals.

A static online web demo is available for you to try at https://zoo.cuichen.cc/.

🚀 Get Started

To get started with the project, clone the repository and build the project using stack:

git clone https://github.com/cu1ch3n/type-inference-zoo.git
cd type-inference-zoo
stack build
stack exec type-inference-zoo-exe -- "let id = \x. x in (id 1, id True)" --alg W

Research Works Implemented

• W: ./src/Alg/HDM/AlgW.hs
  • Robin Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, 1978. [Paper]
• DK: ./src/Alg/DK/DK.hs
  • Jana Dunfield and Neelakantan R. Krishnaswami. Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. ICFP 2013. [Paper]
• Worklist: ./src/Alg/DK/Worklist/DK.hs
  • Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference. ICFP 2019. [Paper]
• Elementary: ./src/Alg/DK/Worklist/Elementary.hs
  • Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference. ECOOP 2022. [Paper]
• R: ./src/Alg/HDM/AlgR.hs
  • Roger Bosman, Georgios Karachalias, Tom Schrijvers. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. ITP 2023. [Paper]
• Bounded: ./src/Alg/DK/Worklist/Bounded.hs
  • Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira. Greedy Implicit Bounded Quantification. OOPSLA 2023. [Paper]
• Contextual: ./src/Alg/Local/Contextual/Contextual.hs
  • Xu Xue and Bruno C. d. S. Oliveira. Contextual Typing. ICFP 2024. [Paper]
• IU: ./src/Alg/DK/Worklist/IU.hs
  • Shengyi Jiang, Chen Cui and Bruno C. d. S. Oliveira. Bidirectional Higher-Rank Polymorphism with Intersection and Union Types. POPL 2025. [Paper]

Contribution

Contributions are welcome! If you're interested in improving this project, please feel free to open an issue or submit a pull request.

License

This project is licensed under the MIT License.

Disclaim

This project is still in its early stages, and I am not an expert in either type inference or Haskell :) Please use it at your own risk (Some of the code was assisted by GitHub Copilot or ChatGPT). If you spot any issues or have suggestions, please open an issue to help improve the project.