Tony Morris

i’m not sure I can explain my tweet in a single tweet, but the essence is that dependent types depend on some property of object in question

one standard form of dependent typing is being able to handle the notion of a dynamically sized array, carrying length in the type

having this information in the type, usually implies having this information available at compile time

‘at compile time’, i mean, some process you can run once, ahead of time, that will always complete yes the halting problem comes in here

anyway, having the length of an array as modelled thing within the types can let a compiler remove length checks or bounds checks

a similar thing happens in (some) static typed languages: the compiler has enough knowledge that it can omit instructions (for type checks)

(whoops canoe) anyway, going back to the joke

static type weenies love to pick on dynamic languages, or type checking at runtime the joke is “they are just as guilty of runtime checks”