Czy właściwości, takie jak wykorzystanie pamięci przez funkcję, można wyrazić w języku zależnym od typu?

Załóżmy, że ktoś chce argumentować o właściwościach kodu wykraczających poza takie rzeczy, jak totalność i czystość funkcjonalna - dba się również o zużycie pamięci lub złożoność algorytmiczną funkcji. Czy można tego dokonać za pomocą zależnych systemów pisania i efektów?

Tak, może. Choć koncepcyjnie nie jest to takie trudne, nie było tak wiele badań. Jednym z aspektów tej dziedziny jest semantyka kosztów, na przykład badania przeprowadzone przez Guy Blelloch .

W tym filmie Anton wspomniał o pracy Daniellsona w lekkiej analizie złożoności czasu półformalnego dla czysto funkcjonalnych struktur danych . To rzeczywiście używa monady do przenoszenia kosztu na operację. Podobna monada na poziomie semantycznym jest używana w semantyce kosztów denotacyjnych dla języków funkcjonalnych z typami indukcyjnymi . Oto artykuł z 2016 r., Który robi coś podobnego w Coq, Bibliotece Coqa do wewnętrznej weryfikacji czasów pracy .

Ludzie NuPRL od dawna są zainteresowani robieniem takich rzeczy. W wyrażaniu złożoności obliczeniowej w teorii typów konstrukcyjnych , co w zasadzie sprowadza się do obliczania na podstawie ustrukturyzowanej semantyki operacyjnej. Bardziej interesujące staje się to, że możesz odzwierciedlić semantykę języka w języku. Przykład w końcowej sekcji, sekcja 12, naiwnej teorii typów obliczeniowych ilustruje i omawia tego rodzaju rzeczy.