[Haskell-cafe] Type systems preventing laziness-related memory leaks?

[Konstantine Rybnikov]

Eugene,

I find your idea quite interesting. One thing that I'd say is that since
you don't know how many recursive calls will foldr do at runtime, you can't
say at compile-time it's thunk depth. Thus, I think, if you would be able
to express something that is similar to type-level `Nat`, which could also
be `Infinity` (e.g., either it's a known nat or an infinity), you could do
something like that.

Here's my code (which I suggest as something that's more concrete than
notation you ovided):

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import GHC.TypeLits

newtype Nf (n::Nat) a = Nf a

-- TODO: add deepseq to ensure?
toNf :: a -> Nf 0 a
toNf = Nf

unNf :: Nf n a -> a
unNf (Nf x) = x

type family Max (n :: Nat) (m :: Nat) :: Nat
-- Implement properly later somehow
type instance Max 0 0 = 0
type instance Max 0 m = m
type instance Max n 0 = n
type instance Max 1 1 = 1

-- addition creates a thunk of `(max n m) + 1` depth
nfAdd :: (Num a) => Nf n a -> Nf m a -> Nf ((Max n m) + 1) a
nfAdd x y = Nf ((unNf x) + (unNf y))

-- TODO: think on this. Need infinity?
nfFold :: (Nf n1 a -> Nf n2 b -> Nf n3 b) -> Nf n4 b -> Nf n5 [a] -> Nf n6 b
nfFold _ acc (Nf []) = Nf (unNf acc)
nfFold f acc xs = undefined

main :: IO ()
main = do
    let nfZero = (toNf 0)
        nfTwo = (toNf 2)
    printNf (nfAdd nfZero nfTwo
               :: Nf 1 Int)
    putStrLn "Hi!"
  where
    printNf = print . unNf
```

Is this is kind of thing you were talking about?

Thanks!

On Fri, Feb 20, 2015 at 7:26 AM, Eugene Kirpichov <ekirpichov at gmail.com>
wrote:

>
>
> On Tue Feb 17 2015 at 11:50:20 PM Roman Cheplyaka <roma at ro-che.info>
> wrote:
>
>> Note that foldr (+) 0 has nothing to do with laziness — it's eager. Its
>> problem is that it's not tail-recursive.
>>
> The problem is that when you say foldr (+) 0 [1, 2, 3, 4, 5] you build a
> thunk "1 + (2 + (3 + (4 + (5 + 0))))", which has - let's call it "whnf
> evaluation depth" of 4 (you need a stack of size 4 to evaluate it to whnf).
>
> I would like a type system that would disallow building thunks with
> *unbounded* whnf evaluation depth.
>
> I'm thinking we could annotate every type in every type signature with
> this depth. Let us use a special kind "@" for these annotations, allow
> polymorphism on them, and use "t at d" to denote "a value of type t
> requiring whnf evaluation depth d".
>
> (+) :: forall (a:@) (b:@) . Int at a -> Int at b -> Int@(1+max(a,b));
>
> ($) :: forall (a:@) (b:@->@) . (forall (a:@) (b:@->@) . x at a -> y@(b a))
> -> x at a -> y@(b a)
>
> The type signature for (.) quickly gets unwieldy and I wasn't able to even
> write down the signature for foldr :) but perhaps you get the idea.
>
> Some informal properties this would have:
> * whnf depth of calling a function in a tailcall position is max(whnf
> depth of the function itself, whnf depth of its argument).
> * whnf depth of "case x of { ... }" is 1.
> * In the context of "case x of { ...(primitive pattern)... }", whnf depth
> of x is 0.
>
> Does this make any sense?
>
>
>> foldl (+) 0 would be an example of a laziness issue.
>>
>> If you want to specify which functions should or shouldn't be used in a
>> lazy context, take a look at polarity (see Harper's Practical
>> Foundations for Programming Languages). So you could say, for instance,
>> that it doesn't make sense to use + in a lazy context; that'd eliminate
>> half the cases of laziness-induced memory leaks in practice.
>>
>> If instead you want to impose some upper bound on the memory consumption
>> without caring about specific cases, then see this ICFP'12 paper:
>> http://www.dcc.fc.up.pt/~pbv/AALazyExtended.pdf
>>
>> On 18/02/15 07:04, Eugene Kirpichov wrote:
>> > Hello haskell-cafe,
>> >
>> > Let me repost here a question I posted to cstheory stackexchange - in
>> > hopes that there are more type theory experts here.
>> >
>> > http://cstheory.stackexchange.com/questions/29518/type-
>> systems-preventing-laziness-related-memory-leaks
>> >
>> > Perhaps the main source of performance problems in Haskell is when a
>> > program inadvertently builds up a thunk of unbounded depth - this causes
>> > both a memory leak and a potential stack overflow when evaluating. The
>> > classic example is defining sum = foldr (+) 0 in Haskell.
>> >
>> > Are there any type systems which statically enforce lack of such thunks
>> > in a program using a lazy language?
>> >
>> > Seems like this should be on the same order of difficulty as proving
>> > other static program properties using type system extensions, e.g. some
>> > flavors of thread safety or memory safety.
>>
>>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150220/e95a8e40/attachment.html>