5

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?
0

1 Resposta 1

4

O que são tipos dependentes?

É o tipo que depende do seu valor e não apenas da qualificação geral do que cabe ali.

O exemplo mais típico é o tipo que permite estabelecer uma faixa de valores permitidos.

Linguagens funcionais acabam usando isso implicitamente já que não costumam ter controle de fluxo imperativo para tomar decisões sob certos valores, então o valor influi no polimorfismo ad-hoc, isso é uma forma de tipo dependente (ou pelo menos pode ser), mas que não entra no sistema de tipagem.

Outro exemplo comum são os tipos algébricos que possuem um tipo interno que depende do tipo principal, portanto um valor do objeto determina a segunda parte do tipo.

O mais interessante é quando você coloca no tipo o que ele pode aceitar (é parecido com genéricos, mas que aceita um argumento com valor em vez de só um tipo):

type BoundedInt(n) = {i : Int | i <= n}

Coloquei no GitHub para referência futura.

Sem os dependent types você teria que escrever o código que verifica se está dentro da faixa estabelecida em todo lugar que usa esse tipo.

Na teoria eles são o suprassumo da robustez. Na prática eles complicam muito a linguagem, em todos os sentidos, e poucas linguagens adotam, em geral as funcionais adotam por quererem mais rigor matemático. E por isso as linguagens que adotam costumam receber o apuro de que seus códigos depois de compilados estão sempre certos (exceto erro de lógica). Claro, à custa de muita dor de cabeça até compilar.

Uma linguagem dependentemente tipada seja aquela que possui a feature de tipos dependente? Ou há algo a mais?

Acredito que podemos classificar assim, basta ter essa feature, pelo menos não vejo nada que difira disso. Só entenda que não precisa toda a tipagem ser dependente.

Toda linguagem com tipos dependentes deve ser, necessariamente, estaticamente tipada?

Uma linguagem de tipagem dinâmica poderia ter tipos dependentes para os valores, mas não para variáveis. Então não faz muito sentido. Tipos dependentes são usados para dar mais robustez para aplicações, reforçar contratos de forma mais estrita, ou seja, faz menos sentido usar em linguagens dinâmicas (quem sabe PHP adote :P eu não podia perder essa :D) que não prezam muito por isso e muitas nem possuem sintaxe para expressar isso de forma adequada. E deve dar trabalho fazer isso certo nesse tipo de linguagem.

Você deve fazer log-in para responder a esta pergunta.

Esta não é a resposta que você está procurando? Pesquise outras perguntas com a tag .