A categorical programming language
| 修订版 | 41583a2fd06df8bb86bcd9889d5dc3a0e3ba60f3 (tree) |
|---|---|
| 时间 | 2021-08-26 06:35:07 |
| 作者 | Corbin <cds@corb...> |
| Commiter | Corbin |
Remove bootstrap notes.
Literally everything of interest is archived at
https://esolangs.org/w/index.php?title=Cammy&oldid=87614 and hopefully
the current version of the page is even more informative and helpful.
cammy.txt| @@ -1,79 +0,0 @@ | ||
| 1 | -As usual, we implement a syntax for a topos with coproducts and an NNO. The | |
| 2 | -category is symmetric monoidal, with explicit reassociators. | |
| 3 | - | |
| 4 | -Let: | |
| 5 | - | |
| 6 | -* metavariables: X, Y, W | |
| 7 | -* terminal object: 1 | |
| 8 | -* products: Given X and Y, X × Y | |
| 9 | -* sums: Given X and Y, X + Y | |
| 10 | -* internal homs: Given X and Y, [X, Y] | |
| 11 | -* object of truth values: Ω | |
| 12 | -* NNO: N | |
| 13 | - | |
| 14 | -Our combinators, given with categorical datatypes, are: | |
| 15 | - | |
| 16 | -id : X → X | |
| 17 | -Given f : X → Y and g : Y → W, (comp f g) : X → W | |
| 18 | - | |
| 19 | -ignore : X → 1 (*) | |
| 20 | - | |
| 21 | -fst : X × Y → X (*) | |
| 22 | -snd : X × Y → Y (*) | |
| 23 | -Given f : X → Y and g : X → W, (pair f g) : X → Y × W | |
| 24 | - | |
| 25 | -left : X → X + Y | |
| 26 | -right : Y → X + Y | |
| 27 | -Given f : X → W and g : Y → W, (case f g): X + Y → W | |
| 28 | - | |
| 29 | -assl : X × (Y × W) → (X × Y) × W | |
| 30 | -assr : (X × Y) × W → X × (Y × W) | |
| 31 | - | |
| 32 | -swap : X × Y → Y × X | |
| 33 | - | |
| 34 | -dup = pair(id, id) : X → X × X | |
| 35 | - | |
| 36 | -Given f : X × Y → W, (curry f) : X → [Y, W] | |
| 37 | -Given f : X → [Y, W], (uncurry f) : X × Y → W | |
| 38 | -app = uncurry(id) : [X, Y] × X → Y | |
| 39 | -Given f : X → Y, (name f) = (curry (comp snd f)) : 1 → [X, Y] | |
| 40 | - | |
| 41 | -t : 1 → Ω | |
| 42 | -f : 1 → Ω | |
| 43 | -not : Ω → Ω (*) | |
| 44 | -conj : Ω × Ω → Ω | |
| 45 | -disj : Ω × Ω → Ω | |
| 46 | - | |
| 47 | -zero : 1 → N | |
| 48 | -succ : N → N | |
| 49 | -Given x : 1 → X and f : X → X, (pr x f) : N → X | |
| 50 | - | |
| 51 | -nil : 1 → [X] | |
| 52 | -cons : X × [X] → [X] | |
| 53 | -Given x : 1 → Y and f : X × Y → Y, (fold x f) : [X] → Y | |
| 54 | -Given f : X → Y, (map f) = (fold nil (comp (pair (comp fst f) snd) cons)) : [X] → [Y] | |
| 55 | - | |
| 56 | -Combinators with (*) are provided by OCaml by default; the others are in a | |
| 57 | -stub module. Type-checking is achieved by copying the combinators into | |
| 58 | -an OCaml expression; compilation is achieved by copying the combinators into | |
| 59 | -a CHICKEN Scheme expression. | |
| 60 | - | |
| 61 | -In terms of the "principal programming paradigms" | |
| 62 | -https://www.info.ucl.ac.be/~pvr/paradigmsDIAGRAMeng101.pdf, Cammy is a | |
| 63 | -"functional programming" language; it possesses the ability to encode | |
| 64 | -arbitrary functions via topos theory. Later improvements may shift Cammy to | |
| 65 | -the "monotonic dataflow programming", "multi-agent dataflow programming", or | |
| 66 | -"event-loop programming" paradigms. | |
| 67 | - | |
| 68 | -In terms of the common taxonomy of type systems, exhibited for tutorial at | |
| 69 | -https://www.cs.uaf.edu/users/chappell/public_html/class/2018_spr/cs331/docs/types_primer.html, | |
| 70 | -Cammy's current toolchain implements a static, implicit, structural, sound | |
| 71 | -type system. For a classic example, the program (comp dup apply), sometimes | |
| 72 | -called the "Turing bird", will be rejected by the toolchain as ill-typed. | |
| 73 | - | |
| 74 | -In terms of the taxonomy of desugaring systems | |
| 75 | -https://cs.brown.edu/research/pubs/theses/phd/2018/pombrio.justin.pdf, Cammy | |
| 76 | -does not implement desugaring. Any nullary sugar can be implemented as plain | |
| 77 | -Cammy programs. Every algebraic equality in Cammy's combinators corresponds to | |
| 78 | -a desugaring rule in the toolchain, but those equalities are not taxonomically | |
| 79 | -syntactic sugar. |
Fork