News for hackers. Stuff that matters.
Re:Where do type systems come from? (2017) by ashton314 on Friday October 01, 2021 @02:10AM (#28715201)
Here's a small attempted answer:

Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Even some programs that may converge have no type. The Y Combinator, for instance, has no type because it would require an infinite type.

From the Wikipedia article under "General Observations":

    Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a λ  abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = (λx.x x) (λx.x x) . Recursion can be added to the language by either having a special operator fixₐ of type (α → α) → α or adding general recursive types, though both eliminate strong normalization.

    Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete.
Another way to look at it is this via the Curry-Howard correspondence [^2]: for any mathematical proof, you can write down a program that is equivalent to that proof. Verifying the proof's result is the same as running the program. This is a very exciting correspondence that runs deep throughout computer science and mathematics. (I highly recommend the Software Foundations course I linked to below.)

Writing a non-terminating program is like writing one of these self-contradictory logic statements: it has no proof of truth or falsehood. Thus, the fact that we can write programs to which we can assign some kind of type but that never terminate is a way of demonstrating the fact that there are theorems that are well-formed but have no truth assignment to them. (Gödel's Incompleteness Theorem)

[^1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-curren...

[^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Re:Where do type systems come from? (2017) by the_french on Friday October 01, 2021 @08:10AM (#28717407)
> Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs.

Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus

Re:Where do type systems come from? (2017) by ashton314 on Friday October 01, 2021 @10:19AM (#28718760)
You’re right. My bad. Thanks!
Re:Where do type systems come from? (2017) by barrenko on Friday October 01, 2021 @03:56AM (#28715811)
Can I ask in a very "noob" way - are types and theory underneath something that runs in parallel to Turing machine and they together enable modern computing OR is Turing completeness and Turing machine stuff also part of type / lambda calculus theory?

Thanks.

Re:Where do type systems come from? (2017) by reuben364 on Friday October 01, 2021 @04:31AM (#28715994)
Semantics of programs in type theory are most of the time described by a small step relation which describes, possibly non-deterministically, how to perform one step of computation. Separately one can consider which terms are values, indicating a successful, terminating computation. Type theory would then involve proving properties about the semantics of typed programs.

One can give a small step relation for a Turing machine and one could possibly come up for a type system for it, but generally one starts with the semantics for untyped lambda calculus.

Some of the more advanced type theory stuff unifies the notions of terms and types, meaning arbitrary computations can happen in type checking and so properties about types can involve properties about computation in general.

Re:Where do type systems come from? (2017) by reuben364 on Friday October 01, 2021 @03:33AM (#28715681)
I'm struggling to fit this into my current understanding. I guess I don't really know how incompleteness looks in a type theory setting. Terms are proofs, types are propositions. _ are theories, _ are models, _ are valid formulas?