DEPENDENT TYPES AND HOW TO GET RID OF THEM

Summary from the TLDR Dev newsletter

Dependent types are a programming language feature where types can depend on values, and the concept can be broken down into three ideas: functions returning types, input values determining output types, and tuple values influencing the types of other tuple elements. To optimize, compilers can erase values that are never used at runtime. Dependently typed languages often automatically identify and erase unused parameters.