Hindley-Milner Inference is Not-That-Good (Kind-Of)

 Egel doesn't have a type checker,  the two major reasons for that was that I a) wanted to explore the operational model and types are overhead on that endeavour, and b) type systems are hard to get right and easy to get wrong. Of course, I am also thinking about what will come after Egel, and that'll be a typed functional language bootstrapped with the interpreter.

But there's a separate reason I didn't want to immediately dive into a typed language, and that is that I find Hindley-Milner based type inferers lacking for programming languages. (If there's such a thing, you can tweak everything into something like a HM-type system description.)

The reason for that is that HM influences towards a particular style of reasoning. Reading T-Lam, from top to bottom, you can see it as an algorithmic description of: when I know this and that entails that then I can conclude that .. That's bottom-up reasoning, often touted as a major accomplishment. Clear, concise, syntax-driven, and all that. Also, good for teaching. In essence, it is the formula for creating an inductive proof.

However, for those who have studied typing of imperative languages ostensibly derived from Algol, you'll notice that that isn't exactly how their type algorithms work. Principally, in an imperative language you usually reason along with what you know: while proving the equivalence of two types you may encounter (other) type equivalences and postulate those as knowns, and -in the end- use those postulates to finish the argument. That's a bisimulation proof.

However, HM-inferencers can be abused to construct bisimulation proofs once you declare the type of a term since it'll happily reason along with user-supplied postulates. But HM style based inferencers often aren't good at creating or deriving bisimilar types per se; which I actually encountered in real-life situations using GHC or Ocaml.

It's awkward to realize that most faculty are teaching students inductive type systems whereas all type algorithms used in industry construct bisimulation proofs. I don't think current HM based inferencers are even that good -though you can tweak everything- for a programming language, and subsequently, I want to implement a functional language with a type system that derives bisimilar types.