提交: 5ce1d98b359ee6713b42fc7ae9185980024ecf9b - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: 5ce1d98b359ee6713b42fc7ae9185980024ecf9b (tree)
• 时间: 2022-03-30 09:21:26
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Implement the Yoneda combinators and other stuff.

更改概述

• add: hive/dynamics.cammy
• add: hive/extnat/about.md
• add: hive/extnat/pred.cammy
• add: hive/extnat/succ.cammy
• modified: hive/fun/int-comp.cammy
• add: hive/fun/unname.cammy
• modified: hive/list/scan.cammy
• modified: hive/monads/maybe/int-comp.cammy
• add: hive/poly/about.md
• add: hive/poly/const.cammy
• add: hive/poly/order.cammy
• add: hive/poly/zero.cammy
• add: hive/sum/assl.cammy
• add: hive/sum/assr.cammy
• add: hive/yoneda/about.md
• add: hive/yoneda/embed.cammy
• add: hive/yoneda/lift.cammy
• delete: hive/{fun => pair}/assl.cammy
• delete: hive/{fun => pair}/assr.cammy
• delete: hive/{list => poly}/horner.cammy
• modified: movelist/test.json
• modified: todo.txt

差异

--- /dev/null
+++ b/hive/dynamics.cammy
@@ -0,0 +1,4 @@
+(pair/mapfst (comp (pair (fun/name @0) id) fun/int-comp))
+
+The dynamics of a deterministic automaton. The second component of the pair is
+left free, but usually is a status value, like a Boolean.

--- /dev/null
+++ b/hive/extnat/about.md
@@ -0,0 +1,3 @@
+The type $\mathbb{N} + 1$ can be interpreted as $\mathbb{\tilde{N}}$, the
+type of extended natural numbers, via [one-point
+compactification](https://ncatlab.org/nlab/show/one-point+compactification).

--- /dev/null
+++ b/hive/extnat/pred.cammy
@@ -0,0 +1,6 @@
+(comp
+  (sum/mapleft nat/pred-maybe)
+  (comp sum/assr (comp (sum/mapright sum/swap) sum/assl)))
+
+The predecessor of an extended natural number. The extra point signals when
+the input is zero.

--- /dev/null
+++ b/hive/extnat/succ.cammy
@@ -0,0 +1,4 @@
+(sum/mapleft succ)
+
+The successor of an extended natural number is also an extended natural
+number.

--- a/hive/fun/int-comp.cammy
+++ b/hive/fun/int-comp.cammy
@@ -1,3 +1,3 @@
-(curry (comp (comp fun/assr (pair fst (comp snd fun/app))) fun/app))
+(curry (comp (comp pair/assr (pair fst (comp snd fun/app))) fun/app))
 
 An internalized version of composition.

--- /dev/null
+++ b/hive/fun/unname.cammy
@@ -0,0 +1,3 @@
+(comp (pair ignore id) (uncurry @0))
+
+Reference an arrow by name.

--- a/hive/list/scan.cammy
+++ b/hive/list/scan.cammy
@@ -1,4 +1,3 @@
-(comp (fold
-  (pair @0 nil)
-  (comp (comp fun/assl (pair @1 snd)) (pair fst cons)))
-snd)
+(comp (fold (pair @0 nil) (comp (comp pair/assl (pair @1 snd)) (pair fst cons))) snd)
+
+

--- a/hive/monads/maybe/int-comp.cammy
+++ b/hive/monads/maybe/int-comp.cammy
@@ -1,7 +1,4 @@
-(curry
-  (comp
-    (comp fun/assr (pair fst (comp snd fun/app)))
-    (comp fun/distribr (case fun/app (comp ignore right)))))
+(curry (comp (comp pair/assr (pair fst (comp snd fun/app))) (comp fun/distribr (case fun/app (comp ignore right)))))
 
 An internalized version of composition in the Kleisli category for the maybe
 monad.

--- /dev/null
+++ b/hive/poly/about.md
@@ -0,0 +1,2 @@
+The type $[\mathbb{N}]$ can be interpreted as the type of polynomials with
+coefficients in $\mathbb{N}$.

--- /dev/null
+++ b/hive/poly/const.cammy
@@ -0,0 +1,3 @@
+(comp (pair id (fun/const nil)) cons)
+
+A constant polynomial which always evaluating to the given natural number.

--- /dev/null
+++ b/hive/poly/order.cammy
@@ -0,0 +1,3 @@
+(comp list/len nat/pred)
+
+The largest exponent in a polynomial. 

--- /dev/null
+++ b/hive/poly/zero.cammy
@@ -0,0 +1,3 @@
+nil
+
+The zero polynomial.

--- /dev/null
+++ b/hive/sum/assl.cammy
@@ -0,0 +1,3 @@
+(case (comp left left) (case (comp right left) right))
+
+Reassociate a triple sum to the left.

--- /dev/null
+++ b/hive/sum/assr.cammy
@@ -0,0 +1,3 @@
+(case (case left (comp left right)) (comp right right))
+
+Reassociate a triple sum to the right.

--- /dev/null
+++ b/hive/yoneda/about.md
@@ -0,0 +1,2 @@
+Given some fixed arrow $f : X \to Y$, its Yoneda embedding can be realized by
+the type $\hat{f} : (X^Z) \to (Y^Z)$.

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

--- /dev/null
+++ b/hive/yoneda/lift.cammy
@@ -0,0 +1,3 @@
+(fun/unname (comp (fun/const (fun/name id)) @0))
+
+Undo the Yoneda embedding.

--- a/movelist/test.json
+++ b/movelist/test.json
@@ -3,7 +3,8 @@
     ["first component", "(pair X Y)", "X"],
     ["right unitor", "X", "(pair X 1)"],
     ["name of id", "1", "(hom X X)"],
-    ["associator", "(pair (pair X Y) Z)", "(pair X (pair Y Z))"],
+    ["product associator", "(pair (pair X Y) Z)", "(pair X (pair Y Z))"],
+    ["sum associator", "(sum (sum X Y) Z)", "(sum X (sum Y Z))"],
     ["application", "(pair (hom X Y) X)", "Y"],
     ["braiding", "(pair X Y)", "(pair Y X)"],
     ["distributivity", "(sum (pair X Y) (pair X Z))", "(pair X (sum Y Z))"],

--- a/todo.txt
+++ b/todo.txt
@@ -60,3 +60,4 @@
   * 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?
+* formal power series N -> Q