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

5

Qual é a diferença entre idiomas tipados dependentes e idiomas como Spec # e Eiffel que permitem especificar "contratos" para funções em seu código para pré / pós-condições? A tipificação dependente é basicamente a versão puramente funcional dos "contratos" de Eiffel?

Pelo que entendi, idiomas com tipos dependentes permitem que você especifique a função de pré e pós condições usando a lógica de predicados como parte do tipo.

O conceito de contratos de Eiffel parece ser semelhante, mas baseado em programação imperativa, não em programação funcional.

    
por Nathan BeDell 22.02.2014 / 20:54
fonte

3 respostas

1

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.

    
por 23.02.2014 / 10:17
fonte
2

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.

    
por 23.02.2014 / 14:26
fonte
-5

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.

    
por 22.02.2014 / 21:21
fonte