A well-typed program is isomorphic to a proof -- google "propositions as types". This is not the same as saying your program is correct. For your specific ques

A well-typed program is isomorphic to a proof -- google "propositions as types". This is not the same as saying your program is correct. For your specific question, google "dependent types", which are types that depend on a value. In your case, Haskell can type check positive integers: http://mvanier.livejournal.com/3820.html http://mvanier.livejournal.com/3820.html