Sobre o que são linguagens estaticamente tipadas eu já estou ciente, mas o conceito de linguagem dependentemente tipada é novo para mim.
Creio que tem a ver com algo chamado tipos dependentes, mas também não sei o que são.
- O que são tipos dependentes?
- Uma linguagem dependentemente tipada seja aquela que possui a feature de tipos dependente? Ou há algo a mais?
- Toda linguagem com tipos dependentes deve ser, necessariamente, estaticamente tipada?