PL iceberg

Email me ice (facts) to contribute! Or suggestions on what to link to, for the facts I have below!

Here's what I have so far (vaguely in order of increasing obscurity):

• Lambda calculus is just a helpful syntax for writing proofs
• Parallelism is not concurrency
• People have been saying "Single-core scaling/Moore's law is over, the future is parallel programming" since at least the 1980s.
• Functional programming has been the future since at least 1978.
• Datatypes (e.g. product and sum types) can be defined just by using functions.
• Your computer is a distributed system
• Message passing is faster than shared memory
• a ≤ b means "a implies b"
• Something about quines?
• C's void should be called unit, but at least they kept the same syntax for applying f to unit: f()
• The fixed point of option is the natural numbers.
• Functions are codata.
• Pattern matching exhaustiveness checking is NP-hard.
• Partial evaluation gives you compilers for free
• Exception handlers are just dynamically scoped continuations
• All IO is monadic
• Dynamic languages are static languages
• Logic, programs, and category theory are the computational trinity
• Inheritance was invented to support intrusive lists and simplify GC implementation relative to composition
• call/cc is the computational interpretation of Pierce's law. (equivalently, double-negation-elimination, or the law of excluded middle)
• Contrapositive is function composition.
• Contraposition is CPS translation.
• cut is process spawning, id is delegation/forwarding.
• Fork is the law of excluded middle, and all continuations are delimited
• Delimited continuations are *mumble* polarity *mumble*
• Typeclass resolution is proof search
• Some surprising interpretation of coinduction/codata?
• Some surprising interpretation of effect systems/effect polymorphism?
• Some surprising interpretation of modal types?
• Some surprising interpretation of substructural type systems?
• Network packets/encryption are just values of an extensible type (search "channels are nothing but dynamic classes")
• You can prove there's no closed form for the 3-body problem by reducing the halting problem to it
• Microkernels are an abstraction inversion
• A mechanized proof of type-safety (preservation and progress) is an interpreter.
• You can do garbage collection without tags
• Garbage collection is just type inference.
• Tracing GC and refcounting are the same thing
• You can make a compacting memory allocator without moving pointers.
• Primitive datatypes are actually highly sophisticated universe-polymorphic type theory constructs
• You can pretty print functions without their source code.
• All computable functions are continuous
• Function equality is decidable (at some types)
• Mustard watches were first theorized in 1990 by Girard