Blog posts tagged with
Erasing runtime irrelevant information while retaining the verification of dependent types.
This obscure class of polymorphism acts as an interesting replacement for subtyping.
What are Algebraic Data Types and what can we do with them?
What is type theory and how is it used?