コミット: 21782876c22e894e34939d075ca8e01ba655d28b - cammy (git)

A categorical programming language

コミットメタ情報

• リビジョン: 21782876c22e894e34939d075ca8e01ba655d28b (tree)
• 日時: 2022-03-17 14:10:00
• 作者: Corbin <cds@corb...>
• コミッター: Corbin

ログメッセージ

Write out some basic docs for the hive.

変更サマリ

• modified: cammy-rpy/draw.nix
• modified: cammy-rpy/weave.py
• add: hive/about.md
• add: hive/baire/about.md
• add: hive/bool/about.md
• add: hive/comonads/product/about.md
• add: hive/comonads/store/about.md
• add: hive/demo/about.md
• add: hive/double/about.md
• add: hive/f/about.md
• add: hive/fun/about.md
• add: hive/int/about.md
• add: hive/list/about.md
• add: hive/list/horner.cammy
• add: hive/mat2/about.md
• modified: hive/mat2/mul.cammy
• add: hive/monads/cont/about.md
• add: hive/monads/either/about.md
• add: hive/monads/maybe/about.md
• add: hive/monads/reader/about.md
• add: hive/monads/state/about.md
• add: hive/nat/about.md
• add: hive/nonempty/about.md
• add: hive/nonempty/to-list.cammy
• add: hive/pair/about.md
• add: hive/scott/about.md
• add: hive/scott/bool/about.md
• delete: hive/scott/list/cons.cammy
• delete: hive/scott/list/nil.cammy
• delete: hive/scott/nat/pred.cammy
• delete: hive/scott/nat/succ.cammy
• delete: hive/scott/nat/zero.cammy
• add: hive/sdf2/about.md
• add: hive/square/about.md
• add: hive/subobj/about.md
• add: hive/sum/about.md
• add: hive/v2/about.md
• add: hive/v3/about.md
• delete: hive/{fun => pair}/tensor.cammy
• modified: todo.txt

差分

--- a/cammy-rpy/draw.nix
+++ b/cammy-rpy/draw.nix
@@ -1,4 +1,4 @@
 let
   makeBuilder = import ./builder.nix;
 in
-  makeBuilder ./draw.py "cammy-draw" false # true
+  makeBuilder ./draw.py "cammy-draw" true

--- a/cammy-rpy/weave.py
+++ b/cammy-rpy/weave.py
@@ -48,6 +48,14 @@ def main(argv):
         section = dirpath[prefix:] or "Top level"
         doc.append("# " + section)
 
+        # Optionally include section-specific information if present.
+        aboutpath = os.path.join(dirpath, "about.md")
+        try:
+            with open(aboutpath, "r") as handle:
+                doc.append(handle.read())
+        except IOError:
+            doc.append("(Undocumented section)")
+
         for filename in filenames:
             if not filename.endswith(".cammy"):
                 continue

--- /dev/null
+++ b/hive/about.md
@@ -0,0 +1,3 @@
+This hive provides some basic tools for approximating and visualizing
+functions on real numbers. It includes a demonstration renderer for iterated
+fractal systems.

--- /dev/null
+++ b/hive/baire/about.md
@@ -0,0 +1,2 @@
+The exponential type $\mathbb{N}^\mathbb{N}$ can be interpreted as [Baire
+space](https://en.wikipedia.org/wiki/Baire_space_(set_theory)).

--- /dev/null
+++ b/hive/bool/about.md
@@ -0,0 +1 @@
+The Boolean type $2$ contains exactly two elements.

--- /dev/null
+++ b/hive/comonads/product/about.md
@@ -0,0 +1 @@
+The product comonad is a comonad.

--- /dev/null
+++ b/hive/comonads/store/about.md
@@ -0,0 +1 @@
+The [store comonad](https://ncatlab.org/nlab/show/store+comonad) is a comonad.

--- /dev/null
+++ b/hive/demo/about.md
@@ -0,0 +1 @@
+These Cammy expressions are included for demonstration purposes.

--- /dev/null
+++ b/hive/double/about.md
@@ -0,0 +1 @@
+The double type $X + X$ is isomorphic to the Boolen tag type $X \times 2$.

--- /dev/null
+++ b/hive/f/about.md
@@ -0,0 +1,3 @@
+The numeric type $F$ is a type of double-precision [IEEE
+754](https://en.wikipedia.org/wiki/IEEE_754) floating-point numbers. Only
+numbers are included; no elements of $F$ are not numbers.

--- /dev/null
+++ b/hive/fun/about.md
@@ -0,0 +1,2 @@
+The function types ${Y}^{X}$ are the primary building blocks of Cammy
+expressions.

--- /dev/null
+++ b/hive/int/about.md
@@ -0,0 +1,6 @@
+The type $N + N$ can be interpreted as the type of integers. Specifically, the
+left-hand components are positive integers, the right-hand components are
+negative integers, and zero can be represented as either left-hand zero or
+right-hand zero. Under the equivalence with the type $N \times 2$, the
+representation can be viewed as a natural number with a [sign
+bit](https://en.wikipedia.org/wiki/Sign_bit).

--- /dev/null
+++ b/hive/list/about.md
@@ -0,0 +1 @@
+The list type $[X]$ is the free monoid over $X$.

--- /dev/null
+++ b/hive/list/horner.cammy
@@ -0,0 +1,11 @@
+(comp
+  (pair/mapfst list/reverse)
+  (uncurry (fold
+    (fun/name (fun/const zero))
+    (curry (comp
+      (pair (pair (comp fst fst) (fun/apppair (comp fst snd) snd)) snd)
+      (pair/of nat/add
+        (pair/of nat/mul (comp fst snd) snd)
+        (comp fst fst)))))))
+
+Evaluate a polynomial at an input coordinate using Horner's rule.

--- /dev/null
+++ b/hive/mat2/about.md
@@ -0,0 +1,2 @@
+The type $(X \times X) \times (X \times X)$ can be interpreted as a two-by-two
+matrix over $X$.

--- a/hive/mat2/mul.cammy
+++ b/hive/mat2/mul.cammy
@@ -1,7 +1,3 @@
-(comp
-    (fun/tensor id mat2/trans)
-    (pair
-        (mat2/vecpair fst (comp snd fst))
-        (mat2/vecpair fst (comp snd snd))))
+(comp (fun/tensor id mat2/trans) (pair (mat2/vecpair fst (comp snd fst)) (mat2/vecpair fst (comp snd snd))))
 
 Multiply two matrices.

--- /dev/null
+++ b/hive/monads/cont/about.md
@@ -0,0 +1,9 @@
+A [continuation monad](https://ncatlab.org/nlab/show/continuation+monad) is a
+codensity monad. The typical continuation monad arises from the
+double-negation endofunctor
+
+$$
+D : X \mapsto {R}^{{R}^{X}}
+$$
+
+for some continuation type $R$.

--- /dev/null
+++ b/hive/monads/either/about.md
@@ -0,0 +1 @@
+The either monad is a monad.

--- /dev/null
+++ b/hive/monads/maybe/about.md
@@ -0,0 +1,6 @@
+The [maybe monad](https://ncatlab.org/nlab/show/maybe+monad) is the monad
+carried by the endofunctor
+
+$$
+M : X \mapsto X + 1
+$$

--- /dev/null
+++ b/hive/monads/reader/about.md
@@ -0,0 +1 @@
+The [reader monad](https://ncatlab.org/nlab/show/function+monad) is a monad.

--- /dev/null
+++ b/hive/monads/state/about.md
@@ -0,0 +1 @@
+The [state monad](https://ncatlab.org/nlab/show/state+monad) is a monad.

--- /dev/null
+++ b/hive/nat/about.md
@@ -0,0 +1 @@
+The elements of the type $\mathbb{N}$ are natural numbers.

--- /dev/null
+++ b/hive/nonempty/about.md
@@ -0,0 +1,2 @@
+The type $X \times [X]$ can be interpreted as a type of nonempty lists of
+$X$. The first component is the head of the list.

--- /dev/null
+++ b/hive/nonempty/to-list.cammy
@@ -0,0 +1,3 @@
+cons
+
+A nonempty list is a list.

--- /dev/null
+++ b/hive/pair/about.md
@@ -0,0 +1,15 @@
+The pair type $X \times Y$ is ubiquitous when programming with
+Cartesian closed categories. Common uses for pairs include:
+
+* Passing multiple arguments to arrows
+* Pairing a state with a projection or observation
+* Placing a value to the side while performing an intermediate transformation
+* Performing multiple transformations in parallel
+
+Pairs naturally form a comonad, the product comonad, carried by the endofunctor
+
+$$
+P : X \mapsto X \times A
+$$
+
+for some fixed type of observations $A$.

--- /dev/null
+++ b/hive/scott/about.md
@@ -0,0 +1,4 @@
+The [Scott
+encoding](https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding) of
+an algebraic data type represents it as a set of arguments in a first-order
+type signature.

--- /dev/null
+++ b/hive/scott/bool/about.md
@@ -0,0 +1,2 @@
+The Scott encoding for Booleans is the same as the [Church encoding for
+Booleans](https://en.wikipedia.org/wiki/Church_encoding#Church_Booleans).

--- a/hive/scott/list/cons.cammy
+++ /dev/null
@@ -1,5 +0,0 @@
-(curry (curry (curry
-  (comp (pair
-    (comp (pair snd (comp (comp fst fst) fst)) fun/app)
-    (comp fst snd))
-  fun/app))))

--- a/hive/scott/list/nil.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(curry fst)

--- a/hive/scott/nat/pred.cammy
+++ /dev/null
@@ -1,2 +0,0 @@
-(comp (pair (comp (pair (fun/const (fun/name scott/nat/zero)) id) fun/app)
-  (fun/name id)) fun/app)

--- a/hive/scott/nat/succ.cammy
+++ /dev/null
@@ -1 +0,0 @@
-(curry (curry (comp (pair snd (comp fst fst)) fun/app)))

--- a/hive/scott/nat/zero.cammy
+++ /dev/null
@@ -1,3 +0,0 @@
-(curry fst)
-
-The Scott-encoded version of zero.

--- /dev/null
+++ b/hive/sdf2/about.md
@@ -0,0 +1,5 @@
+The arrow type $F \times F \to F$ can be interpreted as a type of functions
+from points in the 2-dimensional Cartesian plane to distances. In particular,
+it may be interpreted as a type of [signed distance
+functions](https://en.wikipedia.org/wiki/Signed_distance_function) in the
+Cartesian plane.

--- /dev/null
+++ b/hive/square/about.md
@@ -0,0 +1,8 @@
+The square type $X ^ 2$ is isomorphic to the diagonal pair type $X \times X$.
+The endofunctor
+
+$$
+Sq : X \mapsto X^2
+$$
+
+is a special case of the endofunctor which carries the reader monad.

--- /dev/null
+++ b/hive/subobj/about.md
@@ -0,0 +1,2 @@
+The exponential type $2 ^ X$ can be interpreted as the type of subobjects of
+$X$. However, $2$ is not a subobject classifier.

--- /dev/null
+++ b/hive/sum/about.md
@@ -0,0 +1 @@
+The type $X + Y$ is a heterogenous sum type.

--- /dev/null
+++ b/hive/v2/about.md
@@ -0,0 +1,2 @@
+The product type $X \times X$ can be interpreted as a 2-dimensional vector
+space over $X$.

--- /dev/null
+++ b/hive/v3/about.md
@@ -0,0 +1,2 @@
+The type $X \times ( X \times X )$ can be interpreted as a 3-dimensional
+vector space over $X$.

--- a/todo.txt
+++ b/todo.txt
@@ -8,6 +8,8 @@
   * list/zip : [X] × [Y] → [X × Y]
   * list/tail : [X] → [X]
 * rat
+  * Using binary quote notation?
+  * Continued fractions?
 * refactoring from the bikeshed: ignore -> !
   * Might not be important since fun/const is the only user!
   * zero -> 0, f-zero -> f-0, f-one -> f-1 maybe?
@@ -30,10 +32,7 @@
 * Subtypes?
   * Interval type?
 * Cantor's type of bitstrings: N -> 2
-* The square type: For a type X, 2 -> X
-  * Another special case of reader monad
-  * There's an equivalence X x X <-> [2, X]
-    * Done?
+  * We have subobjects now, X -> 2
 * Moore machines: For state type Q and input type S, Q × S -> Q
   * Moore transducers: [Q × S, Q] -> [Q × S, Q]
 * Mealy machines: For state type Q, input type S, and output type L, Q × S -> Q × L
@@ -56,3 +55,4 @@
   * We now can iter-maybe, short-circuiting evaluation
   * We need to iter-maybe but also keep track of how many steps were taken
     * Instead of X -> [N, Y + 1], we need X -> [N, N x (Y + 1)]
+* ulimit jellification?