• R/O
  • HTTP
  • SSH
  • HTTPS

提交

标签
No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#objective-cqtwindows誰得cocoapythonphprubygameguibathyscaphec翻訳omegat計画中(planning stage)frameworktwittertestdomvb.netdirectxbtronarduinopreviewerゲームエンジン

A categorical programming language


Commit MetaInfo

修订版0720745c874c9b6d5eaf71ce7df436ecae2ace17 (tree)
时间2022-06-14 14:44:52
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Jet (pair snd fst) to swap.

更改概述

差异

--- a/cammy-rpy/cammylib/arrows.py
+++ b/cammy-rpy/cammylib/arrows.py
@@ -59,6 +59,16 @@ class Dup(Arrow):
5959 pair = cs.functor("pair", [x, x])
6060 return x, pair
6161
62+class Swap(Arrow):
63+ _immutable_ = True
64+ def compile(self, compiler): compiler.pairSwap()
65+ def types(self, cs):
66+ x = cs.fresh()
67+ y = cs.fresh()
68+ xy = cs.functor("pair", [x, y])
69+ yx = cs.functor("pair", [y, x])
70+ return xy, yx
71+
6272 class Pair(Arrow):
6373 _immutable_ = True
6474 def __init__(self, f, g):
@@ -418,6 +428,7 @@ unaryFunctors = {
418428 "fst": First(),
419429 "snd": Second(),
420430 "dup": Dup(),
431+ "swap": Swap(),
421432 "left": Left(),
422433 "right": Right(),
423434 "either": Either(),
--- a/cammy-rpy/cammylib/cam.py
+++ b/cammy-rpy/cammylib/cam.py
@@ -50,6 +50,7 @@ termOps = [
5050 TermOp("snd", lambda term: term.second()),
5151 TermOp("branch", lambda term: L(T()) if term.b() else R(T())),
5252 TermOp("dup", lambda term: P(term, term)),
53+ TermOp("pairSwap", lambda term: P(term.second(), term.first())),
5354 # Custom structure term ops.
5455 TermOp("left", lambda term: L(term)),
5556 TermOp("right",lambda term: R(term)),
--- a/hive/pair/dup.cammy
+++ b/hive/pair/dup.cammy
@@ -1,3 +1,3 @@
1-dup
1+(pair id id)
22
33 The [diagonal map](https://ncatlab.org/nlab/show/diagonal+morphism).
--- a/hive/swap.cammy
+++ /dev/null
@@ -1 +0,0 @@
1-pair/swap
\ No newline at end of file
--- a/jelly/src/main.rs
+++ b/jelly/src/main.rs
@@ -111,10 +111,13 @@ fn main() -> std::io::Result<()> {
111111
112112 // jet for pair/dup
113113 rw!("pair-dup-jet"; "(pair id id)" => "dup"),
114+ // jet for pair/swap
115+ rw!("pair-swap-jet"; "(pair snd fst)" => "swap"),
116+ rw!("dup-absorb-swap"; "(comp dup swap)" => "dup"),
114117
115118 // This implies the old rule pair-swap-invo: (comp pair/swap pair/swap) => id
116119 // So, like pair-swap-invo, this turns braided products into symmetric products.
117- rw!("pair-swap-pair"; "(comp (pair ?f ?g) (pair snd fst))" => "(pair ?g ?f)"),
120+ rw!("pair-swap-pair"; "(comp (pair ?f ?g) swap)" => "(pair ?g ?f)"),
118121
119122 // free for left
120123 rw!("left-elim-case"; "(comp left (case ?f ?g))" => "?f"),
@@ -165,14 +168,14 @@ fn main() -> std::io::Result<()> {
165168 rw!("bool-not-invo"; "(comp not not)" => "id"),
166169
167170 // IEEE 754 addition
168- rw!("f-add-comm"; "(comp (pair snd fst) f-add)" => "f-add"),
171+ rw!("f-add-comm"; "(comp swap f-add)" => "f-add"),
169172 rw!("f-add-unit-left"; "(comp (pair ?f f-zero) f-add)" => "?f"),
170173 rw!("f-add-unit-right"; "(comp (pair f-zero ?f) f-add)" => "?f"),
171174 rw!("f-add-negate-left"; "(comp (pair id f-negate) f-add)" => "f-zero"),
172175 rw!("f-add-negate-right"; "(comp (pair f-negate id) f-add)" => "f-zero"),
173176
174177 // IEEE 754 multiplication
175- rw!("f-mul-comm"; "(comp (pair snd fst) f-mul)" => "f-mul"),
178+ rw!("f-mul-comm"; "(comp swap f-mul)" => "f-mul"),
176179 rw!("f-mul-unit-left"; "(comp (pair ?f f-one) f-mul)" => "?f"),
177180 rw!("f-mul-unit-right"; "(comp (pair f-one ?f) f-mul)" => "?f"),
178181
--- a/test_canonical.json
+++ b/test_canonical.json
@@ -2,7 +2,7 @@
22 ["X", "X", ["id"]],
33 ["(pair X Y)", "X", ["fst"]],
44 ["X", "(pair X X)", ["dup"]],
5- ["(pair X Y)", "(pair Y X)", ["(pair snd fst)"]],
5+ ["(pair X Y)", "(pair Y X)", ["swap"]],
66 ["(pair (hom X Y) X)", "Y", ["(uncurry id)"]],
77 ["1", "2", ["t", "f"]],
88 ["1", "(list X)", ["nil", "(comp ignore nil)"]]