You guessed pretty much right: ∀ is usually read as for all. It and others he uses (like ⊢ for is derived from) are defined in http://en.wikipedia.org/wiki/List_of_logic_symbols . Hope that helps; as a beginner in Haskell and strong type systems, it looks like I’m going to have trouble with this too.