[HN Gopher] Damas-Hindley-Milner inference two ways
___________________________________________________________________
Damas-Hindley-Milner inference two ways
Author : todsacerdoti
Score : 118 points
Date : 2024-10-15 22:27 UTC (1 days ago)
(HTM) web link (bernsteinbear.com)
(TXT) w3m dump (bernsteinbear.com)
| fredrikholm wrote:
| 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.
| daanx wrote:
| 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 :-)
| tekknolagi wrote:
| 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)
| daanx wrote:
| Haha, thank you for your kind reply :) really enjoyed the
| blog post as it shows nicely that implementing HM can be
| straightforward -- many papers on inference are usually quite
| math heavy which can be a tough read.
|
| About duplicate labels.. one needs to retain the duplicate
| field at runtime _if_ there is a "remove_l" or "mask_l"
| operation that drops a field "l". For example,
| `{x=2,x=True}.remove_x.x` == `True`. (Where the type of
| `remove_l` is `{l:a|r} -> {r}`)
|
| This comes up with effect systems where we could have 2
| exception handlers in scope, and the current effect would be
| `<exn,exn>` (which corresponds to a runtime evidence vector
| `evn` of `[exn:h1,exn:h2]` where the h1,h2 point to the
| runtime exception handlers.). If a user raises an exception
| it'll select `evn.exn` and raise to `h1`. But a user can also
| "mask" the inner exception handler and raise directly to `h2`
| as well as `evn.mask_exn.exn`.
|
| One could design a system though with different primitives
| and not have a remove or mask operation, such that the
| duplicate fields do not have to be retained at runtime (I
| think).
|
| (Anyway, feel free to contact me if you'll like to discuss
| this more)
| GregarianChild wrote:
| 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
| johtela wrote:
| If you want to learn how HM typechecking works by studying
| working (Haskell) code, I would recommend the papers below. The
| code in these papers is closer to how you would actually
| implement a type checker in practice.
|
| [1]: https://www.microsoft.com/en-us/research/wp-
| content/uploads/...
|
| [2]: https://web.cecs.pdx.edu/~mpj/thih/thih.pdf
| winwang wrote:
| Dang! I was gonna (lol) write an HM-in-python post, also via my
| experiences at Recurse Center! In other news, great to see
| another Recurser :)
| JHonaker wrote:
| There's no reason you still can't!
| tekknolagi wrote:
| Please do! I would love to read it and link to it!
___________________________________________________________________
(page generated 2024-10-16 23:02 UTC)