提交: 9cc1c3a0fccc5664e0d4e3413783588c23aed667 - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: 9cc1c3a0fccc5664e0d4e3413783588c23aed667 (tree)
• 时间: 2022-04-01 13:37:56
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Get faster fractal membership working, somewhat.

I'm not quite confident in the correctness of my step "monad", which
deliberately breaks the monad laws to facilitate counting evaluation
steps. I'm also not sure why it's so slow.

更改概述

• modified: cammy-rpy/draw.py
• modified: cammy-rpy/repl.py
• add: hive/bits/about.md
• add: hive/bits/succ.cammy
• add: hive/bits/zero.cammy
• add: hive/bool/half-adder.cammy
• add: hive/bool/parity.cammy
• add: hive/bool/popcount.cammy
• add: hive/bool/xor.cammy
• add: hive/demo/burning-ship-fast.cammy
• modified: hive/demo/burning-ship.cammy
• modified: hive/demo/mandelbrot.cammy
• add: hive/fps/about.md
• add: hive/fps/add.cammy
• add: hive/fps/diff.cammy
• add: hive/fps/extract.cammy
• add: hive/fps/zero.cammy
• add: hive/fractal-maybe.cammy
• add: hive/fractal-membership-fast.cammy
• delete: hive/fun/inv-img.cammy
• add: hive/fun/postcomp.cammy
• add: hive/fun/precomp.cammy
• add: hive/iter-fractal-fast.cammy
• add: hive/iter-maybe-count.cammy
• add: hive/list/tail.cammy
• add: hive/magma/about.md
• add: hive/magma/braid.cammy
• add: hive/magma/square.cammy
• add: hive/maybe-step.cammy
• add: hive/monads/int-comp.cammy
• add: hive/monads/iter.cammy
• add: hive/monads/maybe/int-bind.cammy
• add: hive/monoids/endo/about.md
• add: hive/monoids/endo/add.cammy
• add: hive/monoids/endo/zero.cammy
• modified: hive/nat/256.cammy
• modified: hive/nat/8.cammy
• add: hive/nat/81.cammy
• add: hive/nat/9.cammy
• add: hive/step-bind.cammy
• add: hive/step-comp.cammy
• add: hive/step-iter.cammy
• add: hive/step-unit.cammy
• add: hive/take-step.cammy
• modified: hive/yoneda/embed.cammy
• modified: shell.nix
• modified: todo.txt

差异

--- a/cammy-rpy/draw.py
+++ b/cammy-rpy/draw.py
@@ -1,6 +1,7 @@
 import math, sys
 
-from rpython.rlib.jit import JitDriver, set_param, unroll_safe
+from rpython.rlib.jit import JitDriver, unroll_safe #, set_param
+from rpython.rlib.rfile import create_stdio
 from rpython.rlib.rfloat import string_to_float
 from rpython.rlib.rstring import StringBuilder, split
 
@@ -77,6 +78,7 @@ def multisample(program, radius, x, y):
     return finishChannel(r / l), finishChannel(g / l), finishChannel(b / l)
 
 def drawPixels(size, program, window):
+    _, stdout, _ = create_stdio()
     sb = StringBuilder()
     i = 0
     while i < size:
@@ -84,6 +86,9 @@ def drawPixels(size, program, window):
         r, g, b = multisample(program, window.pixelRadius, c1, c2)
         sb.append(chr(r) + chr(g) + chr(b))
         i += 1
+        if not (i % 1000):
+            stdout.write(".")
+            stdout.flush()
     return sb.build()
 
 def drawPNG(program, filename, corners, width, height):
@@ -95,7 +100,7 @@ def drawPNG(program, filename, corners, width, height):
 
 
 def main(argv):
-    set_param(None, "trace_limit", 50001)
+    # set_param(None, "trace_limit", 50001)
 
     prog = argv[1]
     window = [string_to_float(s) for s in split(argv[2])]

--- a/cammy-rpy/repl.py
+++ b/cammy-rpy/repl.py
@@ -69,19 +69,16 @@ def repl(hive, stdin, stdout):
             command(hive, line[1], line[3:])
             continue
         sexp, trail = parse(line)
-        print "Got:", line
-        print "S-expression:", sexp.asStr()
-        print "Trail:", trail
         try:
             sexp = sexp.canonicalize(hive)
-            print "Canonicalized:", sexp.asStr()
+            # print "Canonicalized:", sexp.asStr()
         except MissingAtom as ma:
             print "Couldn't canonicalize S-expression; missing atom:", ma.atom
         sexp = jellify(sexp)
-        print "Jellified:", sexp.asStr()
+        # print "Jellified:", sexp.asStr()
         try:
             arrow = sexp.buildArrow()
-            print "Arrow:", arrow
+            # print "Arrow:", arrow
             cs = ConstraintStore()
             domain, codomain = arrow.types(cs)
             extractor = TypeExtractor(cs, PlaintextTypeFormatter())

--- /dev/null
+++ b/hive/bits/about.md
@@ -0,0 +1,2 @@
+The type $[2]$ can be interpreted as a type of natural numbers equipped with a
+relatively fast primitive recursion.

--- /dev/null
+++ b/hive/bits/succ.cammy
@@ -0,0 +1,9 @@
+(comp
+  (fold (pair t nil)
+    (comp
+      (comp pair/assl
+        (pair/mapfst (comp bool/half-adder pair/swap)))
+      (comp pair/assr (pair/mapsnd cons))))
+  (uncurry (bool/if (list/conspair (fun/const t) id) id)))
+
+The successor of a natural number is also a natural number.

--- /dev/null
+++ b/hive/bits/zero.cammy
@@ -0,0 +1 @@
+nil

--- /dev/null
+++ b/hive/bool/half-adder.cammy
@@ -0,0 +1,3 @@
+(pair bool/xor conj)
+
+Add two bits, returning a pair of the result and carry bit.

--- /dev/null
+++ b/hive/bool/parity.cammy
@@ -0,0 +1,3 @@
+(fold f bool/xor)
+
+The parity of a list of bits.

--- /dev/null
+++ b/hive/bool/popcount.cammy
@@ -0,0 +1,3 @@
+(fold zero (uncurry (bool/if succ id)))
+
+The number of set bits in a list of bits.

--- /dev/null
+++ b/hive/bool/xor.cammy
@@ -0,0 +1,3 @@
+(comp (pair disj (comp conj not)) conj)
+
+The exclusive-or operation, also known as the parity operation.

--- /dev/null
+++ b/hive/demo/burning-ship-fast.cammy
@@ -0,0 +1,5 @@
+(comp (fractal-membership-fast v2/burning-ship nat/256) (v3/broadcast (f/subpair (fun/const f-one) id)))
+
+Draw membership for the [Burning Ship
+fractal](https://en.wikipedia.org/wiki/Burning_Ship_fractal), a relative of
+the Mandelbrot set.

--- a/hive/demo/burning-ship.cammy
+++ b/hive/demo/burning-ship.cammy
@@ -1,6 +1,4 @@
-(comp
-  (fractal-membership v2/burning-ship nat/256)
-  (v3/broadcast (f/subpair (fun/const f-one) id)))
+(comp (fractal-membership v2/burning-ship nat/256) (v3/broadcast (f/subpair (fun/const f-one) id)))
 
 Draw membership for the [Burning Ship
 fractal](https://en.wikipedia.org/wiki/Burning_Ship_fractal), a relative of

--- a/hive/demo/mandelbrot.cammy
+++ b/hive/demo/mandelbrot.cammy
@@ -1,6 +1,4 @@
-(comp
-  (fractal-membership v2/mandelbrot nat/256)
-  (v3/broadcast (f/subpair (fun/const f-one) id)))
+(comp (fractal-membership v2/mandelbrot nat/256) (v3/broadcast (f/subpair (fun/const f-one) id)))
 
 Draw membership in the [Mandelbrot
 set](https://en.wikipedia.org/wiki/Mandelbrot_set).

--- /dev/null
+++ b/hive/fps/about.md
@@ -0,0 +1,3 @@
+The function type $\mathbb{N}^\mathbb{N}$ can be interpreted as a [formal
+power series](https://en.wikipedia.org/wiki/Formal_power_series) on the
+natural numbers with coefficients in the natural numbers.

--- /dev/null
+++ b/hive/fps/add.cammy
@@ -0,0 +1,3 @@
+(curry (comp (comp (pair/mapsnd pair/dup) (v2/map2 fun/app)) nat/add))
+
+The sum of two formal power series.

--- /dev/null
+++ b/hive/fps/diff.cammy
@@ -0,0 +1,3 @@
+(curry (comp (comp (pair/mapsnd succ) (pair fun/app snd)) nat/mul))
+
+The formal derivative of a formal power series.

--- /dev/null
+++ b/hive/fps/extract.cammy
@@ -0,0 +1,3 @@
+(comp pair/swap fun/app)
+
+Extract a coefficient from a formal power series.

--- /dev/null
+++ b/hive/fps/zero.cammy
@@ -0,0 +1,3 @@
+(curry (comp fst zero))
+
+The zero formal power series.

--- /dev/null
+++ b/hive/fractal-maybe.cammy
@@ -0,0 +1,3 @@
+(comp (comp @0 (pair v2/complex/mag-2 (pair left (comp ignore right)))) bool/pick)
+
+Take a step in an IFS, failing if the step has magnitude 2 or greater.

--- /dev/null
+++ b/hive/fractal-membership-fast.cammy
@@ -0,0 +1,5 @@
+(comp (iter-fractal-fast @0 @1) (case (fun/const f-one) (fun/const f-zero)))
+
+Iterate a fractal for a maximum number of steps, and return a value in $[0,1]$
+indicating how many steps were taken, with 1 indicating that the fractal did
+not diverge.

--- a/hive/fun/inv-img.cammy
+++ /dev/null
@@ -1,3 +0,0 @@
-(curry (fun/apppair fst (comp snd @0)))
-
-The inverse-image functor for an arbitrary classifier.

--- /dev/null
+++ b/hive/fun/postcomp.cammy
@@ -0,0 +1,4 @@
+(curry (comp fun/app @0))
+
+Postcompose a function type with an arrow. This is like one version of the
+Yoneda embedding for the given arrow.

--- /dev/null
+++ b/hive/fun/precomp.cammy
@@ -0,0 +1,5 @@
+(curry (fun/apppair fst (comp snd @0)))
+
+Precompose a function type with an arrow. This is like the inverse-image
+functor for an arbitrary classifier. It is also like one version of the Yoneda
+embedding for the given arrow.

--- /dev/null
+++ b/hive/iter-fractal-fast.cammy
@@ -0,0 +1,5 @@
+(fun/unname (comp @1
+  (step-iter (fractal-maybe
+    (fun/unname (comp (comp f-zero pair/dup) @0))))))
+
+Given a maximum number of steps, iterate the given fractal.

--- /dev/null
+++ b/hive/iter-maybe-count.cammy
@@ -0,0 +1,13 @@
+(pr @0 @1)
+
+@0: 1 -> [X, X + N]
+@1: [X, X + N] -> [X, X + N]
+(uncurry @1) : [X, X + N] x X -> X + N
+
+Given X -> X + 1
+N -> [X, X + N]
+max iterations -> [x,
+  x after max iterations + number of iterations before failing]
+
+Intermediate state is more like:
+X x N -> X x N + N

--- /dev/null
+++ b/hive/list/tail.cammy
@@ -0,0 +1,3 @@
+(comp list/uncons (case snd nil))
+
+The tail of a list. The tail of the empty list is the empty list.

--- /dev/null
+++ b/hive/magma/about.md
@@ -0,0 +1,2 @@
+The function type $X^{X \times X}$ can be interpreted as the type of magmas on
+$X$. A magma is a binary operation.

--- /dev/null
+++ b/hive/magma/braid.cammy
@@ -0,0 +1,3 @@
+(fun/precomp pair/swap)
+
+Braid a magma, obtaining its opposite magma.

--- /dev/null
+++ b/hive/magma/square.cammy
@@ -0,0 +1,3 @@
+(fun/precomp pair/dup)
+
+A magma can be squared to produce an endomorphism.

--- /dev/null
+++ b/hive/maybe-step.cammy
@@ -0,0 +1 @@
+(comp @0 (case (comp (pair id (fun/const (comp zero succ))) left) (comp zero right)))

--- /dev/null
+++ b/hive/monads/int-comp.cammy
@@ -0,0 +1,3 @@
+(curry (comp (pair (fun/apppair (comp fst snd) snd) (comp fst fst)) @0))
+
+Internal composition in any monad, built from the internal bind.

--- /dev/null
+++ b/hive/monads/iter.cammy
@@ -0,0 +1,12 @@
+(pr
+  (fun/name @0)
+  (comp (pair id (fun/const (fun/name @2))) (monads/int-comp @1)))
+
+Given a unit and internal bind in some monad, iterate an endomorphism in that
+monad.
+
+For example, to iterate in the maybe monad:
+
+    (monads/iter monads/maybe/unit monads/maybe/int-bind @0)
+
+Iteration can terminate early in short-circuiting monads.

--- /dev/null
+++ b/hive/monads/maybe/int-bind.cammy
@@ -0,0 +1,3 @@
+(comp fun/distribl (case (comp pair/swap fun/app) (comp ignore right)))
+
+An internal version of bind for the maybe monad.

--- /dev/null
+++ b/hive/monoids/endo/about.md
@@ -0,0 +1,2 @@
+For a given type $X$, the function type $X^X$ of
+[endomorphisms](https://ncatlab.org/nlab/show/endomorphism) forms a monoid.

--- /dev/null
+++ b/hive/monoids/endo/add.cammy
@@ -0,0 +1,3 @@
+fun/int-comp
+
+Addition in an endomorphism monoid.

--- /dev/null
+++ b/hive/monoids/endo/zero.cammy
@@ -0,0 +1,3 @@
+(fun/name id)
+
+The zero of an endomorphism monoid.

--- a/hive/nat/256.cammy
+++ b/hive/nat/256.cammy
@@ -1 +1 @@
-(comp (pair nat/2 nat/8) nat/exp)
+(comp (pair nat/8 nat/2) nat/exp)

--- a/hive/nat/8.cammy
+++ b/hive/nat/8.cammy
@@ -1 +1 @@
-(comp (pair nat/2 nat/3) nat/exp)
+(comp (pair nat/3 nat/2) nat/exp)

--- /dev/null
+++ b/hive/nat/81.cammy
@@ -0,0 +1,3 @@
+(comp (pair nat/2 nat/9) nat/exp)
+
+

--- /dev/null
+++ b/hive/nat/9.cammy
@@ -0,0 +1 @@
+(comp (pair nat/2 nat/3) nat/exp)

--- /dev/null
+++ b/hive/step-bind.cammy
@@ -0,0 +1,11 @@
+(comp fun/distribl
+  (case
+    (comp
+      (pair (fun/apppair snd (comp fst fst)) (comp fst snd))
+      (comp fun/distribl
+        (case
+          (comp (comp pair/assr (pair/mapsnd nat/add)) left)
+          (comp nat/add right))))
+    (comp fst right)))
+
+(X x N + N) x [X, Y x N + N] -> Y x N + N

--- /dev/null
+++ b/hive/step-comp.cammy
@@ -0,0 +1,10 @@
+(curry
+  (comp
+    (comp
+      (pair (comp fst fst) (fun/apppair (comp fst snd) snd))
+      fun/distribr)
+    (case fun/app (comp snd right))))
+
+([Y x N, Z x N + N] x [X x N, Y x N + N]) x (X x N) -> Z x N + N
+
+[Y x N, Z x N + N] x [X x N, Y x N + N] -> [X x N, Z x N + N]

--- /dev/null
+++ b/hive/step-iter.cammy
@@ -0,0 +1,3 @@
+(monads/iter step-unit step-bind (maybe-step @0))
+
+

--- /dev/null
+++ b/hive/step-unit.cammy
@@ -0,0 +1,3 @@
+(comp (pair id (fun/const zero)) left)
+
+The unit of a sort of step monad.

--- /dev/null
+++ b/hive/take-step.cammy
@@ -0,0 +1,3 @@
+(comp (comp (pair/tensor @0 succ) fun/distribl) (case left (comp snd right)))
+
+Take a step along a partial arrow, incrementing the number of steps taken.

--- a/hive/yoneda/embed.cammy
+++ b/hive/yoneda/embed.cammy
@@ -1,3 +1,3 @@
-(curry (comp fun/app @0))
+(fun/postcomp @0)
 
 The Yoneda embedding of an arrow.

--- a/shell.nix
+++ b/shell.nix
@@ -16,6 +16,8 @@ in pkgs.stdenv.mkDerivation {
     pythonPackages.pyflakes
     # using cammy-comb
     graphviz
+    # using cammy-draw
+    pv
     # using cammy-weave
     pandoc texlive.combined.scheme-small
     # using cammy-repl

--- a/todo.txt
+++ b/todo.txt
@@ -6,7 +6,6 @@
 * More list manipulations
   * list/eq : [X × X, 2] → [[X] × [X], 2]
   * list/zip : [X] × [Y] → [X × Y]
-  * list/tail : [X] → [X]
 * rat
   * Using binary quote notation?
   * Continued fractions?
@@ -19,12 +18,11 @@
   * Euler's constant e
   * Euler's constant gamma
 * Double-negation monad for CPS?
-  * Cont is available but not fully developed
-    * monads/cont/join, monads/cont/bind, etc.
 * fun/name should always start from 1
   * Requires changing some callers
   * Might not be feasible unless we switch to stricter monoidal categories
     * We'd need an equivalence X × 1 → X
+    * swap and dup would need to be primitive again too
 * Prove that nat/add is smallest with its behavior
 * Streams
   * Monad: X → [N, X]
@@ -44,14 +42,6 @@
     * hook the hive to load a specialized routine during codeload?
   * pair/swap is builtin to movelist and jelly
     * this might be fundamental to symmetric monoidal categories or CCCs
-* Search for more optimizations
-  * Some arrows have inferred types that suggest they should be simplifiable
-    * X -> X: should be id?
-    * X -> 1: should be ignore
-    * 1 -> 2: should be t or f
-* Refactoring tools
-  * Find all leaves in a hive
-  * Rename an expression and change all callers
 * Maybe allow inductive datatype definitions during toolchain build time
   * Start by factoring out N and lists into inductive datatype modules somehow
   * Then add trees, etc.