A categorical programming language
Revisão | 545291094d5b7db322b545c1557fd4c788745f6b (tree) |
---|---|
Hora | 2022-07-25 06:28:24 |
Autor | Corbin <cds@corb...> |
Commiter | Corbin |
Damn you're fast.
@@ -1,8 +1,11 @@ | ||
1 | 1 | from cammylib.sexp import sexp |
2 | 2 | |
3 | 3 | |
4 | -class CammyParser(object): | |
4 | +class ParseError(Exception): | |
5 | + def __init__(self, message): | |
6 | + self.message = message | |
5 | 7 | |
8 | +class CammyParser(object): | |
6 | 9 | def __init__(self, s): |
7 | 10 | self._i = 0 |
8 | 11 | self._s = s |
@@ -10,8 +13,11 @@ class CammyParser(object): | ||
10 | 13 | def position(self): |
11 | 14 | return self._i |
12 | 15 | |
16 | + def hasMore(self): | |
17 | + return self._i < len(self._s) | |
18 | + | |
13 | 19 | def eatWhitespace(self): |
14 | - while self._i < len(self._s) and self._s[self._i] in (" ", "\n"): | |
20 | + while self.hasMore() and self._s[self._i] in (" ", "\n"): | |
15 | 21 | self._i += 1 |
16 | 22 | |
17 | 23 | def canAndDoesEat(self, c): |
@@ -23,7 +29,7 @@ class CammyParser(object): | ||
23 | 29 | |
24 | 30 | def takeName(self): |
25 | 31 | start = self._i |
26 | - while self._i < len(self._s) and self._s[self._i] not in (")", "(", " ", "\n"): | |
32 | + while self.hasMore() and self._s[self._i] not in (")", "(", " ", "\n"): | |
27 | 33 | self._i += 1 |
28 | 34 | stop = self._i |
29 | 35 | return self._s[start:stop] |
@@ -42,12 +48,15 @@ class CammyParser(object): | ||
42 | 48 | return sexp.Atom(symbol) |
43 | 49 | |
44 | 50 | def startFunctor(self): |
51 | + start = self._i | |
45 | 52 | head = self.takeName() |
46 | 53 | self.eatWhitespace() |
47 | 54 | args = [] |
48 | 55 | while not self.canAndDoesEat(')'): |
49 | 56 | args.append(self.takeExpression()) |
50 | 57 | self.eatWhitespace() |
58 | + if not self.hasMore(): | |
59 | + raise ParseError("Unterminated functor starting at %d" % start) | |
51 | 60 | return sexp.Functor(head, args) |
52 | 61 | |
53 | 62 |
@@ -6,6 +6,7 @@ class UnificationFailed(Exception): | ||
6 | 6 | |
7 | 7 | def occursCheck(index, var): |
8 | 8 | "If an index occurs in a variable, raise an error." |
9 | + # print "occurs check: does", index, "occur in", var.asStr() | |
9 | 10 | if var.occurs(index): |
10 | 11 | raise UnificationFailed("Occurs check: %d in %s" % |
11 | 12 | (index, var.asStr())) |
@@ -27,19 +28,23 @@ class ConstraintStore(object): | ||
27 | 28 | rv = self.i |
28 | 29 | self.i += 1 |
29 | 30 | self.constraints.append(sexp.Hole(rv)) |
31 | + # print "fresh", rv | |
30 | 32 | return rv |
31 | 33 | |
32 | 34 | def concrete(self, symbol): |
33 | 35 | rv = self.i |
34 | 36 | self.i += 1 |
35 | 37 | self.constraints.append(sexp.Atom(symbol)) |
38 | + # print "concrete", rv, "|->", symbol | |
36 | 39 | return rv |
37 | 40 | |
38 | 41 | def functor(self, constructor, arguments): |
39 | 42 | rv = self.i |
40 | 43 | self.i += 1 |
41 | 44 | args = [sexp.Hole(arg) for arg in arguments] |
42 | - self.constraints.append(sexp.Functor(constructor, args)) | |
45 | + functor = sexp.Functor(constructor, args) | |
46 | + self.constraints.append(functor) | |
47 | + # print "functor", rv, "|->", functor.asStr() | |
43 | 48 | return rv |
44 | 49 | |
45 | 50 | def walk(self, i): |
@@ -10,7 +10,7 @@ from cammylib.hive import Hive, MissingAtom | ||
10 | 10 | from cammylib.djinn import askDjinn |
11 | 11 | from cammylib.elements import T, N |
12 | 12 | from cammylib.jelly import jellify |
13 | -from cammylib.parser import parse, parseTypes | |
13 | +from cammylib.parser import parse, parseTypes, ParseError | |
14 | 14 | from cammylib.types import ConstraintStore, TypeExtractor, TypeFormatter, UnificationFailed |
15 | 15 | |
16 | 16 | LINE_BUFFER_LENGTH = 1024 |
@@ -137,10 +137,17 @@ def repl(hive, stdin, stdout): | ||
137 | 137 | if line.startswith(":"): |
138 | 138 | if len(line) < 2: |
139 | 139 | print "Not a full command" |
140 | - command(hive, line[1], line[3:], context) | |
140 | + try: | |
141 | + command(hive, line[1], line[3:], context) | |
142 | + except ParseError as pe: | |
143 | + print "Parse error:", pe.message | |
141 | 144 | continue |
142 | 145 | lineIsAtom = not line.startswith("(") |
143 | - sexp, trail = parse(line) | |
146 | + try: | |
147 | + sexp, trail = parse(line) | |
148 | + except ParseError as pe: | |
149 | + print "Parse error:", pe.message | |
150 | + continue | |
144 | 151 | # Save the original expr for next time. |
145 | 152 | mostRecentExpr = sexp |
146 | 153 | try: |
@@ -0,0 +1 @@ | ||
1 | +(comp (pair/mapsnd either) (comp fun/distribr (sum/par fst fst))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp (comp (fun/graph @0) (pair/mapsnd either)) (comp fun/distribr (case (comp fst @1) (comp fst @2)))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry fst) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (curry (comp (pair (pair/of app fstfst snd) (pair/of app fstsnd snd)) app))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (comp (pair app snd) app)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair fst @0) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair/of app id (fun/const @0)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (curry (comp (pair snd (comp fst @0)) app))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair (curry id) id) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(bool/ternary nat/even? (comp nat-div2 fst) (comp nat-mul3 succ)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(monad-choose monads/list/zero monads/list/unit monads/list/add) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(fold nil list/append) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(fold @0 @1) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp (fold (pair nil @0) (pair (pair/of cons fst sndfst) @1)) snd) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(list/para (comp (pair (fun/const nil) nil) cons) (l (l fst sndfst) sndsnd)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(fold @0 (comp (pair/mapfst @1) @2)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (comp app app)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (comp (comp (pair (pair fstfst snd) (pair fstsnd snd)) (v2/map app)) disj)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (comp swap snd)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (comp (pair app snd) app)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry @0) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(fun/name (fun/const f)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair fstfst (pair/of @0 fstsnd snd)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair/mapfst @0) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair id (fun/const @0)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +dup | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +nat/add | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +zero | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +nat/mul | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +nat/1 | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pr (pair zero f) (comp bool-sum (case (pair succ (fun/const f)) (pair id (fun/const t))))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pair/of nat/mul id (fun/const nat/3)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(pr @0 @1) | |
\ No newline at end of file |
@@ -1 +1 @@ | ||
1 | -(comp (pr (pair @0 zero) (pair @1 (comp snd succ))) fst) | |
\ No newline at end of file | ||
1 | +(comp (pr (pair zero @0) (pair (comp fst succ) @1)) snd) | |
\ No newline at end of file |
@@ -0,0 +1,12 @@ | ||
1 | +(fold right | |
2 | + (comp | |
3 | + (comp | |
4 | + fun/distribr | |
5 | + (case | |
6 | + (pair | |
7 | + (comp sndfst succ) | |
8 | + (comp (comp pair/assl (pair/mapfst nat/mul)) cons)) | |
9 | + (comp snd (pair nat/1 nil)))) | |
10 | + left)) | |
11 | + | |
12 | +The derivative of a polynomial, which itself is a polynomial. |
@@ -0,0 +1 @@ | ||
1 | +(comp poly/deriv (case snd nil)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(monad-choose monads/subset/zero (monads/subset/unit @0) monads/subset/add) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp list/range (subset-choose nat/eq?)) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(curry (comp swap (uncurry @0))) | |
\ No newline at end of file |
@@ -0,0 +1 @@ | ||
1 | +(comp (pair/of nat/mul id succ) (comp nat-div2 fst)) | |
\ No newline at end of file |
@@ -121,8 +121,8 @@ fn main() -> std::io::Result<()> { | ||
121 | 121 | rw!("swap-fst"; "(comp swap fst)" => "snd"), |
122 | 122 | rw!("swap-snd"; "(comp swap snd)" => "fst"), |
123 | 123 | |
124 | - // This implies the old rule pair-swap-invo: (comp pair/swap pair/swap) => id | |
125 | - // So, like pair-swap-invo, this turns braided products into symmetric products. | |
124 | + rw!("pair-swap-invo"; "(comp swap swap)" => "id"), | |
125 | + // Like pair-swap-invo, this turns braided products into symmetric products. | |
126 | 126 | rw!("pair-swap-pair"; "(comp (pair ?f ?g) swap)" => "(pair ?g ?f)"), |
127 | 127 | |
128 | 128 | // free for left |
@@ -1,5 +1,6 @@ | ||
1 | 1 | [ |
2 | 2 | ["identity", "X", "X"], |
3 | + ["K", "X", "(hom Y X)"], | |
3 | 4 | ["first component", "(pair X Y)", "X"], |
4 | 5 | ["right unitor", "X", "(pair X 1)"], |
5 | 6 | ["name of id", "1", "(hom X X)"], |
@@ -42,8 +42,6 @@ | ||
42 | 42 | * Maybe nat/ -> n/ for consistency with f/ |
43 | 43 | * bool/ -> b/ or bool -> 2/ ? |
44 | 44 | * Predicates should have a trailing question mark |
45 | - * e.g. nat/is_zero -> nat/zero? | |
46 | - * done | |
47 | 45 | * This means f-lt should be f-lt? |
48 | 46 | * fun/name should always start from 1 |
49 | 47 | * Requires changing some callers |
@@ -106,6 +104,7 @@ | ||
106 | 104 | * fun/precomp is an ingredient of CPS transformation |
107 | 105 | * https://okmij.org/ftp/continuations/undelimited.html |
108 | 106 | * It's about time to rewrite the multisampling logic in Cammy |
107 | + * Mostly just needs pixel radius to be passed to image | |
109 | 108 | * Some basic dependent types |
110 | 109 | * Type-level arithmetic would be nice |
111 | 110 | * Could have types like (fin n): not just 1 and 2, but 3, 4, etc. |
@@ -204,3 +203,102 @@ | ||
204 | 203 | * Multiple results: [X] -> [Y × [X]] |
205 | 204 | * blends non-determinism and state |
206 | 205 | * Render 3b1b's simple iterated Newton fractal |
206 | +* Lenses | |
207 | + * Given a category C... | |
208 | + * Lens(C): Objects are pairs X × Y, internal homs [X × Y, Z × W] are: | |
209 | + * [X, Y] × [X × W, Z] | |
210 | + * LinLens(C): Objects are pairs X × Y, internal homs [X × Y, Z × W] are: | |
211 | + * [X, Y × [W, Z]] | |
212 | + * Lens(C) and LinLens(C) are equivalent when C is Cartesian closed! | |
213 | + * Massage Lens(C) arrows to [X, Y] × [X, [W, Z]] by currying under the | |
214 | + second hom | |
215 | + * LinLens => Lens | |
216 | + * LinLens: Pass an X, get Y × [W, Z] | |
217 | + * Lens: Pass X to both sides of the pair, get Y × [W, Z] | |
218 | + * Lens => LinLens | |
219 | + * Same steps but inverse | |
220 | + * djinn can't handle these | |
221 | + * Further, Optic(C) or other generalized lenses are also equivalent | |
222 | +* Profunctors | |
223 | + * Generalizes functors: | |
224 | + * Replace F : C -> D with | |
225 | + * F : C^ × D -> Set | |
226 | +* (l nil nil) fails an occurs check | |
227 | + * Root cause: (comp nil dup) = (pair nil nil) | |
228 | + * Typechecker can't tell that the two nils are different types | |
229 | + * If jelly uses dup, then we get different typechecker results | |
230 | + * Workaround: (pair (fun/const nil) nil) | |
231 | + * jelly can't tell that (comp ignore nil) is superfluous here and doesn't | |
232 | + insert dup | |
233 | + * typechecker instantiates nil's RHS twice, doesn't unify them | |
234 | + * allows writing list/tails : [X] -> [[X]] | |
235 | +* WTB interactive proof assistant | |
236 | + * I ask for an arrow X -> Y, specifying types X and Y | |
237 | + * If the arrow is universal, unwrap it somewhat and recurse | |
238 | + * Otherwise, prompt for me to make a choice | |
239 | + * I can choose an existing theorem from the hive and handle a premise | |
240 | + * I can craft a partial unwrapping and transform a premise | |
241 | + * I can introduce a given | |
242 | + * I can ask djinn for some possibilities | |
243 | + * I can add an invariant and ask for a simplification from jelly? | |
244 | +* Metrics | |
245 | + * Euclidean | |
246 | + * Taxicab | |
247 | + * Maximum | |
248 | + * Lp | |
249 | +* Deferreds | |
250 | + * Monad API | |
251 | + * Given x : 1 -> X, (seed x) : 1 -> DX | |
252 | + * Given f : X -> Y, (dmap f): DX -> DY | |
253 | + * Given a : X -> DY, (dchain m) : DX -> DY | |
254 | +* IDE | |
255 | + * Smalltalk-ish list of recent expressions | |
256 | + * Each expression has a type | |
257 | + * IDE has templates which recognize types | |
258 | + * 1 -> F × (F × F) could be an element of F³, but also an RGB color | |
259 | + * Polymorphic arrows like X -> X could be natural transformations | |
260 | + * Rendering/viewing could be done per-template | |
261 | + * Colors could be shown with swatches in the recent-expression list | |
262 | + * Images and videos could be thumbnailed, previewed, etc. | |
263 | +* Priority queues | |
264 | + * Given min : X × X -> X | |
265 | + * findMin : Q -> X + 1 | |
266 | + * insert : X x Q -> Q | |
267 | + * meld : Q × Q -> Q | |
268 | + * deleteMin: Q -> Q + 1 | |
269 | + * empty : 1 -> Q | |
270 | + * empty? : Q -> 2 | |
271 | + * (comp (comp (pair @0 (fun/const empty)) insert) findMin) == (comp @0 left) | |
272 | +* An optimized natset: [N] × N × [N, 2] | |
273 | + * The idea is that it's just [N, 2], but with a memoizing cache | |
274 | + * The list stores all of the members | |
275 | + * The lone nat is the lower bound for what's been checked so far | |
276 | + * (ns, k, f) where ns = { f(n) | n < k } | |
277 | +* Isomorphisms | |
278 | + * CCC isos are fully characterized by a list of axioms | |
279 | + * https://en.wikipedia.org/wiki/Cartesian_closed_category#Equational_theory | |
280 | + * Also gives a partial listing of BCCC isos (CCCs with sums) | |
281 | + * Motivation: isos are useful objects, but our theories can't prove that | |
282 | + user-provided arrows are iso | |
283 | + * Makes sense, without access to universe types or NTs | |
284 | + * OTOH, every polymorphic arrow is an NT already | |
285 | + * And so every polymorphic iso would be a natural iso... There's | |
286 | + something here, but I'm not sure what yet | |
287 | + * Would monics and epics also be useful? | |
288 | + * Being monic or epic is a property, but being iso is structure | |
289 | + * Category of isos is always groupoid, for example | |
290 | +* Double recursion | |
291 | + * G(0) = \x -> x + 1 | |
292 | + * G(n + 1) = \x -> case x of | |
293 | + zero -> G(n)(1) | |
294 | + x + 1 -> G(n)(G(n + 1)(x)) | |
295 | +* Generalized induction schemes | |
296 | + * Using lists as an example... | |
297 | + * We should have a way to incrementally assemble lists | |
298 | + * cons : X × [X] -> [X] | |
299 | + * And also a way to incrementally eliminate them | |
300 | + * uncons : [X] -> X × [X] + 1 | |
301 | + * And these should be adjoint | |
302 | + * (comp cons uncons) = left : X × [X] -> X × [X] + 1 | |
303 | + * (comp uncons (case cons nil)) = id : [X] -> [X] | |
304 | + * This all suggests that we should automatically generate uncons |