Draft for submission to Haskell 2012 Dependently Typed Programming with Singletons Richard A. Eisenberg University of Pennsylvania Philadelphia, PA, USA eir@cis.upenn.edu Stephanie Weirich University of Pennsylvania Philadelphia, PA, USA sweirich@cis.upenn.edu Abstract Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limi