A reckless introduction to Hindley-Milner type inference (2019)
Hindley-Milner type inference balances expressiveness and legibility in programming languages like Elm and Haskell. It enhances correctness by enforcing strict type checking, limiting coding practices for improved type safety.
Read original article
This text discusses Hindley-Milner type inference, a method used in programming languages to infer types without explicit annotations. The author explores the trade-off between expressiveness and legibility in programming languages, using examples like regular expressions, SQL, and Coq. Hindley-Milner systems, as seen in languages like Elm and Haskell, offer strong type inference capabilities, reducing runtime errors and enhancing program correctness. However, they require adhering to certain programming patterns that the type inference algorithms can handle, limiting some coding practices for the sake of type safety. The text highlights how languages like Elm enforce stricter type checking, leading to more robust programs but potentially restricting certain coding techniques common in dynamically typed languages like Python. Overall, Hindley-Milner type systems provide a balance between expressiveness and legibility, offering a powerful tool for ensuring program correctness at the cost of some coding flexibility.
Related
My experience crafting an interpreter with Rust (2021)
Manuel Cerón details creating an interpreter with Rust, transitioning from Clojure. Leveraging Rust's safety features, he faced challenges with closures and classes, optimizing code for performance while balancing safety.
Own Constant Folder in C/C++
Neil Henning discusses precision issues in clang when using the sqrtps intrinsic with -ffast-math, suggesting inline assembly for instruction selection. He introduces a workaround using __builtin_constant_p for constant folding optimization, enhancing code efficiency.
Why are module implementation and signatures separated in OCaml? (2018)
Separation of module implementation and signatures in OCaml enables scalable builds, creation of cmi files, and streamlined interface modifications. Emphasizing abstraction and implementation separation enhances modular programming and system reasoning.
Elixir Gotchas
The article highlights common pitfalls in Elixir programming, including confusion between charlists and strings, differences in pattern matching, struct behavior, accessing struct fields, handling keyword lists, and unique data type comparisons.
Deriving Dependently-Typed OOP from First Principles
The paper delves into the expression problem in programming, comparing extensibility in functional and object-oriented paradigms. It introduces dependently-typed object-oriented programming, emphasizing duality and showcasing transformations. Additional appendices are included for OOPSLA 2024.
4 commentsProving that a program terminates eventually is a very weak guarantee, since it could be a program that terminates after a million years. This matters mostly for proof languages, where it’s useful to write proofs about functions that you never run. If the function provably terminates, you can assume that whatever value it returns exists, without calculating it.
For a possibly long-running job like a SQL query, a static guarantee that it terminates eventually is almost certainly not what you want. You’re going to need to test its performance, and ideally have a timeout and a way of handling the timeout. If you want to get fancy, a progress bar and cancel button might be nice.
Edit:
Compilers need to run fast for the programs we actually write. A type system that possibly doesn’t terminate under unusual conditions isn’t that big a deal, as long as people don’t write code like that. Hopefully you get a decent error message.
Compare with memory use. We don’t want compilers to use excessive amounts of memory, but don’t need static guarantees about memory use.
The intro here flags that the author i) is not happy with the post in its current form, ii) was resynthesized from wikipedia "without particularly putting in the effort to check my own understanding", which doesn't inspire confidence.
And then when you do get into the content, stuff looks incorrect, but a non-expert reader, given the caveats in the intro, should be on the lookout for errors but isn't equipped to identify them with confidence. E.g. the very first inference rule included is described as:
> if you have a variable x declared to have some polytype π, and if the monotype μ is a specialisation of π, then x can be judged to have type μ
... but I think this should be "π is a specialization of μ".
Basically, I think this is the kind of material where detail matters, where errors seriously impede understanding, and a resource where the reader/learner has to be on guard second-guessing the author is a bad intro resource. But surely there are better ones out there.
From the article:
> HM type systems can't implement heterogenous lists [...] > [well it does when wrapping the elements in a sum type, but then] > it can only accept types you know about in advance. > [which makes it] a massive pain to work with.
Sorry, I totally disagree... Heterogeneous lists without the sum types are a massive pain! Maybe it is easier for the initial development effort, but if you need to maintain code with heterogeneous lists (or dynamically typed code in general) the pain will come at some point and likely when already in production.
I much rather fix compile errors than runtime errors. And a massive thanks to Hindley and Milner for advancing type systems!
Found their photos in gratitude just now:
Related
My experience crafting an interpreter with Rust (2021)
Manuel Cerón details creating an interpreter with Rust, transitioning from Clojure. Leveraging Rust's safety features, he faced challenges with closures and classes, optimizing code for performance while balancing safety.
Own Constant Folder in C/C++
Neil Henning discusses precision issues in clang when using the sqrtps intrinsic with -ffast-math, suggesting inline assembly for instruction selection. He introduces a workaround using __builtin_constant_p for constant folding optimization, enhancing code efficiency.
Why are module implementation and signatures separated in OCaml? (2018)
Separation of module implementation and signatures in OCaml enables scalable builds, creation of cmi files, and streamlined interface modifications. Emphasizing abstraction and implementation separation enhances modular programming and system reasoning.
Elixir Gotchas
The article highlights common pitfalls in Elixir programming, including confusion between charlists and strings, differences in pattern matching, struct behavior, accessing struct fields, handling keyword lists, and unique data type comparisons.
Deriving Dependently-Typed OOP from First Principles
The paper delves into the expression problem in programming, comparing extensibility in functional and object-oriented paradigms. It introduces dependently-typed object-oriented programming, emphasizing duality and showcasing transformations. Additional appendices are included for OOPSLA 2024.