提交: 62cedf9d54c7cdb27e2233e142f1a8bb686b7c6e - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: 62cedf9d54c7cdb27e2233e142f1a8bb686b7c6e (tree)
• 时间: 2021-08-17 00:49:42
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Clean up and start thinking about publication.

更改概述

• modified: cammy.txt
• modified: shell.nix
• modified: todo.txt

差异

--- a/cammy.txt
+++ b/cammy.txt
@@ -14,17 +14,17 @@ Let:
 Our combinators, given with categorical datatypes, are:
 
 id : X → X
-Given f : X → Y and g : Y → W, comp(f, g) : X → W
+Given f : X → Y and g : Y → W, (comp f g) : X → W
 
 ignore : X → 1 (*)
 
 fst : X × Y → X (*)
 snd : X × Y → Y (*)
-Given f : X → Y and g : X → W, pair(f, g) : X → Y × W
+Given f : X → Y and g : X → W, (pair f g) : X → Y × W
 
 left : X → X + Y
 right : Y → X + Y
-Given f : X → W and g : Y → W, case(f, g): X + Y → W
+Given f : X → W and g : Y → W, (case f g): X + Y → W
 
 assl : X × (Y × W) → (X × Y) × W
 assr : (X × Y) × W → X × (Y × W)
@@ -33,10 +33,10 @@ swap : X × Y → Y × X
 
 dup = pair(id, id) : X → X × X
 
-Given f : X × Y → W, curry(f) : X → [Y, W]
-Given f : X → [Y, W], uncurry(f) : X × Y → W
+Given f : X × Y → W, (curry f) : X → [Y, W]
+Given f : X → [Y, W], (uncurry f) : X × Y → W
 app = uncurry(id) : [X, Y] × X → Y
-Given f : X → Y, name(f) = curry(comp(snd, f)) : 1 → [X, Y]
+Given f : X → Y, (name f) = (curry (comp snd f)) : 1 → [X, Y]
 
 t : 1 → Ω
 f : 1 → Ω
@@ -46,12 +46,12 @@ disj : Ω × Ω → Ω
 
 zero : 1 → N
 succ : N → N
-Given x : 1 → X and f : X → X, pr(x, f) : N → X
+Given x : 1 → X and f : X → X, (pr x f) : N → X
 
 nil : 1 → [X]
 cons : X × [X] → [X]
-Given x : 1 → Y and f : X × Y → Y, fold(x, f) : [X] → Y
-Given f : X → Y, map(f) = fold(nil, comp(pair(comp(fst, f), snd), cons)) : [X] → [Y]
+Given x : 1 → Y and f : X × Y → Y, (fold x f) : [X] → Y
+Given f : X → Y, (map f) = (fold nil (comp (pair (comp fst f) snd) cons)) : [X] → [Y]
 
 Combinators with (*) are provided by OCaml by default; the others are in a
 stub module. Type-checking is achieved by copying the combinators into

--- a/shell.nix
+++ b/shell.nix
@@ -14,5 +14,7 @@ in pkgs.stdenv.mkDerivation {
     ocamlPackages.utop
     # running compile.sh
     ocaml
+    # publishing
+    mktorrent
   ];
 }

--- a/todo.txt
+++ b/todo.txt
@@ -3,3 +3,5 @@
 * list/tail : [X] → [X]
 * list/unfold : [Y, X × Y + 1] → [Y, [X]]
 * rat
+* jelly: zero (pr ...), succ (pr ...), nil (fold ...), cons (fold ...) can all
+  be unrolled one step, allowing for loops to be inlined