A categorical programming language
| 修订版 | 04c4c704ea2d187daa492eb53b1848319ab619ac (tree) |
|---|---|
| 时间 | 2022-03-08 18:45:59 |
| 作者 | Corbin <cds@corb...> |
| Commiter | Corbin |
Finish cleanup of type extractor.
cammy-rpy/cammylib/sexp.py (diff) cammy-rpy/cammylib/types.py (diff) cammy-rpy/repl.py (diff) cammy-rpy/weave.py (diff)
hive/double/merge.cammy (diff) hive/f/cube.cammy (diff) hive/f/divpair.cammy (diff) hive/f/mulpair.cammy (diff) hive/fun/flip.cammy (diff) hive/fun/int-flip.cammy (diff) hive/pair/of.cammy (diff) jelly/src/main.rs (diff)
todo.txt (diff)| @@ -39,6 +39,9 @@ class Atom(SExp): | ||
| 39 | 39 | def occurs(self, index): |
| 40 | 40 | return False |
| 41 | 41 | |
| 42 | + def extractType(self, extractor): | |
| 43 | + return self.symbol | |
| 44 | + | |
| 42 | 45 | def buildArrow(self): |
| 43 | 46 | return buildUnary(self.symbol) |
| 44 | 47 |
| @@ -74,6 +77,19 @@ class Functor(SExp): | ||
| 74 | 77 | return True |
| 75 | 78 | return False |
| 76 | 79 | |
| 80 | + def extractType(self, extractor): | |
| 81 | + args = [extractor.extract(unhole(arg)) for arg in self.arguments] | |
| 82 | + if self.constructor == "hom": | |
| 83 | + return "[%s, %s]" % (args[0], args[1]) | |
| 84 | + elif self.constructor == "pair": | |
| 85 | + return "(%s x %s)" % (args[0], args[1]) | |
| 86 | + elif self.constructor == "sum": | |
| 87 | + return "(%s + %s)" % (args[0], args[1]) | |
| 88 | + elif self.constructor == "list": | |
| 89 | + return "[%s]" % args[0] | |
| 90 | + else: | |
| 91 | + assert False, "whoops" | |
| 92 | + | |
| 77 | 93 | def buildArrow(self): |
| 78 | 94 | args = [arg.buildArrow() for arg in self.arguments] |
| 79 | 95 | return buildCompound(self.constructor, args) |
| @@ -99,5 +115,12 @@ class Hole(SExp): | ||
| 99 | 115 | def occurs(self, index): |
| 100 | 116 | return self.index == index |
| 101 | 117 | |
| 118 | + def extractType(self, extractor): | |
| 119 | + return extractor.findTypeAlias(self.index) | |
| 120 | + | |
| 102 | 121 | def buildArrow(self): |
| 103 | 122 | return Given(self.index) |
| 123 | + | |
| 124 | +def unhole(sexp): | |
| 125 | + assert isinstance(sexp, Hole), "implementation error" | |
| 126 | + return sexp.index |
| @@ -1,4 +1,4 @@ | ||
| 1 | -from cammylib.sexp import Atom, Functor, Hole | |
| 1 | +from cammylib.sexp import Atom, Functor, Hole, unhole | |
| 2 | 2 | |
| 3 | 3 | class UnificationFailed(Exception): |
| 4 | 4 | def __init__(self, message): |
| @@ -10,10 +10,6 @@ def occursCheck(index, var): | ||
| 10 | 10 | raise UnificationFailed("Occurs check: %d in %s" % |
| 11 | 11 | (index, var.asStr())) |
| 12 | 12 | |
| 13 | -def unhole(sexp): | |
| 14 | - assert isinstance(sexp, Hole), "implementation error" | |
| 15 | - return sexp.index | |
| 16 | - | |
| 17 | 13 | class ConstraintStore(object): |
| 18 | 14 | "A Kanren-style constraint store." |
| 19 | 15 |
| @@ -87,37 +83,27 @@ class ConstraintStore(object): | ||
| 87 | 83 | LETTERS = "XYZWSTPQ" |
| 88 | 84 | |
| 89 | 85 | class TypeExtractor(object): |
| 90 | - def __init__(self): | |
| 86 | + def __init__(self, cs): | |
| 87 | + self.cs = cs | |
| 91 | 88 | self.d = {} |
| 89 | + self.seen = [] | |
| 92 | 90 | |
| 93 | 91 | def addTypeAlias(self, index): |
| 94 | 92 | self.d[index] = LETTERS[len(self.d)] |
| 95 | 93 | |
| 96 | - def extractType(self, cs, var): | |
| 97 | - return self.go(cs, var, []) | |
| 98 | - | |
| 99 | - def go(self, cs, var, seen): | |
| 100 | - sexp = cs.walk(var) | |
| 101 | - if isinstance(sexp, Hole): | |
| 102 | - if sexp.index not in self.d: | |
| 103 | - self.addTypeAlias(sexp.index) | |
| 104 | - return self.d[sexp.index] | |
| 105 | - elif isinstance(sexp, Atom): | |
| 106 | - return sexp.symbol | |
| 107 | - elif isinstance(sexp, Functor): | |
| 108 | - if var in seen: | |
| 109 | - # XXX split exceptions? | |
| 110 | - raise UnificationFailed("tried to extract infinite type") | |
| 111 | - args = [self.go(cs, unhole(arg), seen + [var]) for arg in sexp.arguments] | |
| 112 | - if sexp.constructor == "hom": | |
| 113 | - return "[%s, %s]" % (args[0], args[1]) | |
| 114 | - elif sexp.constructor == "pair": | |
| 115 | - return "(%s x %s)" % (args[0], args[1]) | |
| 116 | - elif sexp.constructor == "sum": | |
| 117 | - return "(%s + %s)" % (args[0], args[1]) | |
| 118 | - elif sexp.constructor == "list": | |
| 119 | - return "[%s]" % args[0] | |
| 120 | - else: | |
| 121 | - assert False, "whoops" | |
| 122 | - else: | |
| 123 | - assert False, "not whoops" | |
| 94 | + def findTypeAlias(self, index): | |
| 95 | + if index not in self.d: | |
| 96 | + self.addTypeAlias(index) | |
| 97 | + return self.d[index] | |
| 98 | + | |
| 99 | + def extract(self, var): | |
| 100 | + if var in self.seen: | |
| 101 | + # XXX split exceptions? | |
| 102 | + raise UnificationFailed("tried to extract infinite type") | |
| 103 | + self.seen.append(var) | |
| 104 | + | |
| 105 | + sexp = self.cs.walk(var) | |
| 106 | + rv = sexp.extractType(self) | |
| 107 | + | |
| 108 | + self.seen.pop() | |
| 109 | + return rv |
| @@ -16,6 +16,7 @@ def command(hive, code, line): | ||
| 16 | 16 | # XXX code e: Edit a file |
| 17 | 17 | # os.system("$EDITOR") |
| 18 | 18 | if code == "!": |
| 19 | + # Evaluate an element. | |
| 19 | 20 | sexp, trail = parse(line) |
| 20 | 21 | sexp = sexp.canonicalize(hive) |
| 21 | 22 | sexp = jellify(sexp) |
| @@ -50,12 +51,12 @@ def repl(hive, stdin, stdout): | ||
| 50 | 51 | print "Arrow:", arrow |
| 51 | 52 | cs = ConstraintStore() |
| 52 | 53 | domain, codomain = arrow.types(cs) |
| 53 | - extractor = TypeExtractor() | |
| 54 | + extractor = TypeExtractor(cs) | |
| 54 | 55 | for i, (gdom, gcod) in enumerate(cs.knownGivens): |
| 55 | 56 | print "Given @%d : %s -> %s" % (i, |
| 56 | - extractor.extractType(cs, gdom), | |
| 57 | - extractor.extractType(cs, gcod)) | |
| 58 | - print "Type:", extractor.extractType(cs, domain), "->", extractor.extractType(cs, codomain) | |
| 57 | + extractor.extract(gdom), | |
| 58 | + extractor.extract(gcod)) | |
| 59 | + print "Type:", extractor.extract(domain), "->", extractor.extract(codomain) | |
| 59 | 60 | except BuildProblem as bp: |
| 60 | 61 | print "Couldn't build arrow:", bp.message |
| 61 | 62 | except UnificationFailed as uf: |
| @@ -23,6 +23,7 @@ def main(argv): | ||
| 23 | 23 | prefix = len(hivepath) |
| 24 | 24 | doc = [] |
| 25 | 25 | for dirpath, dirnames, filenames in os.walk(hivepath): |
| 26 | + SortFileNames(dirnames).sort() | |
| 26 | 27 | SortFileNames(filenames).sort() |
| 27 | 28 | section = dirpath[prefix:] or "Top level" |
| 28 | 29 | doc.append("# " + section) |
| @@ -44,13 +45,13 @@ def main(argv): | ||
| 44 | 45 | arrow = sexp.buildArrow() |
| 45 | 46 | cs = ConstraintStore() |
| 46 | 47 | domain, codomain = arrow.types(cs) |
| 47 | - extractor = TypeExtractor() | |
| 48 | + extractor = TypeExtractor(cs) | |
| 48 | 49 | for i, (gdom, gcod) in enumerate(cs.knownGivens): |
| 49 | 50 | doc.append("Given @%d : %s -> %s" % (i, |
| 50 | - extractor.extractType(cs, gdom), | |
| 51 | - extractor.extractType(cs, gcod))) | |
| 52 | - doc.append("Type: %s -> %s" % (extractor.extractType(cs, domain), | |
| 53 | - extractor.extractType(cs, codomain))) | |
| 51 | + extractor.extract(gdom), | |
| 52 | + extractor.extract(gcod))) | |
| 53 | + doc.append("Type: %s -> %s" % (extractor.extract(domain), | |
| 54 | + extractor.extract(codomain))) | |
| 54 | 55 | except MissingAtom as ma: |
| 55 | 56 | doc.append( |
| 56 | 57 | "(Couldn't canonicalize due to missing expression %s)" % |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(case id id) | |
| 2 | + | |
| 3 | +Either side of a double. |
| @@ -1,3 +1,3 @@ | ||
| 1 | -(comp (comp (pair id fun/dup) (pair fst (comp snd f-mul))) f-mul) | |
| 1 | +(comp (pair id (comp fun/dup f-mul)) f-mul) | |
| 2 | 2 | |
| 3 | 3 | The cube of a floating-point number. |
| @@ -1,3 +1,3 @@ | ||
| 1 | -(f/mulpair @0 (comp @1 f-recip)) | |
| 1 | +(pair/of f/div @0 @1) | |
| 2 | 2 | |
| 3 | 3 | Apply division to a pair of arrows. |
| @@ -1,3 +1,3 @@ | ||
| 1 | -(comp (pair @0 @1) f-mul) | |
| 1 | +(pair/of f-mul @0 @1) | |
| 2 | 2 | |
| 3 | 3 | Apply multiplication to a pair of arrows. |
| @@ -1 +1,3 @@ | ||
| 1 | -(curry (curry (comp (pair (comp (pair (comp fst fst) snd) fun/app) (comp fst snd)) fun/app))) | |
| 1 | +(curry (comp fun/swap (uncurry @0))) | |
| 2 | + | |
| 3 | +Swap the order in which arguments are applied onto a curried arrow. |
| @@ -0,0 +1 @@ | ||
| 1 | +(curry (curry (comp (pair (comp (pair (comp fst fst) snd) fun/app) (comp fst snd)) fun/app))) |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(comp (pair @1 @2) @0) | |
| 2 | + | |
| 3 | +Call an arrow of two arguments by building both arguments from a single input. |
| @@ -11,6 +11,9 @@ fn load_tree(handle :&mut Read) -> std::io::Result<RecExpr<SymbolLang>> { | ||
| 11 | 11 | // Wadler 1989: https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf |
| 12 | 12 | // Elliott 2013: http://conal.net/blog/posts/optimizing-cccs |
| 13 | 13 | |
| 14 | +// "R when X is id" means that rule R is being specialized modulo the equality: | |
| 15 | +// (comp id ?f) = ?f = (comp ?f id) = (comp (comp ?f id) id) = ... | |
| 16 | + | |
| 14 | 17 | // "free for X" means that the polymorphic type of X implies the underlying equality justifying |
| 15 | 18 | // the annotated rule, as in Wadler 1989. |
| 16 | 19 |
| @@ -38,10 +41,22 @@ fn main() -> std::io::Result<()> { | ||
| 38 | 41 | // free for snd |
| 39 | 42 | rw!("snd-elim-pair"; "(comp (pair ?f ?g) snd)" => "?g"), |
| 40 | 43 | rw!("pair-fst-snd"; "(pair fst snd)" => "id"), |
| 44 | + rw!("pair-repack"; "(comp (pair ?f ?g) (pair (comp fst ?j) (comp snd ?k)))" | |
| 45 | + => "(pair (comp ?f ?j) (comp ?g ?k))"), | |
| 46 | + // pair-repack when ?j is id | |
| 47 | + rw!("pair-repack-snd"; "(comp (pair ?f ?g) (pair fst (comp snd ?k)))" | |
| 48 | + => "(pair ?f (comp ?g ?k))"), | |
| 49 | + // pair-repack when ?k is id | |
| 50 | + rw!("pair-repack-fst"; "(comp (pair ?f ?g) (pair (comp fst ?j) snd))" | |
| 51 | + => "(pair (comp ?f ?j) ?g)"), | |
| 41 | 52 | // Elliott 2013 |
| 42 | 53 | rw!("pair-precompose"; "(pair (comp ?r ?f) (comp ?r ?g))" => "(comp ?r (pair ?f ?g))"), |
| 43 | - // Needed with pair-precompose as a special case. | |
| 44 | - rw!("pair-factor"; "(pair ?r ?r)" => "(comp ?r (pair id id))"), | |
| 54 | + // pair-precompose when ?f is id | |
| 55 | + rw!("pair-factor-fst"; "(pair ?r (comp ?r ?g))" => "(comp ?r (pair id ?g))"), | |
| 56 | + // pair-precompose when ?g is id | |
| 57 | + rw!("pair-factor-snd"; "(pair (comp ?r ?f) ?r)" => "(comp ?r (pair ?f id))"), | |
| 58 | + // pair-precompose when ?f and ?g are id | |
| 59 | + rw!("pair-factor-both"; "(pair ?r ?r)" => "(comp ?r (pair id id))"), | |
| 45 | 60 | |
| 46 | 61 | // Turn braided products into symmetric products. |
| 47 | 62 | rw!("pair-swap-invo"; "(comp (pair snd fst) (pair snd fst))" => "id"), |
| @@ -1,28 +1,8 @@ | ||
| 1 | -* Literate Cammy | |
| 2 | - * Entrypoints: | |
| 3 | - - cammy-repl $HIVE: REPL session with a hive | |
| 4 | - - cammy-weave $HIVE: document a hive | |
| 5 | - * cammy-tangle $HIVE: take an expression on stdin, return framed optimized | |
| 6 | - expression on stdout | |
| 7 | - - cammy-frame $HIVE | cammy-jelly | |
| 8 | - - cammy-draw ...: take an expression and canvas params, make a PNG | |
| 9 | - - cammy-frame $HIVE: take an expression on stdin, return framed expression | |
| 10 | - on stdout | |
| 11 | - - cammy-jelly: print an optimized expression on stdout | |
| 12 | - - cammy-djinn $TY $TY: synthesize a function with the given signature | |
| 13 | - - uses last bit of movelist code | |
| 14 | 1 | * REPL improvements |
| 15 | 2 | * allow mid-functor newlines |
| 16 | - * jellification | |
| 17 | - * : commands | |
| 18 | - * help, describe commands | |
| 19 | - * edit an atom's trail | |
| 20 | -* Other entrypoints | |
| 21 | - * Split and cleanup movelist | |
| 22 | - * cammy-typecheck: take an expression on stdin, print its type | |
| 23 | - * cammy-djinn: take a closed type, return expression with that type on | |
| 24 | - stdout | |
| 25 | - | |
| 3 | + * : commands | |
| 4 | + * help, describe commands | |
| 5 | + * edit an atom's trail | |
| 26 | 6 | * list/eq : [X × X, 2] → [[X] × [X], 2] |
| 27 | 7 | * list/zip : [X] × [Y] → [X × Y] |
| 28 | 8 | * list/tail : [X] → [X] |
| @@ -33,12 +13,13 @@ | ||
| 33 | 13 | * Transcendental and other constants |
| 34 | 14 | * Euler's constant e |
| 35 | 15 | * Euler's constant gamma |
| 36 | -* Remove movelist djinn, maybe? | |
| 37 | 16 | * Double-negation monad for CPS? |
| 38 | 17 | * Cont is available but not fully developed |
| 39 | 18 | * monads/cont/join, monads/cont/bind, etc. |
| 40 | 19 | * fun/name should always start from 1 |
| 41 | 20 | * Requires changing some callers |
| 21 | + * Might not be feasible unless we switch to stricter monoidal categories | |
| 22 | + * We'd need an equivalence X × 1 → X | |
| 42 | 23 | * Prove that nat/add is smallest with its behavior |
| 43 | 24 | * Streams |
| 44 | 25 | * Monad: X → [N, X] |
| @@ -50,8 +31,23 @@ | ||
| 50 | 31 | * Cantor's type of bitstrings: N -> 2 |
| 51 | 32 | * The square type: For a type X, 2 -> X |
| 52 | 33 | * Another special case of reader monad |
| 53 | -* The double type: For a type X, X + X | |
| 54 | 34 | * Moore machines: For state type Q and input type S, Q × S -> Q |
| 55 | 35 | * Moore transducers: [Q × S, Q] -> [Q × S, Q] |
| 56 | 36 | * Mealy machines: For state type Q, input type S, and output type L, Q × S -> Q × L |
| 57 | 37 | * Jets |
| 38 | + * how to replace e.g. nat/add? | |
| 39 | + * find its subgraph with E-matching? | |
| 40 | + * hook the hive to load a specialized routine during codeload? | |
| 41 | +* Search for more optimizations | |
| 42 | + * Some arrows have inferred types that suggest they should be simplifiable | |
| 43 | + * X -> X: should be id? | |
| 44 | + * X -> 1: should be ignore | |
| 45 | + * 1 -> 2: should be t or f | |
| 46 | +* New int type | |
| 47 | + * Current type: quotient of N × N under subtraction | |
| 48 | + * big, tricky case analysis, big quotient overlap | |
| 49 | + * Proposed type: quotient of N + N gluing zero | |
| 50 | + * almost minimal, sign bit, quotient glues exactly two elements into one | |
| 51 | +* Refactoring tools | |
| 52 | + * Find all leaves in a hive | |
| 53 | + * Rename an expression and change all callers |
Fork