17 ms·
Hindley-Milner Type Inference (2012)
- 3001 6y agoLearnt this in my compiler class.It was the most brutal week of my life.
- jldugger 6y agoIMO, the most brutal week was realizing that nothing you will ever use on the job will use H-M type inference. Back to smashing rocks together.
- 3001 6y agoYou can go work for Jane street.
- nicoburns 6y agoPerhaps more achievable: iOS dev with Swift. Not technically HM I don't think, but it functions more or less the same.
- Klathmon 6y agoTake it from someone who has to occasionally work on an over complicated type system which uses HM inference, it ain't all that fun.
- AnimalMuppet 6y agoCould you be more specific? What makes it painful? (I mean, "overly complicated" is bad news no matter what the specifics of what we're talking about, but how does it cause pain when it's specifically in the types?)
- Klathmon 6y agoFor me personally it's just a lot of really heavy and very "meta" code that is really hard for me to reason about. I also touch it very rarely, so there's always a steep learning curve when I'm jumping back into it.
- GregarianChild 6y agoAlmost all modern statically typed languages use the ideas first coherently described in the Damas-Hindley-Milner approach. The main reason we do not see more full type inference, is that full type inference becomes uncomputable pretty quickly, once you move to more expressive typing systems.
- literallycancer 6y agoYou could use ReasonML in JS projects. It's even compatible with the rest of your codebase, if you don't want to start by rewriting everything.
- Kutta 6y agoThis tutorial seems to miss the level-based generalization optimization, which is crucial for production-strength HM inference. For, that you can look at: http://okmij.org/ftp/ML/generalization.html http://okmij.org/ftp/ML/generalization.html
- shpongled 6y agoLevel based generalization is a massive improvement in speed - I'm currently writing a Standard ML compiler for fun, and I saw a 30-50% decrease in elaboration type-checking duration when I switched to using levels. And it's not difficult at all to implement.
- nestorD 6y agoOcaml use Hindley-Milner type inference. I was taught programming with it and ended up deeply spoiled. I could not understand why most static language required writing so many types that were easy to deduce and why people where saying that not having to write types made dynamic language better. I can count on the finger of my hands the number of times when I needed to write explicit types in Ocaml (my single use case for explicit types in Ocaml was data deserialization). Plus, the compiler is fast.
- dwohnitmok 6y agoDoes the bytecode OCaml compiler compile faster than Go? What about Bucklescript? I've never experienced issues with OCaml compile times but I wonder how it compares against a widely acknowledged "fast" compiler.
- dropofwill 6y agoI think its safe to say it's fast in the general sense, the first time I compiled Revery I didn't believe that it had actually worked it was so fast. Just tried it again 0.98 secs to compile 20-25k lines of native OCaml/Reason. I'd be interested if anyone found/ran any benchmarks, though I thinks its pretty hard to write a fair compile time benchmark. I did a quick search and came across this post comparing solving the same problem with haskell/ocaml/go, which just kind of off hand mentions the compile times. OCaml versions range from 0.3-0.8s and Go was reported as ~1s. https://pl-rants.net/posts/haskell-vs-go-vs-ocaml-vs/ https://pl-rants.net/posts/haskell-vs-go-vs-ocaml-vs/
- dwohnitmok 6y agoIn that case maybe generics aren't a compile time killer. (Although I'm quite curious how the OCaml compiler compiles so quickly).
- shpongled 6y agoGenerics in the sense of C++ templates can be a compile time killer. However generics in the sense of HM type systems are basically just asking the compiler to fill in the type for you, which it has already figured out. HM type inference in general is ~O(n) (and exponential in the worst case, but you basically have to try to do that)
- ohazi 6y agoThe great thing about languages that implement HM types is that they allow you work as quickly or as carefully as you'd like without needing to change languages. If you've done something a million times before and are familiar with how it works, you can leave off all the type hints, and it'll figure them out for you and stay out of your way so that you can work more quickly. If you make a mistake somewhere, the compiler will still tell you. If you're doing something new, or don't quite understand something, you're free to add type hints wherever you need them to gain clarity. You can even do stuff like: let var: () = ...; if you have no idea what type something is and just want to ask the compiler for help. Once you're done, you can tidy up if you think it makes your code more readable. You can still leave top level hints to be kind to your coworkers or future you. I think the ability to dynamically shift between "cautious exploratory mode" and "reckless I-know-what-I'm-doing mode" at the drop of a hat is why you hear a lot of anecdotes about people using languages like OCaml or Rust as if they were scripting languages.
- CDSlice 6y agoTo expand on this, if you use CLion as your Rust IDE it will actually show you the types for all your variables automatically. For example, if you had a line like this: let foo = vec![1, 2, 3]; CLion would then show the type in a faded font where the type would go if you wrote it out manually like so: let foo: Vec<i32> = vec![1, 2, 3]; This is extremely useful when working with more complicated types such as iterator chain because it lets you see exactly what type everything is without having to manually write it all out and have the compiler check it.
- riquito 6y agoThat's available with VSCode and rust-analyzer too (but I suspect others that piggyback on rust-analyzer got that ability). It can get noisy fast, but you can toggle hints for when you need them
- frank2 6y agoHaskell, which uses a HM type system, has a type called Dynamic, which is described as follows: >Finally, dynamically typed programming in Haskell made easy! Tired of making data types in your Haskell programs just to read and manipulate basic JSON/CSV files? Tired of writing imports? Use dynamic, dynamically typed programming for Haskell! [1] If using an HM type system is really as easy and as fluid as you suggest, what purpose would be served by a type such as Haskell's Dynamic? Nor is Dynamic a panacea: to use it requires a lot of extra typing (er, extra keypresses) IIRC, and >A Dynamic may only represent a monomorphic value; an attempt to create a value of type Dynamic from a polymorphically-typed expression will result in an ambiguity error (see toDyn). [2] 1: https://hackage.haskell.org/package/dynamic https://hackage.haskell.org/package/dynamic 2: https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-Dynamic.html#t:Dynamic https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-...
- fizixer 6y agoI'm starting to understand why HMTI, and OCaml/Haskell et. al., struggle from such obscurity despite its fanboys swearing by it. The problem is that it's a crap technology in both easy mode and hard mode. - easy mode: beginners just want to learn how to program as quickly as possible, something like python is fantastic for that. And the side-benefit, you can do amazing stuff with it, like bypass whole of symbolic AI of 80s and 90s (including HMTI, OCaml/Haskell) and go straight to deep learning, BERT, GPT what not. - hard mode: mathematicians would love a helpful computing system that'll make them more productive mathematicians. When they attempt to explore stuff like Coq, and HoTT etc, the first thing that's thrown at their face is that they have to give up law of excluded middle, non-constructive logic and what not. I'm sorry but the tail does not wag the dog. If your theorem assistants and checkers require the mathematicians to turn their world upside down, most won't give a rat's ass about what you have to say about propositions-as-types and programs-as-proofs. There is a medium mode, or shall we say mediocre mode, whereby you fall in love with type-theory and type-based languages, you want to live in your own bubble and not be bothered by what's happening in the outside world. And that's were the users of these systems live.
- nullc 6y agoThis would be an interesting statement of an opinion if the language were toned down a little bit from flame-broiled mode to medium well. You took all this time to write out your thoughts, why not put a little extra effort into massaging them in a way that will maximize their impact rather than just turning people off with flame-bait?
- dependenttypes 6y agoI do not get it. HM lets you do things like f x = fold g x without writing the types, how is that not easy mode compared to C or Java for example?
- WJW 6y agoIt's easy mode when writing, not when reading.
- hellofunk 6y agoOne of the principal maintainers of the Racket language once gave a talk, I think it was at the main Clojure conference, on a topic about Typed Racket, where he strongly outlined the reasons why HM inference is a bad idea. It was interesting to hear these differences in philosophies.
- tommybu 6y agoWould you mind providing a link to this talk?
- hellofunk 6y agoI've been searching for a few minutes and can't find it -- it was several years ago, maybe at least 5 years, and at one of the Clojure conferences (there used to be several big Clojure conferences each year back in the language's golden age, but now there's 0 - 1 per year), and I can't remember which conference.
- andrekandre 6y agowas it this one? https://www.youtube.com/watch?v=RvHYr79RxrQ https://www.youtube.com/watch?v=RvHYr79RxrQ
- hellofunk 6y agoThat looks interesting as well, but it’s not the talk I was thinking of.
- FPreallyHurts 6y agoI had to implement this in Haskell while in university, we started with an interpreter for a Scheme-like language, then added static typing and inference. Parser combinators, monads, monad transformers, curry-howard. Think for 15 minutes, write 5 lines of code, repeat. What I remember is that was code was really elegant but brain hurt so much.
- mcbuilder 6y agoEventually you program enough FP, and then imperative starts to hurt your brain. Programming is much like a muscle. As your program in one paradigm, you brain starts to reason that way, then switch paradigms and you're suddenly struck with a bunch of programming atrophy.
- DaiPlusPlus 6y agoImperative doesn’t hurt my brain, but because many operations in FP are generally much more succinct and expressive than in an imperative style - writing in imperative instead just makes me groan about all the manual keyboard-typing I’ll have to do (e.g. Linq vs foreach). I really wish I could do more FP, but the languages and libraries I use for my day-job aren’t as-accommodating (mostly C#) - while C# has some FP features, it’s really held-back by the CLR’s type-system - so until that fundamental plumbing gets done we’ll never see features like type-classes, true immutable types, algebraic-types, and so on. Without those features we’ll have to keep on writing more code than is necessary. <digress>Heck, it’s bad enough that IDictionary doesn’t implement IReadOnlyDictionary - or that none of the IReadOnly* types make any guarantees about immutability, which means having to review documentation or disassembly in ILSpy. And the famed non-nullable-reference-types in C# 8.0 is actually all just syntactic sugar for yet more attributes rather than true code-contracts, a built-in Option type, or extending the CLR’s type-system to understand nullability. Grumble.</digress>
- Multicomp 6y ago> while C# has some FP features....we’ll never see features like type-classes, true immutable types, algebraic-types, and so on. IIRC you just described some features of F#, excepting type classes. Or at least F# gets you closer to the goal. Maybe the ever elusive F* has that stuff?
- recursivedoubts 6y agoLocal type inference can give you 90% of the benefit at a fraction of the cost of a global type inference system. Simply introducing local variable inference probably captures 50+% of that and it's the simplest programming trick I ever saw. When I first came across it in the gosu code base (https://gosu-lang.github.io https://gosu-lang.github.io) I said: "Wait. That's all you do? You just take the type from the right hand side and then put it on the left hand side?" "Yep." "That's type inference?" "Yep." It called into question many aspects of my computer science education.
- cheerlessbog 6y agoWould it help with this case? https://news.ycombinator.com/item?id=23777197 https://news.ycombinator.com/item?id=23777197
- cultus 6y agoI've been really enamored of bidirectional type systems [0] lately, which seem to really give the best of all worlds. They explicitly separate inference from type checking, with the type checker switching between both modes during checking/inference. It's also more syntax directed, which makes good error messages easy. A pure HM type-system is pretty restrictive, so most ML family languages don't have global type inference anyway. [0] https://arxiv.org/pdf/1908.05839.pdf https://arxiv.org/pdf/1908.05839.pdf
- shpongled 6y agoYea bidirectional systems are nice - one of the big benefits is that you can also have polymorphic function arguments, something you can't do in standard HM. I recently implemented the bidirectional system in Rust from the paper you linked, it was fun (and a challenge!) [0] https://bit.ly/2W96K2r https://bit.ly/2W96K2r
- cultus 6y agoWow! Very cool!
- 6y ago
- DanielBMarkham 6y agoI code both ways simultaneously. I'm interested in what types I need to solve my business problem. The rest of it, I don't care. The reason I care about the types I need for my business problem is that I don't want my code doing something that it shouldn't: DDD-style coding allows me to code in such a way that it's impossible for the program to exist in a state that's invalid. That's a great time-saver. Other than that, polymorphic coding FTW.
- atrudeau 6y agoWhy is Damas dropped when referring to HM type inference? Not being critical, just genuinely curious. I imagine there's a good reason.
- dang 6y agoI put 2012 as an upper bound on the year above: https://web.archive.org/web/20120324053910/http://www.ian-grant.net/hm/ https://web.archive.org/web/20120324053910/http://www.ian-gr.... Perhaps it is earlier?
- somewhereoutth 6y agoIf my understanding is correct, type inference producing a set of possible types - instead of a single type - for each term has proven to be undecidable? This is a shame, because sum types (e.g. Shape := Circle U Square U Triangle) are actually pretty useful, and languages such as Java ended up implementing them via class or interface inheritance. Languages often also required type coercion to deal with things like 0.2 + 5, otherwise + could have had a type signature like: float U int -> float U int -> float U int.
- marcosdumay 6y agoIf my understanding is correct, yes, it's undecidable. On practice nobody cares. It being undecidable just means you need an extra check at your compiler to verify the types are converging, and a new error for the problematic case.
- siraben 6y agoOne of my favorite resources that develop the HM algorithm from scratch is Ben Lynn's[0], who treats it like a series of interview questions, because really type inference algorithms match up two trees into constraints, which can contain concrete types or type variables, then solves those constraints. [0] https://crypto.stanford.edu/~blynn/lambda/hm.html https://crypto.stanford.edu/~blynn/lambda/hm.html
- vyuh 6y agoThe algorithm, the type system, and some of the logical background are explained in this tutorial, along with an implementation in standard ML. http://steshaw.org/hm/hindley-milner.pdf http://steshaw.org/hm/hindley-milner.pdf I found this 30 page PDF document very helpful in understanding the Algorithm.
- yawaramin 6y agoThis may be my favourite explanation of the algorithm's logic: https://stackoverflow.com/a/42034379/20371 https://stackoverflow.com/a/42034379/20371