Readers with a background in the lambda calculus and functional programming can get an alternative first approximation of intuitionistic type theory by thinking about it as a typed functional programming language in the style of Haskell or one of the dialects of ML. However, it differs from these in two crucial aspects: (i) it has dependent types (see below) and (ii) all typable programs terminate. (Note that intuitionistic type theory has influenced recent extensions of Haskell with generalized algebraic datatypes which sometimes can play a similar role as inductively defined dependent types.)