Qual é a diferença entre digitação dependente e contratos?

A digitação dependente (Full) permite que você escreva expressões arbitrárias no nível de tipo incluindo aquelas que, em uma linguagem mais "mainstream", seriam exclusivas do nível de valor. Isso permite que você escreva pré e pós-condições com verificação de tipo para suas funções, mas apenas como um caso especial de poder escrever qualquer coisa que você goste .

Por outro lado, "contratos" só pode fazer uma verificação muito específica, ao contrário de verificar literalmente qualquer coisa que você possa conceber (contanto que seja computável).

Os chamados "tipos de refinamento" estão em algum lugar entre os dois.

Uma diferença importante que não foi explicitamente mencionada até agora, é que os tipos dependentes são verificados no tempo de verificação do tipo (duh!), ou seja, estaticamente, antes do tempo de execução. Contratos Eiffel são verificados dinamicamente, em tempo de execução. Spec # cai em algum lugar entre: contratos são verificados dinamicamente, em tempo de execução, mas você pode obter um provador de teoremas que pode (tentar) provar (alguns) contratos estaticamente, antes do tempo de execução.

Os contratos devem sempre ser expressos de maneira funcional e livre de efeitos. Eles são agnósticos quanto à linguagem como tal. Existem bibliotecas e extensões de contrato para idiomas como scheme, java, c # e haskell. Eles são muito expressivos, mas raramente são verificados estaticamente.

Os tipos dependentes, por outro lado, costumam ser menos expressivos e, até onde eu saiba, sempre verificados estaticamente.

Meu ponto com este post é rejeitar a noção de que os contratos são limitados a linguagens imperativas.