As propriedades, como o uso de memória de uma função, podem ser expressas em um idioma digitado de forma dependente?

11

Suponha que alguém queira raciocinar sobre propriedades do código além de coisas como totalidade e pureza funcional - também se preocupa com o consumo de memória ou com a complexidade algorítmica de uma função. Isso pode ser feito através de sistemas de digitação e efeitos dependentes?

Dr. John A Zoidberg
fonte
2
Neste vídeo, Brian McKenna fornece um exemplo de codificação da complexidade do tempo em tipos.
Anton Trunov

Respostas:

8

Sim pode. Embora conceitualmente não seja tão difícil, não foi estudado muito. Um aspecto do campo é a semântica de custos, como a pesquisa realizada por Guy Blelloch .

Na veia do vídeo mencionado por Anton, está o trabalho de Daniellson em Análise de complexidade de tempo semiformal leve para estruturas de dados puramente funcionais . Isso realmente usa uma mônada para suportar um custo por operação. Uma mônada semelhante, no nível semântico, é usada na semântica de custo denotacional para linguagens funcionais com tipos indutivos . Aqui está um artigo de 2016 fazendo algo semelhante em Coq, uma biblioteca Coq para verificação interna dos tempos de execução .

O pessoal da NuPRL também se interessou por fazer coisas assim. Em Expressando a complexidade computacional na teoria do tipo construtivo , que basicamente equivale ao cálculo sobre uma semântica operacional estruturada. Onde fica um pouco mais interessante é que você pode refletir a semântica do idioma no idioma. O exemplo na seção final, seção 12, da Teoria do tipo computacional ingênuo ilustra e discute esse tipo de coisa.

Derek Elkins deixou o SE
fonte