<div dir="ltr"><div><div><div>Eugene,<br><br></div>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.<br><br></div>Here's my code (which I suggest as something that's more concrete than notation you ovided):<br><br>```<br>{-# LANGUAGE DataKinds #-}<br>{-# LANGUAGE KindSignatures #-}<br>{-# LANGUAGE TypeFamilies #-}<br>{-# LANGUAGE TypeOperators #-}<br><br>module Main where<br><br>import GHC.TypeLits<br><br>newtype Nf (n::Nat) a = Nf a<br><br>-- TODO: add deepseq to ensure?<br>toNf :: a -> Nf 0 a<br>toNf = Nf<br><br>unNf :: Nf n a -> a<br>unNf (Nf x) = x<br><br>type family Max (n :: Nat) (m :: Nat) :: Nat<br>-- Implement properly later somehow<br>type instance Max 0 0 = 0<br>type instance Max 0 m = m<br>type instance Max n 0 = n<br>type instance Max 1 1 = 1<br><br>-- addition creates a thunk of `(max n m) + 1` depth<br>nfAdd :: (Num a) => Nf n a -> Nf m a -> Nf ((Max n m) + 1) a<br>nfAdd x y = Nf ((unNf x) + (unNf y))<br><br>-- TODO: think on this. Need infinity?<br>nfFold :: (Nf n1 a -> Nf n2 b -> Nf n3 b) -> Nf n4 b -> Nf n5 [a] -> Nf n6 b<br>nfFold _ acc (Nf []) = Nf (unNf acc)<br>nfFold f acc xs = undefined<br><br>main :: IO ()<br>main = do<br> let nfZero = (toNf 0)<br> nfTwo = (toNf 2)<br> printNf (nfAdd nfZero nfTwo<br> :: Nf 1 Int)<br> putStrLn "Hi!"<br> where<br> printNf = print . unNf<br>```<br><br></div>Is this is kind of thing you were talking about?<br><br>Thanks!<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Feb 20, 2015 at 7:26 AM, Eugene Kirpichov <span dir="ltr"><<a href="mailto:ekirpichov@gmail.com" target="_blank">ekirpichov@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><br><div class="gmail_quote"><span class="">On Tue Feb 17 2015 at 11:50:20 PM Roman Cheplyaka <<a href="mailto:roma@ro-che.info" target="_blank">roma@ro-che.info</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Note that foldr (+) 0 has nothing to do with laziness — it's eager. Its<br>
problem is that it's not tail-recursive.<br></blockquote></span><div>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).</div><div><br></div><div>I would like a type system that would disallow building thunks with *unbounded* whnf evaluation depth.</div><div><br></div><div>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@d" to denote "a value of type t requiring whnf evaluation depth d".</div><div><br></div><div>(+) :: forall (a:@) (b:@) . Int@a -> Int@b -> Int@(1+max(a,b));</div><div><br></div><div>($) :: forall (a:@) (b:@->@) . (forall (a:@) (b:@->@) . x@a -> y@(b a)) -> x@a -> y@(b a)</div><div><br></div><div><span style="font-size:13.1999998092651px">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.</span></div><div><span style="font-size:13.1999998092651px"><br></span></div><div><span style="font-size:13.1999998092651px">Some informal properties this would have:</span></div><div><span style="font-size:13.1999998092651px">* whnf depth of calling a function in a tailcall position is max(whnf depth of the function itself, whnf depth of its argument).</span></div><div><span style="font-size:13.1999998092651px">* whnf depth of "case x of { ... }" is 1.</span></div><div><span style="font-size:13.1999998092651px">* In the context of "case x of { ...(primitive pattern)... }", whnf depth of x is 0.</span></div><div><span style="font-size:13.1999998092651px"> </span><br></div><div><span style="font-size:13.1999998092651px">Does this make any sense?</span></div><span class=""><div><span style="font-size:13.1999998092651px"><br></span></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
foldl (+) 0 would be an example of a laziness issue.<br>
<br>
If you want to specify which functions should or shouldn't be used in a<br>
lazy context, take a look at polarity (see Harper's Practical<br>
Foundations for Programming Languages). So you could say, for instance,<br>
that it doesn't make sense to use + in a lazy context; that'd eliminate<br>
half the cases of laziness-induced memory leaks in practice.<br>
<br>
If instead you want to impose some upper bound on the memory consumption<br>
without caring about specific cases, then see this ICFP'12 paper:<br>
<a href="http://www.dcc.fc.up.pt/~pbv/AALazyExtended.pdf" target="_blank">http://www.dcc.fc.up.pt/~pbv/<u></u>AALazyExtended.pdf</a><br>
<br>
On 18/02/15 07:04, Eugene Kirpichov wrote:<br>
> Hello haskell-cafe,<br>
><br>
> Let me repost here a question I posted to cstheory stackexchange - in<br>
> hopes that there are more type theory experts here.<br>
><br>
> <a href="http://cstheory.stackexchange.com/questions/29518/type-systems-preventing-laziness-related-memory-leaks" target="_blank">http://cstheory.stackexchange.<u></u>com/questions/29518/type-<u></u>systems-preventing-laziness-<u></u>related-memory-leaks</a><br>
><br>
> Perhaps the main source of performance problems in Haskell is when a<br>
> program inadvertently builds up a thunk of unbounded depth - this causes<br>
> both a memory leak and a potential stack overflow when evaluating. The<br>
> classic example is defining sum = foldr (+) 0 in Haskell.<br>
><br>
> Are there any type systems which statically enforce lack of such thunks<br>
> in a program using a lazy language?<br>
><br>
> Seems like this should be on the same order of difficulty as proving<br>
> other static program properties using type system extensions, e.g. some<br>
> flavors of thread safety or memory safety.<br>
<br>
</blockquote></span></div></div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>