From that wikipedia page: "The untyped lambda calculus is Turing-complete, but many typed lambda calculi, including System F, are not."<p>Anyone have any details about System F not being turing complete? Is it not straightfoward to implement an untyped lambda calculus in a typed one?