I recently implemented a Hindley Milner type checker. The algorithm itself is not necessarily super difficult (once you get your head around it ofcourse) but the way it is explained is. It seems like HM is mostly explained by people with a mathematics background that already know the proper notation. I wonder how much overlap there is between people that know the notation and do not know how HM works, probably not much.
Anyway nice demo. Bi-directional is already quite powerful!
Or is that case simply not covered by this bare-bones example? I can't parse the code well enough just in my mind to tell if that would work, but I think it would work?
EDIT:
I just noticed the working demo at the bottom that includes an example of a multi-argument function so that answers whether it works.
Apparently it only gets away without annotations if the language doesn’t support subtyping? Here’s an explanation about why bidirectional type checking is better for that:
It seems to me that type-checking that relies on global constraint-solving is usually a bad idea. Annotated function types result in less confusion about what a function does.
I recently implemented a Hindley Milner type checker. The algorithm itself is not necessarily super difficult (once you get your head around it ofcourse) but the way it is explained is. It seems like HM is mostly explained by people with a mathematics background that already know the proper notation. I wonder how much overlap there is between people that know the notation and do not know how HM works, probably not much.
Anyway nice demo. Bi-directional is already quite powerful!
In the small example type checker given, would a function of type A -> B -> C be represented something like this?
Or is that case simply not covered by this bare-bones example? I can't parse the code well enough just in my mind to tell if that would work, but I think it would work?EDIT:
I just noticed the working demo at the bottom that includes an example of a multi-argument function so that answers whether it works.
I recently made a toy type checker for Python and had a lot of fun.
https://austinhenley.com/blog/babytypechecker.html
I grabbed the code from the article and annotated it with the different cases from the famous picture*
Looks like most of the hard work's done, and probably wouldn't be too tricky to get [Abs] in there too!* https://wikimedia.org/api/rest_v1/media/math/render/svg/10d6...
I thought the implementation here was how hindley Milner worked? I guess not?
No, HM is unification based and requires no annotations at all.
Apparently it only gets away without annotations if the language doesn’t support subtyping? Here’s an explanation about why bidirectional type checking is better for that:
https://www.haskellforall.com/2022/06/the-appeal-of-bidirect...
It seems to me that type-checking that relies on global constraint-solving is usually a bad idea. Annotated function types result in less confusion about what a function does.