Why Dependent Types Matter: http://www.cs.nott.ac.uk/%7Etxa/publ/ydtm.pdf
increase expressiveness:
http://www.seas.upenn.edu/%7Esweirich/ssgip/main.pdf