[HN Gopher] How the OCaml type checker works (2022)
___________________________________________________________________
How the OCaml type checker works (2022)
Author : mooreds
Score : 149 points
Date : 2024-08-18 10:52 UTC (12 hours ago)
(HTM) web link (okmij.org)
(TXT) w3m dump (okmij.org)
| eska wrote:
| OT: how come there are so many OCaml posts recently? Genuinely
| curious!
| kinow wrote:
| I don't know if there's any reason like a project, derived
| language, or some new feature. But there are always posts and
| comments about OCalm at
| https://old.reddit.com/r/functionalprogramming/. So it's not
| really a surprise to me that it gets some waves of posts every
| now and then.
| pieix wrote:
| OCaml is the one language I've used whose standard library is
| great to read. It's a very developer-friendly language but in
| all of the ways that make it popular on HN and rarely used in
| the real world.
| mattarm wrote:
| Some popular streamers have dabbled in OCaml this year,
| sometimes calling it "the Go of functional programming", which
| probably set off a small wave of people tinkering with the
| language. OCaml has also gotten gradually better in recent
| years in terms of tooling, documentation, standard library,
| etc.
| adambrod wrote:
| I think they were saying that Gleam was Go of functional
| programming? OCaml may be like Go compared to Haskell but
| IMHO Gleam really embraces simplicity and pragmatism.
| myaccountonhn wrote:
| I would say some other reasons OCaml is similar to Go is
| that the runtime is very simple, performance is on par and
| the compilation times are very fast. It also markets itself
| as a GC'd systems language similar to Go. I think a
| seasoned OCaml would be able to guess the generated
| assembler code.
|
| I suspect that Gleam is quite different in that regard.
| fire_lake wrote:
| Before OCaml multi core it was a non starter for many
| applications. Now, OCaml can be used for almost anything!
| adambrod wrote:
| I really rooting for the Riot framework. It's based on the
| actor model and makes using multi core in OCaml a breeze.
| _flux wrote:
| Well its feature list seems positively delightful:
| https://github.com/riot-ml/riot !
|
| Basically, it seems, it's Erlang for OCaml. Hot reloading
| would be a cool feature, though, but I can see why it's not
| implemented, at least not yet.. I recall the OCaml native
| toplevel is able to load code in dynamically, so that could
| be the mechanism to do it.
|
| It seems to use open types for handling messages (per just
| looking at https://github.com/riot-
| ml/riot/tree/main/examples/3-message...) reducing the
| benefits of exhaustiveness checking, but it still seems
| rather interesting!
| sporkl wrote:
| Anecdotally, I feel like OCaml is growing in popularity,
| probably due to ecosystem improvements. Stuff like dune and
| other OCaml Platform tools becoming mature, multicore support,
| recently first-class Windows support, etc.
| ericjmorey wrote:
| OCAML on Windows was such a pain several years back. It's
| good to hear that they've improved on it.
| myaccountonhn wrote:
| I also suspect that people are more open to a language like
| OCaml. With Rust and javascript being so popular, a lot of
| constructs in OCaml will not seem so foreign.
|
| OCaml is in many ways a sane Typescript or a functional
| version of Go.
| adambrod wrote:
| Ditto, it feels like more people are coming around to the
| ML style type systems. I'm hoping Gleam will fill the void
| with a scalable BEAM backend and compiling to JS with
| Lustre on the frontend (or even just serverside with htmx).
| carapace wrote:
| It feels like we're (IT, hackers, et. al.) finally growing up.
| incognito124 wrote:
| Before opening the article, my first thought was "wdym, it's HM
| and Algorithm W"
|
| The very first sentence was: > There is more to Hindley-Milner
| type inference than the Algorithm W.
|
| I guess congratulations to the author for knowing the audience
| well enough
| 082349872349872 wrote:
| The subtitle, "or what polymorphism and garbage collection have
| in common", is another hint there may be more to TFA than its
| HN submission title indicates.
| Drup wrote:
| That remark is actually more interesting than you think. As
| groundbreaking as it was, algorithm W iss far too slow for non-
| toy languages. All modern HM languages (that I know of) use
| some form of union-find trickeries, as pioneered by the one
| presented in the blog post (but also present in resolution-by-
| constraints approaches employed by Haskell and Scala).
|
| So, in fact, it's actually never algorithm W in non-toy
| languages. ;)
|
| Side note: this article is originally from 2013 and is
| considered a must-read by any would-be hackers trying to modify
| the OCaml typechecker (it's cited in the documentation).
| lupire wrote:
| The Wikipedia articles claims that W is efficient, but only
| for a core language without highly desirable features like
| recursion, polymorphism, and subtyping.
|
| https://en.m.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_.
| ..
| Rusky wrote:
| In fact, those union-find trickeries come from the _same_
| paper that presented algorithm W, where they were named
| algorithm J. W was known from the start to be more useful for
| proofs than implementation:
|
| > As it stands, W is hardly an efficient algorithm;
| substitutions are applied too often. It was formulated to aid
| the proof of soundness. We now present a simpler algorithm J
| which simulates W in a precise sense.
|
| https://doi.org/10.1016/0022-0000(78)90014-4
| lupire wrote:
| Title should say (2013) not (2022)
| escape_key wrote:
| Is says "Last updated January 9, 2022" at the bottom of the
| page. But I guess the article is about the type checker version
| of February 2013?
| deredede wrote:
| This was updated in 2022 but was indeed written and
| originally published in 2013.
| bbminner wrote:
| A complete novice question: I think I remember reading that Rust
| is moving from one of the standard type checking algorithms (this
| one?) to general purpose Z3 SMT for speed. Does type checking
| happen to have the same complexity as SMT? Or Z3 is just so
| insanely well optimized with heuristics and all that it happens
| to give better overall performance then problem specific checking
| algorithms with better theoretical performance (eg this one)?
| deredede wrote:
| I think you remember wrong. Rust is moving towards using a
| datalog engine, but for lifetime resolution (the project is
| called Polonius), not for type checking. Datalog engines have
| some similarities with SMT solvers so this might be what you're
| thinking of.
| Rusky wrote:
| The Polonius rules were formulated using Datalog, but the
| implementation that will ship in rustc does not use Datalog:
| https://blog.rust-lang.org/inside-
| rust/2023/10/06/polonius-u...
| SkiFire13 wrote:
| The implementation based on the datalog engine was also found
| to be generally too slow and was replaced with an ad-hoc
| dataflow algorithm.
| jahewson wrote:
| Having built a type checker with Z3 in the past, the simple
| answer to "does type checking happen to have the same
| complexity as SMT?" is no. That's because the "T" in SMT,
| "theories" can be pretty much anything - they're essentially
| plugins.
|
| A more nuanced answer is that many problems are reducible to
| SAT, meaning that the answer can technically be yes, but a type
| checker that simply prints the message "UNSAT" upon failure
| isn't very useful!
| RandomThoughts3 wrote:
| Unification is at the heart of type checking and unification is
| doable with a SMT solver. So a SMT solver can be a type checker
| if you want which should show that SMT is indeed much more
| complex than type checking.
| kccqzy wrote:
| > OCaml generalization is based on tracking of so-called levels
| of a type.
|
| The level tracking reminds me of a recent paper exploring
| SimpleSub[0], a simpler alternative of adding subtyping to ML-
| style type systems. It also gets rid of the algorithm W's
| repeated generalization (introducing foralls and turning a type
| into a polytype) and instantiation (changing the universally
| quantified type variables to fresh type variables). They have
| slightly different operations on levels, e.g. extrude. I wonder
| if this level tracking is independently invented again.
|
| [0]: https://dl.acm.org/doi/pdf/10.1145/3409006
| deredede wrote:
| Not independently invented again. Lionel is fully aware of the
| level tracking in the OCaml type-checker; in fact the OP is
| cited in the Simple-sub paper (section 3.5.1, page 15).
| nj5rq wrote:
| Say whatever you want, but this is how websites should be
| designed.
___________________________________________________________________
(page generated 2024-08-18 23:00 UTC)