4 ms·

This brings back memories from my type inference work... Hindley-Milner is very simple to understand, it's just the formalization that's too dense.

benbataille 14y ago
I tend to disagree with you in the sens that Damas-Milner seems to me as the typical exemple of an algorithm which seems simple but actually have subtle implication and trade-off. Robinson's unification which is at the center of the algorithm is already made a bit tricky by quantification as soon as you have polymorphism. Then, some rules have actually deeper implication and trade-off than it seems (especially let). For people interested in type checkers, there is a couple of really good chapters by written by Peter Hancock in a book available online : The Implementation of Functional Programming Languages by Simon Peyton Jones. They entirely cover the theory and there is a complete implementation in Miranda. Here is the link : http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/PAGES/139.HTM http://research.microsoft.com/en-us/um/people/simonpj/papers...
VikingCoder 14y ago
Two professors were arguing in front of a chalkboard, for hours and hours. Finally one of them nodded in agreement and said, "You're right, it's trivial."
- qu4z-2 14y ago
  I've been in situations like this. I'll give a simple rule set of some topic that someone hasn't quite managed to defragment in their brain (and thus know it as a bunch of rules and special-cases), and then they'll spend hours going "But what if <x>?". Eventually they believe me that my simplified model is equivalent to their overcomplicated internal model. The result is usually closer to "You're right; it is that simple." but that's fairly similar to "It's trivial." In short: Often people need to try a lot of "Yeah, but what if <x>?" before they satisfy themselves that something is in fact as simple as it appears.

benbataille 14y ago

I tend to disagree with you in the sens that Damas-Milner seems to me as the typical exemple of an algorithm which seems simple but actually have subtle implication and trade-off. Robinson's unification which is at the center of the algorithm is already made a bit tricky by quantification as soon as you have polymorphism. Then, some rules have actually deeper implication and trade-off than it seems (especially let). For people interested in type checkers, there is a couple of really good chapters by written by Peter Hancock in a book available online : The Implementation of Functional Programming Languages by Simon Peyton Jones. They entirely cover the theory and there is a complete implementation in Miranda. Here is the link : http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/PAGES/139.HTM http://research.microsoft.com/en-us/um/people/simonpj/papers...

VikingCoder 14y ago

Two professors were arguing in front of a chalkboard, for hours and hours. Finally one of them nodded in agreement and said, "You're right, it's trivial."

qu4z-2 14y ago
I've been in situations like this. I'll give a simple rule set of some topic that someone hasn't quite managed to defragment in their brain (and thus know it as a bunch of rules and special-cases), and then they'll spend hours going "But what if <x>?". Eventually they believe me that my simplified model is equivalent to their overcomplicated internal model. The result is usually closer to "You're right; it is that simple." but that's fairly similar to "It's trivial." In short: Often people need to try a lot of "Yeah, but what if <x>?" before they satisfy themselves that something is in fact as simple as it appears.