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?
type-theory
functional-programming
dependent-types
inductive-datatypes
Dr. John A Zoidberg
fonte
fonte
Respostas:
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.
fonte