Тип системы, предотвращающей утечки памяти, связанные с ленью?

10

Возможно, основным источником проблем с производительностью в Haskell является случай, когда программа по неосторожности создает поток неограниченной глубины - это вызывает как утечку памяти, так и потенциальное переполнение стека при оценке. Классический пример - определение sum = foldr (+) 0в Haskell.

Существуют ли системы типов, которые статически навязывают отсутствие таких кодов в программе, использующей ленивый язык?

Похоже, что это должно быть того же уровня сложности, что и при проверке других статических свойств программы с использованием расширений системы типов, например, некоторых разновидностей безопасности потоков или памяти.

jkff
источник

Ответы:

4

Вызов Леви методом исчисления push- различий делает различие между ценностями и их принципами. Для значения vтипа tyвычисление thunk vимеет тип U ty. Язык Фрэнка Линдли и Макбрайда , вдохновленный CBPV, также делает это различие между вычислениями и значениями явным, хотя, в отличие от Хаскелла, Фрэнк строг.

Доминик Маллиган
источник