Type de systèmes empêchant les fuites de mémoire liées à la paresse?

La principale source de problèmes de performances dans Haskell est peut-être lorsqu'un programme crée par inadvertance un thunk d'une profondeur illimitée - cela provoque à la fois une fuite de mémoire et un débordement de pile potentiel lors de l'évaluation. L'exemple classique définit sum = foldr (+) 0dans Haskell.

Existe-t-il des systèmes de types qui imposent statiquement le manque de tels thunks dans un programme utilisant un langage paresseux?

Il semble que cela devrait être du même ordre de difficulté que de prouver d'autres propriétés de programme statiques en utilisant des extensions système de type, par exemple certaines versions de la sécurité des threads ou de la sécurité de la mémoire.

L' appel de Levy par calcul de valeurs push fait une distinction entre les valeurs et leurs thunks. Pour une valeur vde type, tyle calcul thunk va type U ty. Le langage Frank de Lindley et McBride , inspiré du CBPV, rend également explicite cette distinction entre les calculs et les valeurs, bien que contrairement à Haskell, Frank soit strict.