3 ms·
This definition of dependent type system is a bit controversial. There was a conflict between Julia language maintainers and FP researchers a few years back.
by zeckalpha 4y ago
This definition of dependent type system is a bit controversial. There was a conflict between Julia language maintainers and FP researchers a few years back.
- JonChesterfield 4y agoWell, sort of. There's the (dominant?) school of thought that believes that types encode a program that runs before your actual program runs (and may thus be deleted at some point). This is often characterized by writing the type in a more awkward language than the usual one, C++'s separate languages for example. Dependent Type Theory is quite strongly associated with the compiletime/runtime phase separation assumption, where the weirdness is that values from the runtime world leak into the compiletime one. This is magic in the static/AoT type world and trivial in the dynamic/JIT one. So, strictly you're right, python is not dependently typed, as that term is owned by a different branch. However if you were to put an ahead of time type system on arbitrary python, that would need to be dependently typed to be able to describe the programs people write in python today. It would also be prone to failing to terminate during type checking.