The new Disciple Core language

It's been a while since updates. The last one was in August, and after that I got distracted with ICFP. When I got back I spent more time doing Coq proofs, finishing with Progress and Preservation for a version of SystemF2 with mutable algebraic data. The proofs are here. All data is allocated into the store (heap), and there are primitive functions to update it. In this language you can, say, destructively update a list so that the tail points to different physical data. This language doesn't have effect typing, but after this proof I felt like I had crossed the line from "Coq-shy" to "Coq-sure".

In early November I read about ciu-equivalence, and how to prove contextual equivalence of program transformations. Thinking ahead, it felt like time to cleanup the sponginess in the existing DDC core language, because I'd need to do this before trying to formalise it. Although the plain calculus has a proper semantics and a hand-done soundness proof, the actual core language as used in the compiler also has some half-baked hacks. The reviewers of a previous paper had made suggestions about how to cleanup other aspects of the core calculus, and having Coqified all those languages, I now understand why it was good advice.

Cutting to the chase, I've redesigned the DDC core language and there is an interpreter that works well enough to evaluate simple recursive functions. Here is an example:

  letrec {
   ack    [r1 r2 r3: %] 
          (m : Int r1) {!0 | Use r1 + Use r2 + Use r3}
          (n : Int r2) { Read r1 + Read r2 + Alloc r3
                       | Use r1  + Use r2  + Use r3}
          : Int r3
    = letregion r4 in
      let zero = 0 [r4] () in
      let one  = 1 [r4] () in
      case eqInt [:r1 r4 r4:] m zero of {
          1 -> addInt [:r2 r4 r3:] n one;
          _ -> case eqInt [:r2 r4 r4:] n zero of {
                  1 -> ack [:r4 r4 r3:] 
                           (subInt [:r1 r4 r4:] m one) 
                           (1 [r4] ());

                  _ -> ack [:r4 r4 r3:] 
                           (subInt [:r1 r4 r4:] m one)
                           (ack [:r1 r4 r4:] m (subInt [:r2 r4 r4:] n one));
          }
    }
  } in ack [:R0# R0# R0#:] (2 [R0#] ()) (3 [R0#] ());;

Here is another example that does destructive update of an integer:

  letregion r1 with {w1 : Mutable r1} in
  let x : Int r1 = 0 [r1] () in
  let _ : Unit   = updateInt [:r1 r1:] < w1 > x (2 [r1] ()) in
  addInt [:r1 r1 R2#:] x (3 [r1] ());;

and one that suspends the allocation of an integer with lazy evaluation:

  letregion r1 with { w1 : Const r1; w2 : Lazy r1; w3 : Global r1 } in
  let x : Int r1 lazy < w2 > 
     = purify < alloc [r1] w1 >  in
       forget < use [r1] w3 w1 > in
       2 [r1] () 
  in addInt [:r1 R0# R0#:] x (3 [R0#] ());;

Note that this is an intermediate representation for a compiler, and has vastly more type information than a real user would want to write. The compiler will perform type inference on the source language, and automatically translate the user program to this lower level language.

The new DDC core language is described on the wiki and so far I've been reasonably good at keeping the wiki up to date with what's implemented.

The main changes are:

• Witnesses now exist in their own universe, at level 0 next to values. Both values and witnesses are classified by types, and types classified by kinds. This removes the dependent-kinding of the old language. The more I thought about it, the less fun formalising a dependently kinded language seemed to be.
  
  
• I've removed the more-than constraints on effect and closure variables. The type inference algorithm I am using returns constraints on effect and closure variables, so I had added similar constraints to the core language. This was a bad idea because managing the additional subsumption judgements during core type checking is a headache. The new core language has no such constraints, and I think I know to process the output of the inferencer so I won't need them.
  
  
• Introducing lazy evaluation is now done with the let .. lazy binding form instead of a primitive suspend operator. This goes hand-in-hand with the purify and forget keywords that mask the effect and closure of their body respectively. These two keywords are akin to the type casts used by SystemFc and the GHC core language to support GADTs. I think it makes more sense to mask out the effect of an expression before suspending it, than to pass a witness as to why it's pure. The former style will still be used in the source program because that's how the type inferencer works, but the latter should be easier to work with in the core language.
  

Anyway, if you darcs get the DDC repo you can make bin/ddci-core to build the interpreter. Run the examples like bin/ddci-core test/ddci-core/30-Eval/30-Letrec/Test.dcx. It's not completely finished, but all the examples under the test/ddci-core directory run fine.

The interpreter should be done in another couple of weeks. After that it'll be time to split off the LLVM backend from the existing compiler so that we can compile core programs directly.

How I learned to stop worrying and love de Bruijn indices

When I started learning how to formalise languages in Coq, one of my initial stumbling blocks was choosing an approach to name binding. There are at least three fancy sounding contenders: Locally Nameless, Nominal Reasoning and Parametric Higher Order Abstract Syntax. Of course, you could also use good old de Bruijn indices, but proponents of fancy approaches warn about the large volume of lemmas regarding lifting and substitution you'll need to prove before you can start the "real work".

Back in April I scratched around for about two weeks reading up on all the different approaches, trying to identify the "best" one (whatever that means). Then I read the following comment by Xavier Leroy on the POPLmark website. He had used the Locally Nameless approach, but had stated: "If the purpose is just to solve the challenge and be done with it, I would rather go for pure de Bruijn". That was enough to convince me to stop worrying and just get into it. I've spent about 250 hours now doing my own proofs, and I can report that using de Bruijn isn't really that bad. Yes, you need to prove some lemmas about lifting and substitution, but my entire response to naysayers is summed up henceforth: "The only computational operation that lambda calculus has is substitution, so don't pretend you can get away without proving something about it." Corollary: HOAS doesn't count.

The Lemmas

You need to know what the lemmas are though, and I advise cribbing them from someone else's proof. I learned them from Arthur Charguéraud's proof, but I don't know where they are from originally. You're more than welcome to copy them from mine.

Once you know what the lemmas are, and how they work in STLC, extending them to new languages is straightforward. For reference, the following are the definitions of the lifting and substitution operators for STLC. Note that if you just want to prove Progress and Preservation for STLC, you don't actually need the lemmas. They're needed in bigger languages such as SystemF2 to show that type substitution is commutative. Nevertheless, for illustrative purposes we'll just stick with STLC expressions.

Inductive exp : Type :=
 | XVar  : nat -> exp
 | XLam  : ty  -> exp -> exp
 | XApp  : exp -> exp -> exp.

Fixpoint 
 liftX  (d:  nat) (* current binding depth in expression *)
        (xx: exp) (* expression containing references to lift *)
        : exp
 := match xx with 
    |  XVar ix    
    => if le_gt_dec d ix
        (* Index is referencing the env, so lift it across the new elem *)
        then XVar (S ix)

        (* Index is locally bound in the expression itself, and 
           not the environment, so we don't need to change it. *)
        else xx

    (* Increase the current depth as we move across a lambda. *)
    |  XLam t1 x1
    => XLam t1 (liftX (S d) x1)

    |  XApp x1 x2
    => XApp   (liftX d x1) (liftX d x2)
    end.

Fixpoint
 substX (d:  nat) (* current binding depth in expression *)
        (u:  exp) (* new expression to substitute *)
        (xx: exp) (* expression to substitute into *)
        : exp 
 := match xx with
    | XVar ix 
    => match nat_compare ix d with
       (* Index matches the one we are substituting for. *)
       | Eq  => u
       
       (* Index was free in the original expression.
          As we've removed the outermost binder, also decrease this
          index by one. *)
       | Gt  => XVar (ix - 1)

       (* Index was bound in the original expression. *)
       | Lt  => XVar ix
       end

    (* Increase the depth as we move across a lambda. *)
    |  XLam t1 x2
    => XLam t1 (substX (S d) (liftX 0 u) x2)

    |  XApp x1 x2 
    => XApp (substX d u x1) (substX d u x2)
 end. 

Drawing the deBruijn environment

Here is a nice lemma to get started.

Lemma lift_lift
 :  forall n m t
 ,  lift n              (lift (n + m) t) 
 =  lift (1 + (n + m)) (lift n t).

This is one of the lemmas you need for proving commutativity of substitution. Although it looks complicated at first glance, it will make significantly more sense when you know how to draw it.

First, consider the standard typing judgement form:

Env |- Exp :: Type

Assume there are de Bruijn indices in the expression. Some of these indices point to lambdas in the expression itself, corresponding to locally bound variables, while some point to lambdas in the environment, corresponding to free variables. Here is an example:



Suppose I apply (lift 2) to the above expression. Although it would be helpful for educational purposes to do this directly using the definition of 'lift' above (try it!), I'll tell you the shortcut instead. Firstly, if we assume that the definition of 'lift' is correct, none of the bound indices will be changed during the application. Ignoring bound indices, the only ones remaining are free indices. These are the indices that point into the environment.

Now, although applying 'lift' to an expression may increment these free indices, instead of thinking about indices being incremented, it's easier to think about environment elements being shifted. I'll explain what I mean by that in a moment, but for now let's just do it...

Here is the same expression as before, with the environment positions numbered in blue:


Shifting the elements after position two yields the following:



In the above diagram I've used '_' to represent a hole in the environment. This is a place where I could insert a new element, and be guaranteed that none of the indices in the expression point to this new element. This in turn means that if I apply (lift 2) to the expression, then insert a new element into the hole, then the resulting judgement is guaranteed to give me the same type as before (t5 in this case).

Of course, applying 'lift' to the expression doesn't actually change the environment. In this example I've moved 't1' and 't2' to the left for illustrative purposes, but this is an operation separate from applying 'lift' to the expression itself. However, applying 'lift' does changes the indices, and these indices are pointers into the environment. If we like, we could instead think about moving the pointers (the arrow heads) instead of the actual environment elements. This is an important change in perspective. Instead of thinking about 'lift' as incrementing indices in the expression, we want to think about 'lift' as shifting environment pointers to the left.


Let's look at our lemma again:

Lemma lift_lift
 :  forall n m t
 ,  lift m              (lift (n + m) t) 
 =  lift (1 + (n + m)) (lift n t).

As 't' is quantified, we need to prove this for all possible terms 't'. Using our change in perspective, this also means that we want to prove the lemma for all possible sets of environment pointers. Given the environment pointers for 't', the expression '(lift (n + m) t)' transforms them into a new set (by adding a hole at position n + m). Likewise the expression 'lift (1 + (n + m)) (lift n t)' transforms the environment pointers of 't' by adding a hole a position 'n', and then adding another hole at position '1 + (n + m)'. Here is a picture of the full situation. I've just drawn the contiguous set of environment pointers as rectangles, with the holes are marked in grey.

In the first line we have set of environment pointers for 't'. Applying 'lift n' adds a hole a position 'n'. Alternatively, applying 'lift (n + m)' adds a hole at position '(n + m)'. Given 'lift n t', if we add another hole at (1 + n + m) we get the last set shown. Likewise, if we take the set 'lift (n + m) t' and add a hole at position 'n' then we also get the last line.

That's it. That complicated looking lemma above can be drawn with a few rectangles, and provided the definition of 'lift' does what it's supposed to, the lemma is obviously true. For a language like SystemF2 you need about 5 lemmas concerning lifting and substitution. They're all easy to draw, and the proofs are straightforward once you understand the general approach. In the next post I'll show how to draw substitution, which works in a similar way.

Proofs and mutual recursion

Quick update. I'm still working on mechanising the proofs for the DDC core language in Coq. So far I've made it through Progress, Preservation and the correspondence between Big and Small step semantics for Simply Typed Lambda Calculus (STLC), System-F, System-F2, and PCF. Extending the STLC proof with polymorphism and fixpoints etc was surprisingly straightforward. It only took about 4 hours each to create the other versions of the proof.

The next qualitative hurdle appears to be handling the mutual recursion that arises when we extend the language in other ways. To add case expressions, I need to represent case alternatives. Case alternatives contain expressions, and expressions contain (lists of) alternatives.

Unfortunately, with mutually recursive definitions, it appears that Coq can't automatically generate all the induction schemes I need. I could be wrong on this though, as I'm still a Coq newbie. I've figured out that the Coq command "Combined Schemes", will make some of the schemes I might want, but it doesn't cover all of the use-cases. The problem (I think) is that although expressions are defined in terms of lists of alternatives, the lists themselves are polymorphic and aren't directly defined in terms of alternatives. For this reason, I can't convince "Combined Scheme" to make me a strong enough induction scheme, so I must write down and prove this myself.

At least, that's what I'm inferring from reading the proof of soundness for the STG machine described in a paper by Maciej Pirog and Dariusz Biernacki. I'm still working through it.

Falling down the naming well

Over the last month or so I've started to formalise the proofs of the DDC core language in Coq. The existing proofs were just getting too big to manage by hand, and typing them all up in Latex was seeming like a less and less fun thing to do.

Being a Coq-newbie I started with Benjamin Pierce and co's Software Foundations course notes. I had done a couple of pages of Coq tutorial before, but never tried to use it for anything real. I've found the course notes to provide a fairly smooth ride, though I got antsy during the IMP formalisation and skipped straight to the lambda calculus one. After about two weeks of evenings I was able to redo the simply typed lambda calculus (STLC) one by myself, but hit a wall trying to scale up to System-F. To cut a longer story short, I've come to appreciate (along with many others) what a massive hack capture avoiding substitution is.

I'm fast moving towards the viewpoint that the deBruijn and/or locally nameless representation is actually the "real" lambda calculus, whereas named binders are just a layer of syntactic sugar that confuses everything (and gives you cavities). I've ended up just settling on vanilla deBruijn indices for further work, mainly because the examples I've seen so far using the locally nameless representation rely on a heavy amount of Coq Ltac magic that I don't understand yet. I'm also more than willing to trade time for cleverness. By that I mean I'm willing to commit more time for a less clever solution, provided I know that the approach I take will get the job done and I won't have to start all over again using a different formalisation of binders.

Underneath all of this is an itch in my mind saying that I was already writing a perfectly good paper about the DDC core language, and I don't want to start another one right now about "How to formalise DDC Core in Coq". Anyway, I've made it through Progress and Preservation for STLC using the deBruijn representation, including all the list lemmas, and am feeling fairly good about it so far. The proofs are in the main DDC tree at http://code.ouroborus.net/ddc/ddc-head/proof/.

Real Time Edge Detection in Haskell

Last week we submitted a paper to ICFP about how to implement efficient parallel stencil convolutions in Haskell. This goes along with a new release of Repa that runs on GHC 7.0.3. We've extended the old array representation to support the partitioning of arrays into several regions, and rewritten the back-end to recover sharing between the computation of adjacent array elements. Coupled with a careful management of aliasing issues, this lets us implement image processing algorithms that have comparable performance to OpenCV.

Absolute performance depends on what data format we're using. Using Word8s is about 4 times slower than OpenCV because it uses SIMD intrinsics that we don't have access to from Haskell (yet!). On the other hand, using Float32s and 2 Haskell threads can run faster than single threaded OpenCV, as the parallelism makes up for the lack of SIMD instructions.

Here is a video of me demonstrating a Canny edge detector applied to a stream captured from my iSight camera. The demo uses Objective C for the GUI, and Haskell for the processing. The source builds with XCode 3.2.1 and GHC 7.0.3, though you'll need to update and run the CONFIGURE.sh script in the root dir to point it to your GHC install. There are also prebuilt versions with the GHC "+RTS -N" option baked in for two, four and six threads. They all do the same thing apart from the number of threads. You can change the RTS options in the main.m module if you want to rebuild it. On my 4-Core i7 desktop it does about 20 frames per second with no problem -- the framerate from the iSight is set dynamically by OSX depending on system load. I've tested it on 3 separate machines, but let me know if it doesn't work for you. Non-Mac users can run the edge detector over .bmp files, using the repa-canny program from repa-examples.

Papers, Proofs, PrimOps, Allocation and Strengthening

Papers
General status update: I got the reviews back for the paper I submitted to JFP on the DDC core language. The reviews were very helpful, and a huge thank you to the reviewers if you're reading this. I will endeavour to make all my own reviews as helpful.

The bottom line was the paper looked promising, but needs more motivation for the language design, and more meta-theory. The motivation is easy enough to 'port across from my thesis, so this part shouldn't take too long. For background, the JFP paper is an extension of the APLAS 2009 paper I wrote just after I finished my thesis. The original version of that paper had more motivational material, but I ended up cutting it to fit the page limit. For the JFP paper I tried to stick to the details of the core language, but I suppose not discussing the source language and wider context makes it hard to see the point of it all. There were also suggestions and questions as to the details of the language and typing rules, which I'll either fold in or explain why.

Proofs
For the meta-theory, the paper needs proofs of observational equivalence for the example optimisations, showing how the witnesses are used during optimisation. I had a proof of soundness for the type system in the appendix, and worked examples of the optimisations, but not formal proofs that the optimisations are ok. Said optimisations are just standard ones like let floating and full-laziness, but I agree that if the point of having witnesses of purity and constancy in the core language is to perform optimisations in the presence of side-effects, then we want some formal link between the witnesses and those optimisations.

Anyway, I started on the proofs over the christmas break, and have the structure of one showing that let-floating is sound (changing the order of let-bindings with non-interferring effects), though I still need to fill in some details. I'm estimating about two or three weeks work (full time equivalent) to finish the proofs and update the paper.

PrimOps
I went to a hackathon hosted by Erik last week where we worked on LLVM support for DDC. Erik's written all the code for the backend, though to push it all the way through I needed to change how primops are handled in the rest of the compiler (which is explained in Erik's blog post). I just finished that this afternoon, so we're gunning for full LLVM support in the near future. The primop handling is pretty clean now, so if we wanted to, say, add support for vector operations like MMX and SSE then this should be reasonably straightforward.

Allocation Effects
The paper reviews have also convinced me that we want explicit allocation effects in the source and core languages. One of my thesis reviewers also suggested this, though so far I've left them out because they weren't absolutely needed. Allocation effects have a slightly different flavour to world effects (like writing to the Console) and to read/writing mutable data. When two expressions have world or read/write effects then this means they can interfere in such a way that you cannot change the order of these two expressions. In contrast, you can always change the order of expressions that just allocate new objects.

However, if an expression allocates new mutable objects, then you cannot hoist it out of a lambda (apply the full-laziness transform). Hoisting an expression means it is potentially executed less often, so we're not just changing the order of two actions in time. If you want to do hoisting without information about allocation, then it's sufficient to check that the binding to be hoisted performs no world or read/write effects, and does not return mutable data. However, using allocation effects will make this reasoning clearer, and can enable more optimisations later, so I'll add them in. I started on a branch that has them, but now I've convinced myself they're easy enough to add I'm going to leave the hacking to later and focus on getting the paper finished first.

Strengthening
In the type inferencer, it turns out that strengthening more-than constraints to equality constraints during inference breaks programs that use interesting higher order functions (like with parser combinators). This isn't a problem with standard 2nd order functions like map, fold, filter etc, but only appears with 3rd order functions and higher, or with data containing functions, which is why I hadn't noticed it before. By "break" I mean the inferencer returns a bad type, so we get a panic when we try to type check the corresponding core program. We still want to do the strengthening because it removes the need for a pile of redundant effect applications in the core programs, but it should be done while converting the desugared language to core, instead of during inference, which is fairly obvious in hindsight. I've started fixing this as well, but need to adjust the type utils (like type simplification and effect masking) so they'll handle the non-strengthened forms. Another job to be left until after the paper is finished...

Shootout: Fannkuch redux

A few times after finishing some GHC hacking, I've been talking to Simon Marlow and mentioned that whatever it was I was doing now "works".
Usually, his reply is then "for what value of works?". Especially with compilers, there is quite a gap between "sorta works", "seems to work" and "industrial strength".

Last night I was taking a stroll through the "sorta" end of town while hacking on a Disciple version of the fannkuch-redux program from the languages benchmarks game. Disciple is a dialect of Haskell, so I started with one of the nicer existing Haskell versions.

Here is the version by Miha Vučkovič. I've reformatted it a bit and used the Disciple string pasting operator % instead of the (hated) Haskell ++, but it's otherwise the same program. (I've also added a type sig because DDC doesn't do dictionary passing yet, and used iterateL, but more on that later.)

flop (2:x1:t)                   = x1:2:t
flop (3:x1:x2:t)                = x2:x1:3:t
flop (4:x1:x2:x3:t)             = x3:x2:x1:4:t
flop (5:x1:x2:x3:x4:t)          = x4:x3:x2:x1:5:t
flop (6:x1:x2:x3:x4:x5:t)       = x5:x4:x3:x2:x1:6:t
flop (7:x1:x2:x3:x4:x5:x6:t)    = x6:x5:x4:x3:x2:x1:7:t

flop lst@(h:_) = r
 where flop' 0 (t, r)          = (t, r)
       flop' n ((h:t), r)      = flop' (n-1) (t, h:r)
       (t, r)                  = flop' h (lst, t)
 
flopS (1:_)  = 0
flopS lst    = 1 + flopS (flop lst)

rotate n (h:t)         = rotate' (n-1) t 
 where rotate' 0 l     = h:l
       rotate' n (f:t) = f:(rotate' (n-1) t)

checksum :: Int -> Int -> Int
checksum i f
   | mod i 2 == 0 = f
   | True         = -f

pfold :: (Int, Int) -> [(Int, Int)] -> (Int, Int)
pfold r [] = r
pfold (ac, af) ((c, f):t)  = pfold (sc, sf) t 
 where  sc = ac+c
        sf = max af f

permut n          = foldr perm [[1..n]] [2..n] 
 where perm x lst = concat [take x $ iterateL (rotate x) l | l <- lst]

main () 
 = do n = 8
      (chksm, mflops) 
            = pfold (0,0) 
            $ map (\(i, p) -> let flops = flopS p 
                              in  (checksum i flops, flops))
            $ zip [0..] (permut n)

 putStr $ show chksm % "\nPfannkuchen(" % show n % ") = " % show mflops % "\n"

It doesn't matter what it does, or how it does it. Check the shootout page if you're interested, we're just trying to get it running for now.

Faking value recursion

My first compile attempt reported:

desire:ddc-head-devel benl$ bin/ddc -O --make test/60-Shootout/Fannkuch-Redex/MainShoot.hs 
[1 of 1] Compiling MainShoot
ddc: ERROR
./test/60-Shootout/Fannkuch-Redex/MainShoot.hs:16:29
        Conflicting region constraints.
        
              constraint: Direct %115
         from the use of: flop
                      at: ./test/60-Shootout/Fannkuch-Redex/MainShoot.hs:16:29
        
            conflicts with,
              constraint: Lazy %115
         from the use of: permut
                      at: ./test/60-Shootout/Fannkuch-Redex/MainShoot.hs:42:29

Confusing, yes, but at least it's a civilised message. What it's trying to say it thought the region named %115 was Direct, meaning it cannot contain thunks, but later code wants to add thunks to it (make it Lazy). Disciple tracks what objects can or cannot be thunks, because if the backend doesn't have to check for them then the code can be a lot faster.

The confusing thing is why it thinks this region is supposed to be Direct. Top level data (like global integers) default to Direct because when we create them we know they're fully evaluated, and not thunks. However, flop is a function so should be polymorphic in this aspect, it should not require its arguments to be Direct.

Ok, looking in the interface file for the inferred type of flop says:

flop    :: Data.List.List %rTC0 (Int32 %rTC4) -(!e0 $c0)> Data.List.List %rTC0 (Int32 %rTC4)
        :- $c0   =  ${t : %rTC0} + ${t : %rTC4}
        ,  !e0   =  !Read %rTC0 + !Read %rTC4
        ,  Const  %rTC0
        ,  Const  %rTC4
        ,  Direct %rTC0
        ,  Direct %rTC4

What I'm looking at is the line:

           $c0   =  ${t : %rTC0} + ${t : %rTC4}

This is a closure constraint, and reveals that the inferencer thinks this function is referencing data in regions %rTC0 and %rTC4 from its environment. This might be true if it was referring to some top level piece of data, but it's not. The closure constraint also reports the variable being used to refer to this data, namely "t".

A closer inspection of flop reveals the underlying problem:

flop lst@(h:_) = r
 where flop' 0 (t, r)          = (t, r)
       flop' n ((h:t), r)      = flop' (n-1) (t, h:r)
       (t, r)                  = flop' h (lst, t)

Here, Miha has been tricky and used value recursion in the last line. Notice that "t" appears on both the left and the right of the binding, but the binding isn't defining a recursive function -- it's a recursive value.

Disciple doesn't support value recursion yet, as it's tricky to implement in a default-strict language, but I'd like to look into it in the future. Anyway, in Disciple today only function bindings can be recursive, so what should have happened is that the renamer should have said that "t" is not in scope in the right of the binding. Instead, that screwup has gotten through the renamer, and now the inferencer thinks that "t" has been defined outside of "flop". It has then defaulted its region to Direct and Const, as there are no opposing Lazy or Mutable constraints.

The work around is to rewrite this as an actual function binding, then use laziness to break the recursive loop:

flop lst@(h:_) = snd (thing ())
 where  flop' 0 (t, r)          = (t, r)
        flop' n ((h:t), r)      = flop' (n-1) (t, h:r)
        thing ()                = flop' h @ (lst, fst @ (thing @ ()))

A @ on the right of a binding means "lazy function application". For example, the expression (f @ x) builds a thunk holding pointers to the code for "f" and its argument "x". The programmer decides where to suspend expressions, and they are forced automatically by consumers as needed. I should probably use a different operator because it looks weird with respect to the @ on the left of bindings, but no matter.

Changing this makes the program run fine, at least with an input size of 7 (the "n" in the main function).

desire:ddc-head-devel benl$ bin/ddc -O --make test/60-Shootout/Fannkuch-Redex/MainShoot.hs 
[1 of 1] Compiling MainShoot

desire:ddc-head-devel benl$ ./a.out 
228
Pfannkuchen(7) = 16

Sadly, setting n >= 8 gives

desire:ddc-head-devel benl$ ./a.out 
*** DDC RTS PANIC! Slot stack overflow.
Abort trap

Explicit Laziness

The "slot stack" is the stack that holds pointers to heap objects. This is sometimes called a "shadow stack" and the pointers are used as roots for the garbage collector. The reason it's overflown is that Disciple is a default strict language, so our friends map, fold, filter etc evaluate the entire list when called. We can see where the stack has overflown by running the program in GDB, the GNU debugger.

desire:ddc-head-devel benl$ gdb a.out 
GNU gdb 6.3.50-20050815 (Apple version gdb-1346) (Fri Sep 18 20:40:51 UTC 2009)
...
(gdb) run
Starting program: /Users/benl/devel/ddc/ddc-head-devel/a.out 
Reading symbols for shared libraries ++. done
*** DDC RTS PANIC! Slot stack overflow.

Program received signal SIGABRT, Aborted.
0x93a74732 in __kill ()
(gdb) 
(gdb) bt
#0  0x93a74732 in __kill ()
#1  0x93a74724 in kill$UNIX2003 ()
#2  0x93b0798d in raise ()
#3  0x93b1da44 in abort ()
#4  0x00012041 in _panicOutOfSlots ()
#5  0x00003a0c in Data_List__symCl ()
#6  0x00003c04 in Data_List_iterateL ()
#7  0x00014d17 in _forceStep ()
#8  0x00014db8 in _force ()
#9  0x000048a0 in Data_List_take ()
#10 0x000049c5 in Data_List_take ()
#11 0x0000363c in Data_Function__symDl ()
#12 0x0000679f in _permut_vCL2 ()
#13 0x0000434a in Data_List_concatMap ()
#14 0x00004362 in Data_List_concatMap ()
#15 0x00004362 in Data_List_concatMap ()
#16 0x00004362 in Data_List_concatMap ()
#17 0x00004362 in Data_List_concatMap ()
#18 0x00004362 in Data_List_concatMap ()
#19 0x00004362 in Data_List_concatMap ()
#20 0x00004362 in Data_List_concatMap ()
#21 0x00004362 in Data_List_concatMap ()
#22 0x00004362 in Data_List_concatMap ()
#23 0x00004362 in Data_List_concatMap ()
... 5000 more lines

Usefully, DDC compiles via C and also uses the regular C stack for return addresses and unboxed data. The intermediate C files look like they almost could have been written by a human, and there is no evil mangler butchering the assembly code once it's been compiled. This means we get real stack traces, and I don't have the same sense of impending doom as when a GHC compiled program segfaults on me.

From the stack trace, it looks a bit like it's run out of space in concatMap. There is no concatMap in the source code, but of course every Haskell hacker knows that list comprehensions are desugared to concatMap, so it's run out of space in the list comprehension.

Disciple is default strict, so if you want producer/consumer style list processing to run in constant space using laziness, then you have to say so. Here are new versions of permut and main after rewriting the list comprehension to use a map, and converting to the lazy list functions concatL mapL and zipL:

permut n   = foldr perm [[1..n]] [2..n] 
 where perm x lst = concatL $ mapL (\l -> take x $ iterateL (rotate x) l) lst

main () 
 = do   n = 10
        (chksm, mflops) 
                = pfold (0,0) 
                $ mapL (\(i, p) -> let flops = flopS p 
                                   in  (checksum i flops, flops))
                $ zipL [0..] (permut n)

        putStr $ show chksm % "\nPfannkuchen(" % show n % ") = " % show mflops % "\n"

The functions concatL, mapL and zipL have similar definitions to the strict versions, but they're more lazy. This is like the difference between foldl and foldl' in the Haskell libraries. iterateL builds an infinite list, so there is no strict version called plain "iterate".

This makes n=8 work, but n=9 runs out of heap.

desire:ddc-head-devel benl$ bin/ddc -O --make test/60-Shootout/Fannkuch-Redex/MainShoot.hs 
[1 of 1] Compiling MainShoot
desire:ddc-head-devel benl$ ./a.out 
*** DDC RTS PANIC! Out of heap space.
        current (full) heap size: 9999999 bytes
      could not allocate another: 16 bytes
Abort trap

In a real runtime system, when the runtime heap is full it would ask for more from the OS. Unfortunately, the Disciple runtime is less featureful, uses a fixed size heap, and when it's full it's dead. It does have a garbage collector, but when all data in the heap is live there's nothing more the GC can do. However, you can set the size of the heap on the command line. Giving it 100Megs gets us n=9.

desire:ddc-head-devel benl$ ./a.out +RTS -H 100000000
8629
Pfannkuchen(9) = 30

The Treasure Finder

Garbage collection is a misnomer. Garbage collectors don't collect unused data, they copy out live data to a new space. It'd be more accurate to call them "Treasure Finders". Anyway, for interests sake we can examine the rate treasure is being found in our program. The DDC runtime supports some simple statistics like so:

desire:ddc-head-devel benl$ ./a.out +RTS -H 100000000 -profile-gc
8629
Pfannkuchen(9) = 30
desire:ddc-head-devel benl$ cat ddc-rts.prof 

-- Garbage Collection
  collection    count =                      17

  alloc         total =             760,836,560     (bytes)

  copy          total =           1,034,618,572     (bytes)
                count =              68,351,051     (objects)
      avg object size =                      15.137 (bytes)

  process time   user =                       6.120 (s)
               system =                       0.070 (s)

  mutator       total =                       1.760 (s)
                 user =                       1.700 (s)
               system =                       0.060 (s)

  collector     total =                       4.430 (s)
                 user =                       4.420 (s)
               system =                       0.010 (s)

     time efficiency  =                      28.433 (%)

Heh, 28% time efficiency isn't the best. The Disciple GC is a simple two space collector. It's not a generational GC and there is no nursery. The way the code is compiled also makes it hold onto far too much intermediate data. Fixing that would be equivalent do doing "register allocation" on the GC slot stack, so it doesn't treat an object as a root unless it really needs it.

Of course, the great thing about having 8GB of RAM in your desktop machine is that you can achieve so much with a naive language implementation. Let's compare against GHC to see how we're going:

desire:ddc-head-devel benl$ /usr/bin/time ./a.out +RTS -H 1000000000
73196
Pfannkuchen(10) = 38
       83.04 real        82.12 user         0.90 sys


desire:ddc-head-devel benl$ ghc -O2 --make test/60-Shootout/Fannkuch-Redex/MainGHC.hs -o Main
desire:ddc-head-devel benl$ /usr/bin/time ./Main 10
73196
Pfannkuchen(10) = 38
        2.10 real         2.08 user         0.01 sys

That's when I went to bed.