카테고리 보관물: cstheory

cstheory

게으름 관련 메모리 누수를 방지하는 유형 시스템? 프로그램이 우연히 무한한 깊이의 덩어리를 쌓을 때입니다.

아마도 Haskell의 성능 문제의 주요 원인은 프로그램이 우연히 무한한 깊이의 덩어리를 쌓을 때입니다. 이는 평가할 때 메모리 누수와 잠재적 인 스택 오버플로를 유발합니다. 전형적인 예는 sum = foldr (+) 0Haskell에서 정의 됩니다.

게으른 언어를 사용하는 프로그램에서 그러한 썽크 부족을 정적으로 강제하는 유형 시스템이 있습니까?

이 방법은 유형 시스템 확장을 사용하는 다른 정적 프로그램 속성 (예 : 일부 스레드 안전성 또는 메모리 안전성)을 증명하는 것과 같은 난이도에 있어야합니다.



답변

푸시 가치 미적분에 의한 레비의 요구 는 가치와 썽크를 구별합니다. v유형 값 의 ty경우 계산 thunk v에는 유형이 U ty있습니다. CBPV에서 영감을 얻은 Lindley와 McBride의 Frank 언어는 Haskell과 달리 계산과 값의 차이를 명시 적으로 보여줍니다. Frank는 엄격합니다.


답변