Leibniz Talk

Jump to bottom Edit New page

Alexander Konovalov edited this page Jun 6, 2018 · 5 revisions

All the awesome things in alexknvl/leibniz.

Rough structure

Type inhabitation.
- Void.
- Inhabitation.
- Mere-propositions and bracket types.
Type equality and subtyping
- Type equality, inequality, subtyping, and strict subtyping.
- Variance and parametricity of type constructors.
- Axioms.
Decidable type equality.
- The problem with =!:=
- Concrete types & type ids.
- Inferring Covariant, Injective, Constant and much more.
"Quantified Contexts" in Scala.

If there is time:

As2 - As using existential types.
Universal and existential quantification.
Σ and Π types (sort of).