Ever since their inception lambda calculus and type theory have been such an influence in the design of modern programming languages so much so that even programming lan guages outside of the functional circle have adopted ...