The bigger challenge is doing the pattern matching and mainly the exhaustiveness checking of patterns which aren't constructors of a sum type, but for example i

The bigger challenge is doing the pattern matching and mainly the exhaustiveness checking of patterns which aren't constructors of a sum type, but for example integer intervals. Simon Peyton Jones together with others wrote a relatively easy to read book about the writing of Miranda (Haskell), which even includes a simple explanation of lambda calculus, so it includes everything you need to know about the theory, more or less: "The Implementation of Functional Programming Languages" 1987, https://www.microsoft.com/en-us/research/wp-content/uploads/1987/01/slpj-book-1987-small.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...