Idris: Dependent Types
Types that depend on values — type-level programming as first-class Idris
Vect n a
Fin n
Matrix m n
Effects
Proofs