- R/O
- HTTP
- SSH
- HTTPS

No Tags

A categorical programming language

修订版 | 1f1de8e749bfef21d1f49da0036a94034e78236e (tree) |
---|---|

时间 | 2022-05-14 14:10:56 |

作者 | Corbin <cds@corb...> |

Commiter | Corbin |

Re-enable jelly acceptance tests.

- modified: default.nix (diff)
- add: hive/bits/repeat-endo.cammy (diff)
- modified: hive/demo/burning-ship-color.cammy (diff)
- modified: hive/demo/burning-ship.cammy (diff)
- add: hive/nat/64.cammy (diff)
- modified: hive/nat/to-f.cammy (diff)
- modified: make-demos.sh (diff)
- modified: todo.txt (diff)

--- a/default.nix

+++ b/default.nix

@@ -14,7 +14,7 @@ in pkgs.stdenv.mkDerivation { | ||

14 | 14 | |

15 | 15 | outputs = [ "bin" "lib" "doc" "out" ]; |

16 | 16 | |

17 | - doCheck = false; | |

17 | + doCheck = true; | |

18 | 18 | checkPhase = '' |

19 | 19 | ${pkgs.python3}/bin/python accept-jelly.py ${movelist}/bin/movelist ${jelly}/bin/jelly |

20 | 20 | ''; |

--- /dev/null

+++ b/hive/bits/repeat-endo.cammy

@@ -0,0 +1,3 @@ | ||

1 | +(bits/exp-sqr (fun/name id) (curry (comp fun/app @0)) (comp pair/dup fun/int-comp)) | |

2 | + | |

3 | +Repeatedly apply an endomorphism. |

--- a/hive/demo/burning-ship-color.cammy

+++ b/hive/demo/burning-ship-color.cammy

@@ -1,4 +1,8 @@ | ||

1 | -(comp (comp (fractal-membership-color v2/burning-ship (comp nat/32 succ)) (monads/maybe/guard (pair/of nat/lt-eq? id (fun/const nat/32)))) (case (comp (comp nat/to-f f/radians-to-turns) h2rgb) (v3/broadcast f-zero))) | |

1 | +(comp | |

2 | + (comp | |

3 | + (fractal-membership-color v2/burning-ship (comp nat/64 succ)) | |

4 | + (monads/maybe/guard (pair/of nat/lt-eq? id (fun/const nat/64)))) | |

5 | + (case (comp (comp nat/to-f f/radians-to-turns) h2rgb) (v3/broadcast f-zero))) | |

2 | 6 | |

3 | 7 | Draw membership for the [Burning Ship |

4 | 8 | fractal](https://en.wikipedia.org/wiki/Burning_Ship_fractal), a relative of |

--- a/hive/demo/burning-ship.cammy

+++ b/hive/demo/burning-ship.cammy

@@ -1,4 +1,4 @@ | ||

1 | -(comp (fractal-membership v2/burning-ship nat/32) (v3/broadcast (f/subpair (fun/const f-one) id))) | |

1 | +(comp (fractal-membership v2/burning-ship nat/64) (v3/broadcast (f/subpair (fun/const f-one) id))) | |

2 | 2 | |

3 | 3 | Draw membership for the [Burning Ship |

4 | 4 | fractal](https://en.wikipedia.org/wiki/Burning_Ship_fractal), a relative of |

--- /dev/null

+++ b/hive/nat/64.cammy

@@ -0,0 +1 @@ | ||

1 | +(comp nat/32 nat/double) |

--- a/hive/nat/to-f.cammy

+++ b/hive/nat/to-f.cammy

@@ -1,3 +1,4 @@ | ||

1 | 1 | (comp bits/from-nat bits/to-f) |

2 | 2 | |

3 | -(pr f-zero (f/addpair id (fun/const f-one))) | |

3 | +Convert a unary natural number to a floating-point number. The conversion uses | |

4 | +binary as an intermediate step to allow construction of large numbers. |

--- a/make-demos.sh

+++ b/make-demos.sh

@@ -1,11 +1,13 @@ | ||

1 | 1 | #!/bin/sh |

2 | 2 | |

3 | -<hive/demo/burning-ship.cammy result/bin/cammy-frame hive/ cost \ | |

4 | - | result/bin/cammy-jelly >demo.cammy | |

5 | -result/bin/cammy-draw demo.cammy '-1.8 -0.08 -1.7 0.02' 1920 1080 burning-ship.png \ | |

3 | +export CAMMY_HIVE=hive/ | |

4 | + | |

5 | +<hive/demo/burning-ship.cammy result-bin/bin/cammy frame cost \ | |

6 | + | result-bin/bin/cammy-jelly >demo.cammy | |

7 | +result-bin/bin/cammy draw demo.cammy '-1.8 -0.08 -1.7 0.02' 1920 1080 burning-ship.png \ | |

6 | 8 | | pv -s $((1920 * 1080 / 1000)) >/dev/null |

7 | 9 | |

8 | -<hive/demo/burning-ship-color.cammy result/bin/cammy-frame hive/ cost \ | |

10 | +<hive/demo/burning-ship-color.cammy result-bin/bin/cammy frame cost \ | |

9 | 11 | | result/bin/cammy-jelly >demo.cammy |

10 | -result/bin/cammy-draw demo.cammy '-1.8 -0.08 -1.7 0.02' 1920 1080 burning-ship-color.png \ | |

12 | +result-bin/bin/cammy draw demo.cammy '-1.8 -0.08 -1.7 0.02' 1920 1080 burning-ship-color.png \ | |

11 | 13 | | pv -s $((1920 * 1080 / 1000)) >/dev/null |

--- a/todo.txt

+++ b/todo.txt

@@ -1,15 +1,23 @@ | ||

1 | -* Faster fractals are nearly here | |

2 | - * It's all built and type-checked, but it doesn't work | |

3 | - * The fractal has type C -> [C, C] where C is complex numbers | |

4 | - * We are currently calling it with 0+0i, which is a family index | |

5 | - * Constant family, constant output | |

6 | - * We need to call it with the input number (easy) and then use internal | |

7 | - logic to call the endomorphism in a loop (hard) | |

8 | - * but done | |

9 | - * Faster fractals are fast, but don't work | |

10 | - * Can get all-white, all-green, nothing else | |

11 | - * Are we returning wrong values again? | |

12 | - * Factor out monads and try again? | |

1 | +* Idea for new subcommands | |

2 | + * cammy dissolve | |

3 | + * Takes no arguments, just hive and input expr | |

4 | + * Returns equivalent to input, but using as much of hive as possible | |

5 | + * Implementation strategy: build up hash-cons structure in memory | |

6 | + * Iterate over hive, adding each expression to hash-cons | |

7 | + * Also build up partial dissolution map from hash-cons nodes to hive paths | |

8 | + * In unlikely case of ambiguity, guess | |

9 | + * Later on, we can make an informed guess by looking at neighboring nodes | |

10 | + * cammy crystallize | |

11 | + * Again, just hive and input | |

12 | + * Returns equivalent to input, mostly dissolved, but top few nodes are | |

13 | + deliberately tracked or expanded | |

14 | + * Each expanded node has its trail appended | |

15 | + * A weave is generated, including documentation | |

16 | + * Output is ready to feed to pandoc | |

17 | + * Output is a "crystal grown from $EXPR"; it explains the algorithm | |

18 | + incrementally, piece-by-piece | |

19 | + * Still not real literate programming, but getting closer | |

20 | + * Should use same underlying tools as dissolve | |

13 | 21 | * REPL improvements |

14 | 22 | * allow mid-functor newlines |

15 | 23 | * : commands |

@@ -84,6 +92,18 @@ | ||

84 | 92 | * formal power series N -> Q |

85 | 93 | * needs Q |

86 | 94 | * done for N -> N |

95 | +* computable reals from N -> Z | |

96 | + * So-called "fast binary" Cauchy sequences | |

97 | + * f : N -> Z is fast binary Cauchy iff | |

98 | + exists real x s.t. for all n, abs(x - f(n)*(2**-n)) < 2**-n | |

99 | + * Values of f get big fast, but only linear growth in memory | |

100 | + * We'll need bigints! | |

101 | + * Haskell's CReal has time-tested algorithms for this | |

102 | + * We can't reuse the formal proofs, but it's not like Haskell can reuse | |

103 | + them either~ | |

104 | + * Would not be fast enough for raytracing, but could generate various | |

105 | + computable real constants | |

106 | + * Extraction to floats would hopefully require n < 100 | |

87 | 107 | * Dual numbers: like complex numbers, but different units, multiplication |

88 | 108 | * started a folder, haven't done AD yet |

89 | 109 | * CI: automatic generation of demo images |

@@ -144,14 +164,14 @@ | ||

144 | 164 | * would give us constant-time pred and succ |

145 | 165 | * So, jets? Jets: |

146 | 166 | * Replace user-level composites with builtin ops |

147 | - * how to replace e.g. nat/add? | |

148 | - * find its subgraph with E-matching? | |

149 | - * This seemed to work, but didn't speed things up much | |

150 | - * hook the hive to load a specialized routine during codeload? | |

167 | + * Done for nat/add and nat/pred-maybe | |

168 | + * Makes Project Euler (6) possible, accelerates demos | |

151 | 169 | * pair/swap is now known as a special case to movelist and jelly |

152 | 170 | * this might be fundamental to symmetric monoidal categories or CCCs |

153 | 171 | * uncurry distills down to fun/app, as in the literature |

154 | 172 | * (uncurry @0) could be defined as (comp (pair/mapfst @0) fun/app) |

173 | +* Clean up CAM term ops and stack ops | |

174 | + * Term ops should be vmprof'd somehow | |

155 | 175 | * Some basic dependent types |

156 | 176 | * Type-level arithmetic would be nice |

157 | 177 | * Could have types like (fin n): not just 1 and 2, but 3, 4, etc. |

@@ -169,31 +189,45 @@ | ||

169 | 189 | 4) unclear how to proceed |

170 | 190 | 5) turn numbers into multisets of factors (Gödel style), take union of |

171 | 191 | multisets with maximum of each coefficient |

172 | - 6) implemented, can compute f(10) but not f(100) | |

192 | + 6) implemented and computable | |

173 | 193 | 7) need the function N -> N which indexes the primes |

174 | 194 | 8) more digit-manipulation BS |

175 | 195 | 9) not really a programming exercise; we could implement the algorithm for |

176 | 196 | generating Pythagorean triples |

177 | 197 | 10) could generate a list of primes and sum it |

198 | + 11) need to eat a file as input | |

199 | + 12) not really programming | |

200 | + 13) need to eat input file | |

201 | + 14) Collatz sequence | |

202 | + 15) combinatorial question, doesn't actually require geometry | |

203 | + 16) looks like a digit-manipulation question, but probably isn't done with | |

204 | + brute-force computation | |

205 | + 17) definitely a digit-manipulation question | |

206 | + 18) A* through a given graph | |

207 | + 19) Conway's Doomsday algorithm | |

208 | + 20) oh look, digit manipulation | |

178 | 209 | * take every third element in a list |

179 | 210 | * Useful for (1) and (2) |

180 | 211 | * enumerate the primes |

181 | 212 | * Directly solves (7) and (10) |

213 | + * compute binomial coefficients | |

214 | + * Useful in general, would solve (15) | |

215 | + * (15) is solved by f(n) = binomial(2n, n) | |

182 | 216 | * Can we use bits/exp-sqr to speed up iteration of endomorphisms? |

183 | 217 | * needs zero, succ, double |

184 | 218 | * Given f : X -> X, (fun/name f) : 1 -> [X, X] is the succ |

185 | 219 | * Well, really, needs |

186 | 220 | (pair/of fun/int-comp (fun/name f) id) : [X, X] -> [X, X] |

187 | 221 | * Could be crucial to choose whether to pre- or postcompose |

188 | - * zero is natural: (fun/name id) 1 -> [X, X] | |

222 | + * zero is natural: (fun/name id) : 1 -> [X, X] | |

189 | 223 | * double is also natural! (comp pair/dup fun/int-comp) : [X, X] -> [X, X] |

224 | + * proof of concept: bits/repeat-endo | |

190 | 225 | * Current refactoring |

191 | - * Tired of so many RPython builds for overlapping code | |

192 | 226 | * Making a single entrypoint with subcommands ala git |

193 | 227 | * comb, draw, frame, rename, repl, weave |

194 | 228 | * draw doesn't use hive, other five do |

195 | 229 | * Maybe draw should be changed to invoke frame and jelly? It's usually |

196 | 230 | what we want anyway |

197 | - * so maybe hive should be available via env var | |

231 | + * hive is be available via env var CAMMY_HIVE | |

198 | 232 | * we usually don't want to change it |

199 | 233 | * we could compile in a default hive |