Dependent Types

dependent_types.md

// Either is an example of a sum type.
enum Either<Left, Right>
{
    Ok(Right),
    Err(Left)
}

// Point is an example of a product type.
type Point = (i64, i64, String);

Why types at all?

F : X -> Subclasses(X)
where F: !Surjective

or in other words:

2 ≐ 4 ∈ Nat
2 ≐ 4 ∈ Nat mod 2

is not intrinsic, due to Gödel's incompleteness theorem.

To put it another way:

Fact: The class of all sets cannot be considered itself to be a set.

again:

The discovery of the undecidable propositions may have been motivated by a heuristic argument that it is unlikely that one can extend the completeness theorem of first-order logic to (the theory of) type theory."

Alonzo Church (paraphrased)

Dependent Sums: σ

type σ = bool :> Either<Success, Error>;

Dependent Products: π

type π = a, b, c 
       = Tuple a, b, c :: -> (a, b, c) 
       :> (a, ..));

Why is this useful?

The semantic differences between static types and dynamic values blur into a so-called phase distinction. The analysis of phase-distinction results in practical extensions to type theory, category theory, and mathematics broadly:

• Cost-aware logic: http://www.jonmsterling.com/agda-calf/
• Univalence: https://unimath.github.io/agda-unimath/