-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #22 from well-typed/edsko/circular
Circular programs
- Loading branch information
Showing
31 changed files
with
1,088 additions
and
423 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -7,3 +7,4 @@ dist-newstyle/ | |
| .stack-work | ||
| .cabal.sandbox.config | ||
| .envrc | ||
| foo.js | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,54 @@ | ||
| -- See "Using Circular Programs for Higher-Order Syntax" | ||
| -- by Emil Axelsson and Koen Claessen (ICFP 2013) | ||
| -- <https://emilaxelsson.github.io/documents/axelsson2013using.pdf> | ||
| -- | ||
| -- See Unfolder episode 17 for more details. | ||
| -- | ||
| -- Suggested execution: | ||
| -- | ||
| -- > cabal run visualize-cbn -- \ | ||
| -- > --show-trace \ | ||
| -- > --hide-prelude=1 \ | ||
| -- > --gc \ | ||
| -- > --selector-thunk-opt \ | ||
| -- > --inline-heap \ | ||
| -- > --hide-inlining \ | ||
| -- > --hide-gc \ | ||
| -- > --hide-selector-thunk-opt \ | ||
| -- > --javascript foo.js \ | ||
| -- > -i examples/circular_hos.hs | ||
| -- | ||
| -- Annotated execution (as of dc51993): | ||
| -- | ||
| -- 2. As soon as we demand the value of @maxBV body_0@ to determine the | ||
| -- variable to be used for the outer-most lambda, this will force the | ||
| -- construction of the next term down. This happens recursively, so the | ||
| -- entire term is build in memory. | ||
| -- 10. This is an instructive subsequence: we will see the evaluation of | ||
| -- the simple term @lam (\y -> y)@. | ||
| -- 16. At this point this term is fully known: @Lam 1 (Var 1)@. | ||
| -- 17. The computation is driven by the computation of the variable to be used | ||
| -- for the outermost lambda; we can now continue this computation a little | ||
| -- bit, because we now know the @maxBV@ of the subterm @Lam 1 (Var 1)@. | ||
| -- 19. We repeat for the second simple term @lam (\z -> z)@. | ||
| -- 27. At this point we're almost done: we need to know the @max@BV@ of the | ||
| -- subterm @Var n_1@, but there aren't any, so that is just @0@. | ||
| -- 33. At this point all bound variables are known, and the new term has been | ||
| -- constructed. | ||
| maxBV = (\exp -> | ||
| case exp of { | ||
| Var x -> 0 | ||
| ; App f e -> max (@maxBV f) (@maxBV e) | ||
| ; Lam n f -> n | ||
| } | ||
| ) | ||
|
|
||
| lam = (\f -> | ||
| let { | ||
| body = f (Var n) | ||
| ; n = succ (@maxBV body) | ||
| } | ||
| in seq n (Lam n body) | ||
| ) | ||
|
|
||
| main = @lam (\x -> App (App (@lam (\y -> y)) (@lam (\z -> z))) x) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| f = (\x -> @g x) | ||
| g = (\x -> @h x) | ||
| h = (\x -> succ x) | ||
|
|
||
| main = @f 1 | ||
|
|
||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| -- Simple example of two mutually recursive functions | ||
| -- f x will return 0 if x is even and 1 if x is odd. | ||
| main = | ||
| let { | ||
| f = (\x -> if eq x 0 then 0 else g (sub x 1)) | ||
| ; g = (\x -> if eq x 0 then 1 else f (sub x 1)) | ||
| } in f 2 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,51 @@ | ||
| -- The classic repMin circular program due to Richard Bird. | ||
| -- See Unfolder episode 17 for more details. | ||
| -- | ||
| -- Suggested execution: | ||
| -- | ||
| -- > cabal run visualize-cbn -- \ | ||
| -- > --show-trace \ | ||
| -- > --hide-prelude=1 \ | ||
| -- > --gc \ | ||
| -- > --selector-thunk-opt \ | ||
| -- > --inline-heap \ | ||
| -- > --hide-inlining \ | ||
| -- > --hide-gc \ | ||
| -- > --hide-selector-thunk-opt \ | ||
| -- > --javascript foo.js \ | ||
| -- > -i examples/repmin.hs | ||
| -- | ||
| -- Annotated execution (as of dc51993): | ||
| -- | ||
| -- 1. One way to think about this circular program is to consider that it | ||
| -- first creates a pointer to an int (the new value in the leaves), and | ||
| -- then starts building up a tree with all leaves pointing to this int; | ||
| -- as it builds the tree, it is also computing the value of this int. | ||
| -- 6. We're starting to see the tree take shape here; the top-level structure | ||
| -- of the tree is now known. | ||
| -- 10. Similarly, we now see the shape of the left subtree. | ||
| -- 13. Here we see the first @Leaf@, ponting to @m_1@; part of the computation | ||
| -- of @m_1@ is now also known (@mb_7@). | ||
| -- 16. The second @Leaf@ is known. | ||
| -- 18. The minimum value of the left subtree is known (@mb_4@). | ||
| -- 28. At this point the structure of the tree is mostly done. We can | ||
| -- finish the value computation. | ||
| worker = (\m -> \t -> | ||
| case t of { | ||
| Leaf x -> Pair x (Leaf m) | ||
| ; Branch l r -> | ||
| let { | ||
| resultLeft = @worker m l | ||
| ; resultRight = @worker m r | ||
| ; mb = min (fst resultLeft) (fst resultRight) | ||
| } | ||
| in seq mb (Pair mb (Branch (snd resultLeft) (snd resultRight))) | ||
| } | ||
| ) | ||
|
|
||
| repMin = (\t -> | ||
| let result = @worker (fst result) t | ||
| in snd result | ||
| ) | ||
|
|
||
| main = @repMin (Branch (Branch (Leaf 1) (Leaf 2)) (Branch (Leaf 3) (Leaf 4))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| -- Demonstration of the need for the selector thunk optimization | ||
| -- This is the example from "Fixing some space leaks with a garbage collector". | ||
|
|
||
| break = (\xs -> | ||
| case xs of { | ||
| Nil -> Pair Nil Nil | ||
| ; Cons x xs' -> | ||
| if eq x 0 | ||
| then Pair Nil xs' | ||
| else let b = @break xs' | ||
| in Pair (Cons x (fst b)) (snd b) | ||
| } | ||
| ) | ||
|
|
||
| -- strict version of concat (makes the example more clear) | ||
| concat = (\xs -> \ys -> | ||
| case xs of { | ||
| Nil -> ys | ||
| ; Cons x xs' -> let r = @concat xs' ys in seq r (Cons x r) | ||
| } | ||
| ) | ||
|
|
||
| surprise = (\xs -> | ||
| let b = @break xs | ||
| in @concat (fst b) (@concat (Cons 4 (Cons 5 (Cons 6 Nil))) (snd b)) | ||
| ) | ||
|
|
||
| main = @surprise (Cons 1 (Cons 2 (Cons 3 (Cons 0 (Cons 7 (Cons 8 (Cons 9 Nil))))))) |
Oops, something went wrong.