That's a nice overview of Hindley-Milner in practice!
For those interested, I recently have been thinking of a better way to specify type inference with principal derivations that lends itself better for type system extensions:
The man, the myth, the legend! Ok, so for extensible records: I don't have a good intuition for why the record objects would have to keep around the shadowed (hidden/duplicate) fields at run-time. Do you have a motivating example for that? Also entirely possible I missed it in the paper
(I'll check out the new paper later - thank you for the link)
For those interested in the history of computing: the article mentions that the algorithm
"seems to have been discovered independently multiple times over the years". Interestingly, it also seems to have been discovered by Max Newman [1]
, who, at some point, was Alan Turing's supervisor. See [2, 3].
That's a nice overview of Hindley-Milner in practice!
For those interested, I recently have been thinking of a better way to specify type inference with principal derivations that lends itself better for type system extensions:
https://www.microsoft.com/en-us/research/uploads/prod/2024/0...
Still a bit preliminary but hopefully fun to read :-)
The man, the myth, the legend! Ok, so for extensible records: I don't have a good intuition for why the record objects would have to keep around the shadowed (hidden/duplicate) fields at run-time. Do you have a motivating example for that? Also entirely possible I missed it in the paper
(I'll check out the new paper later - thank you for the link)
For those interested in the history of computing: the article mentions that the algorithm "seems to have been discovered independently multiple times over the years". Interestingly, it also seems to have been discovered by Max Newman [1] , who, at some point, was Alan Turing's supervisor. See [2, 3].
[1] M. H. Newman, Stratified Systems Of Logic. https://www.classes.cs.uchicago.edu/archive/2007/spring/3200...
[2] J. R. Hindley, M. H. Newmans Typability Algorithm for Lambda-Calculus.
[3] H. Geuvers, Newmans Typability Algorithm. https://www.cs.ru.nl/~herman/computing2011.pdf
Max articles constitutes some ~90% of what I know about programming language implementation.
His Lisp series are often shared around, but the entire blog is jam packed with golden nuggets. Big fan.
I see bernsteinbear.com, I upvote.