A categorical programming language
修订版 | 5fd12d13873df41116bc348843c73a8384ddc1b1 (tree) |
---|---|
时间 | 2022-07-10 12:56:20 |
作者 | Corbin <cds@corb...> |
Commiter | Corbin |
Specialize (uncurry id) to app.
@@ -3,7 +3,7 @@ | ||
3 | 3 | ["(pair X Y)", "X", ["fst"]], |
4 | 4 | ["X", "(pair X X)", ["dup"]], |
5 | 5 | ["(pair X Y)", "(pair Y X)", ["swap"]], |
6 | - ["(pair (hom X Y) X)", "Y", ["(uncurry id)"]], | |
6 | + ["(pair (hom X Y) X)", "Y", ["app"]], | |
7 | 7 | ["1", "2", ["t", "f"]], |
8 | 8 | ["1", "(list X)", ["nil", "(comp ignore nil)"]] |
9 | 9 | ] |
@@ -152,6 +152,20 @@ class Uncurry(Arrow): | ||
152 | 152 | cs.unify(fcod, cs.functor("hom", [x, y])) |
153 | 153 | return cs.functor("pair", [fdom, x]), y |
154 | 154 | |
155 | +class App(Arrow): | |
156 | + _immutable_ = True | |
157 | + def compile(self, compiler): | |
158 | + compiler.push() | |
159 | + compiler.snd() | |
160 | + compiler.swap() | |
161 | + compiler.fst() | |
162 | + # app == (uncurry id); id would go here | |
163 | + compiler.app() | |
164 | + def types(self, cs): | |
165 | + x = cs.fresh() | |
166 | + y = cs.fresh() | |
167 | + return cs.functor("pair", [cs.functor("hom", [x, y]), x]), y | |
168 | + | |
155 | 169 | class Either(Arrow): |
156 | 170 | _immutable_ = True |
157 | 171 | def compile(self, compiler): compiler.branch() |
@@ -392,6 +406,7 @@ unaryFunctors = { | ||
392 | 406 | "snd": Second(), |
393 | 407 | "dup": Dup(), |
394 | 408 | "swap": Swap(), |
409 | + "app": App(), | |
395 | 410 | "left": Left(), |
396 | 411 | "right": Right(), |
397 | 412 | "either": Either(), |
@@ -39,12 +39,30 @@ class PlaintextTypeFormatter(TypeFormatter): | ||
39 | 39 | class PromptContext(object): |
40 | 40 | mostRecentExpr = None |
41 | 41 | |
42 | +def printDuration(duration): | |
43 | + unit = "s" | |
44 | + if duration < 1.0: | |
45 | + duration *= 1000 | |
46 | + unit = "ms" | |
47 | + if duration < 1.0: | |
48 | + duration *= 1000 | |
49 | + unit = "µs" | |
50 | + print "(%f %s)" % (duration, unit) | |
51 | + | |
42 | 52 | def printElement(cam): |
53 | + start = time.time() | |
43 | 54 | print cam.execute(T()).asStr() |
55 | + printDuration(time.time() - start) | |
44 | 56 | |
45 | 57 | def printSequence(cam): |
46 | - for i in range(5): | |
58 | + start = time.time() | |
59 | + duration = 0.0 | |
60 | + for i in range(10): | |
47 | 61 | print i, "|->", cam.execute(N(i)).asStr() |
62 | + duration = time.time() - start | |
63 | + if duration > 1.0: | |
64 | + break | |
65 | + printDuration(duration) | |
48 | 66 | |
49 | 67 | def command(hive, code, line, context): |
50 | 68 | # XXX code e: Edit a file |
@@ -58,32 +76,20 @@ def command(hive, code, line, context): | ||
58 | 76 | cs = ConstraintStore() |
59 | 77 | domain, codomain = arrow.types(cs) |
60 | 78 | |
61 | - start = time.time() | |
62 | 79 | # If the arrow is polymorphic, monomorphize it. |
63 | 80 | try: |
64 | 81 | cs.unify(domain, cs.concrete("1")) |
65 | 82 | # Compile the arrow and run it. |
66 | 83 | cam = compileArrow(arrow) |
67 | - start = time.time() | |
68 | 84 | printElement(cam) |
69 | 85 | except UnificationFailed: |
70 | 86 | # Maybe it's a sequence? |
71 | 87 | try: |
72 | 88 | cs.unify(domain, cs.concrete("N")) |
73 | 89 | cam = compileArrow(arrow) |
74 | - start = time.time() | |
75 | 90 | printSequence(cam) |
76 | 91 | except UnificationFailed: |
77 | 92 | print "Couldn't unify domain with 1 or N, so can't display this element" |
78 | - duration = time.time() - start | |
79 | - unit = "s" | |
80 | - if duration < 1.0: | |
81 | - duration *= 1000 | |
82 | - unit = "ms" | |
83 | - if duration < 1.0: | |
84 | - duration *= 1000 | |
85 | - unit = "µs" | |
86 | - print "(%f %s)" % (duration, unit) | |
87 | 93 | elif code == "n": |
88 | 94 | # Normalize an arrow. |
89 | 95 | sexp, trail = parse(line) |
@@ -0,0 +1 @@ | ||
1 | +(comp (pair/tensor (pair/mapfst f-recip) (v2/map (comp nat/to-f dup))) (comp (v2/map2 (comp pair/assl f/mad)) (pair/mapsnd f-recip))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp (fold (pair nil @0) (pair (pair/of cons (comp sndsnd @1) sndfst) (pair/of @2 sndsnd fst))) fst) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp (pair/of disj f-lt (comp swap f-lt)) not) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp f-zero f-recip) |
@@ -0,0 +1 @@ | ||
1 | +(comp (pair/mapfst f-mul) f-add) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(fold f-one f-mul) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pr (fun/name id) (curry (comp (pair/mapsnd (comp list/uncons (case snd nil))) app))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp (pr (pair @0 zero) (pair @1 (comp snd succ))) fst) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp nat/double succ) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(v2/map2 f-add) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair f-one f-zero) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair f-zero f-zero) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp @0 (case id @1)) | |
\ No newline at end of file |
@@ -141,13 +141,15 @@ fn main() -> std::io::Result<()> { | ||
141 | 141 | rw!("curry-uncurry-cancel"; "(uncurry (curry ?f))" => "?f"), |
142 | 142 | rw!("uncurry-curry-cancel"; "(curry (uncurry ?f))" => "?f"), |
143 | 143 | |
144 | - rw!("beta-full"; "(comp (pair (comp ?x (curry ?f)) ?y) (uncurry id))" => "(comp (pair ?x ?y) ?f)"), | |
144 | + // jet for app | |
145 | + rw!("app-jet"; "(uncurry id)" => "app"), | |
146 | + rw!("beta-full"; "(comp (pair (comp ?x (curry ?f)) ?y) app)" => "(comp (pair ?x ?y) ?f)"), | |
145 | 147 | // Cousineau, Curien, & Mauny 1987 |
146 | 148 | // beta-full when ?x is id |
147 | - rw!("beta"; "(comp (pair (curry ?f) ?y) (uncurry id))" => "(comp (pair id ?y) ?f)"), | |
149 | + rw!("beta"; "(comp (pair (curry ?f) ?y) app)" => "(comp (pair id ?y) ?f)"), | |
148 | 150 | // Hagino 1987 |
149 | 151 | // This is a more powerful form of beta when ?x is (uncurry ...) |
150 | - rw!("beta-fuse"; "(comp (pair ?x ?y) (uncurry ?f))" => "(comp (pair (comp ?x ?f) ?y) (uncurry id))"), | |
152 | + rw!("beta-fuse"; "(comp (pair ?x ?y) (uncurry ?f))" => "(comp (pair (comp ?x ?f) ?y) app)"), | |
151 | 153 | |
152 | 154 | rw!("curry-const"; "(comp ?f (curry (comp fst ?g)))" => "(curry (comp fst (comp ?f ?g)))"), |
153 | 155 | // curry-const when ?g is id |
@@ -162,7 +164,7 @@ fn main() -> std::io::Result<()> { | ||
162 | 164 | rw!("nat-shift-pr-endo"; "(comp (pr ?x ?f) ?f)" => "(pr (comp ?x ?f) ?f)"), |
163 | 165 | |
164 | 166 | // jet for nat/add |
165 | - rw!("nat-add-jet"; "(pr (curry snd) (curry (comp (uncurry id) succ)))" => "(curry n-add)"), | |
167 | + rw!("nat-add-jet"; "(pr (curry snd) (curry (comp app succ)))" => "(curry n-add)"), | |
166 | 168 | // jet for nat/pred-maybe |
167 | 169 | rw!("nat-pred-maybe-jet"; "(pr right (comp (case succ zero) left))" => "n-pred-maybe"), |
168 | 170 |