Jeremy W. Sherman: A dependent type is a type that depends, not just on other types, but on terms. This means you can have values – plain old data – in your types. A common example is that of length-indexed lists. You likely caught on that that code is Swift-ish but not actually Swift. That’s … Continue reading Why Dependent Types Matter