I latex’d some notes while reading Dana N. Xu et al’s POPL’09 paper: Static contract checking for Haskell.