Hindley-Damas-Milner algorithm

The Hindley-Damas-Milner algorithm (traditionally also known as Algorithm W) is a type inference algorithm that finds the most general type of a term of the untyped \lambda-calculus.

Bidirectional type checking

A bidirectional ersion of the Hindley-Damas-Milner algorithm is given in Gandry et al. 2010.

References

The algorithm for type inference was presented in

Hindley, R. ‘The Principal Type-Scheme of an Object in Combinatory Logic’. Transactions of the American Mathematical Society 146 (1969): 29. https://doi.org/10.2307/1995158.

@article{hindley_1969,
	title = {The Principal Type-Scheme of an Object in Combinatory Logic},
	volume = {146},
	doi = {10.2307/1995158},
	pages = {29},
	journaltitle = {Transactions of the American Mathematical Society},
	author = {Hindley, R.},
	date = {1969},
}

Milner, Robin. ‘A Theory of Type Polymorphism in Programming’. Journal of Computer and System Sciences 17, no. 3 (1978): 348–75. https://doi.org/10.1016/0022-0000(78)90014-4.

@article{milner_1978,
	title = {A theory of type polymorphism in programming},
	volume = {17},
	doi = {10.1016/0022-0000(78)90014-4},
	pages = {348--375},
	number = {3},
	journaltitle = {Journal of Computer and System Sciences},
	author = {Milner, Robin},
	date = {1978},
}

Damas, Luis. ‘Type Assignment in Programming Languages’. PhD thesis, University of Edinburgh, 1984. http://hdl.handle.net/1842/13555.

@thesis{damas_1984,
	title = {Type assignment in programming languages},
	url = {http://hdl.handle.net/1842/13555},
	institution = {University of Edinburgh},
	type = {phdthesis},
	author = {Damas, Luis},
	date = {1984},
}

A bidirectional version of it is given in

Gundry, Adam, Conor McBride, and James McKinna. ‘Type Inference in Context’. In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 43–54. Association for Computing Machinery, 2010. https://doi.org/10.1145/1863597.1863608.

@inproceedings{gundry_2010,
	title = {Type inference in context},
	doi = {10.1145/1863597.1863608},
	pages = {43--54},
	booktitle = {Proceedings of the third {ACM} {SIGPLAN} workshop on Mathematically Structured Functional programming},
	publisher = {Association for Computing Machinery},
	author = {Gundry, Adam and {McBride}, Conor and {McKinna}, James},
	date = {2010}
}