Playing With Pointers

I recently had occasion to screw around Haskell's type system. The end goal was to produce a Tic-tac-toe game in which all type-correct moves are legal and where all illegal moves produce type errors. I decided call the following moves illegal attempts to move on a cell already occupied attempts to make a move on [...]

I studied a proof today that I had been putting off for some time now; that a simply typed lambda calculus is normalizing -- every well-typed expression eventually reduces to a value. The proof is quite clever and that the exact wording of the proof in Types and Programming Languages is a bit terse so [...]