Reasoning when you have Static Types

Type systems, and more importantly, type checkers, are invaluable to how someone could go through understanding how any given codebase works. They might consider typing errors as guard rails as they start wrapping their mind around the expected computational outcomes of any given code block they are examining.

It is a stark contrast to the proposition of working without any obvious contracts, expectations, or local invariants as is more common in un-typed scenarios like javascript, ruby or pearl.

The explorations done under these guard rails, when computation can be cleanly connected to category theory, different type theories, and certain logics, gives predictive power beyond a few trial runs in someone’s head or on a typical repl session. For example the observation in this post by Isaac Elliott about how lambdas are codata types is a great example.

Completeness vs Soundness

It is true that type systems sacrifice a fundamental loss of expressiveness; as they fundamentally cannot cope with any arbitrary correct code block, e.g. when type checking a given self-interpreter. It is a non trivial choice to fail to check blocks that would otherwise run to completion if so allowed.

This choice all type systems make; to prioritize soundness over completeness, allows them to probe its connection to different logics, proof systems, and the study of composition. More than dictate a single approach there is an increasing multitude of them… for example, in the realm of type enrichment for usage tracking Idris is doing quantitative types, rust describes an alteration to linear types useful for borrow checking, and Haskell is attempting linearity of just the functions; these three approaches are, to a degree, incompatible and at odds with each other.

Emacs and the Wolfram ecosystem are great example of forgoing soundness instead of completeness, they are projects that have survived for decades, the first at the heart of open source, and the second as a commercial tour de force behind services like Siri and Cortana.

There is probable cause to enforce this connection computation has with our other techniques of reasoning? The reasoning power one wins, when they know their language is strongly normalizing is huge; for one; it is possible to understand meta programming as a structured layering of subsuming type universes as apposed to chaotic (in the genuinely unpredictable sense) self-interpretation.

Reducing False Negatives

What if the insistence on forgoing types; is that said argumentation purposefully or unknowingly got stuck on the halting problem. As if the discussion ends there and the power of self-interpretation is somehow unequivocally transcendental.

Why not, instead, focus on leveraging, understanding, and exploring notions like the calculus of construction and the lambda cube to peek and prod into the consequences, limitations, and further implications that Turing, Godel, and Russel started… If it is possible to have succinct libraries that extend proof theorems to its dependents; then that is code I want to use…

Incompleteness

By sacrificing completeness in order to regain soundness, type systems offer a slew of points to their benefit:

• Performance: no need for garbage collection, since you can track memory requirements as needed and run a plethora of optimizations leveraging all the metadata accompanying the types.
• Security: You get proofs for free, enforcing strong statements about the behavior of your programs
• Documentation: types record the intention of your code, contracts they meet, and effects they perform.
• Genericity: Without the guardrails of a type system, in practice developers given the freedom of dynamic types are timid (with due cause, since they lack the tooling support) in exploring polymorphism:
  parametric polymorphism, kind polymorphism, record (shape) polymorphism. Or more esoteric forms of polymorphism such as levity polymorphism
• Specificity: Types bind your code against contracts a compiler verified for you. An ideal type system should let you delimit your code to confirm and comply to the exact specification of your problem statement. For that we have devised:
  dependent type systems and multiple proof assistants,
  session types and a huge library of process calculi for distributed computing,
  quantitative types to maybe start combining dependent types with sessions types,
  homotopy type theory to piece out what we mean by equality…