提交: c08887f024dd593812d696ff75f00c93ba919992 - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: c08887f024dd593812d696ff75f00c93ba919992 (tree)
• 时间: 2022-02-26 13:48:39
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Implement a not-yet-translated typechecker.

更改概述

• modified: cammy-rpy/cammylib/arrows.py
• add: cammy-rpy/cammylib/types.py
• modified: cammy-rpy/repl.py
• modified: hive/fractal-membership.cammy
• modified: hive/graph-fun.cammy
• modified: hive/h2rgb.cammy
• modified: hive/hv2rgb.cammy
• modified: hive/iter-fractal.cammy
• modified: todo.txt

差异

--- a/cammy-rpy/cammylib/arrows.py
+++ b/cammy-rpy/cammylib/arrows.py
@@ -113,9 +113,15 @@ class Xs(Element):
 class Arrow(object):
     _immutable_ = True
 
+    def boundVars(self):
+        return self.domain.boundVars() | self.codomain.boundVars()
+
 class Id(Arrow):
     _immutable_ = True
     def run(self, x): return x
+    def types(self, cs):
+        rv = cs.fresh()
+        return rv, rv
 
 class Comp(Arrow):
     _immutable_ = True
@@ -123,71 +129,138 @@ class Comp(Arrow):
         self.f = f
         self.g = g
     def run(self, x): return self.g.run(self.f.run(x))
+    def types(self, cs):
+        fdom, fcod = self.f.types(cs)
+        gdom, gcod = self.g.types(cs)
+        cs.unify(fcod, gdom)
+        return fdom, gcod
 
 class Ignore(Arrow):
     _immutable_ = True
     def run(self, x): return T()
+    def types(self, cs): return cs.fresh(), cs.concrete("1")
 
 class First(Arrow):
     _immutable_ = True
     def run(self, x): return x.first()
+    def types(self, cs):
+        left = cs.fresh()
+        pair = cs.functor("pair", [left, cs.fresh()])
+        return pair, left
 
 class Second(Arrow):
     _immutable_ = True
     def run(self, x): return x.second()
+    def types(self, cs):
+        right = cs.fresh()
+        pair = cs.functor("pair", [cs.fresh(), right])
+        return pair, right
 
 class Pair(Arrow):
     _immutable_ = True
     def __init__(self, f, g):
         self.f = f
         self.g = g
-    def run(self, x):
-        return P(self.f.run(x), self.g.run(x))
+    def run(self, x): return P(self.f.run(x), self.g.run(x))
+    def types(self, cs):
+        fdom, fcod = self.f.types(cs)
+        gdom, gcod = self.g.types(cs)
+        cs.unify(fdom, gdom)
+        return fdom, cs.functor("pair", [fcod, gcod])
 
 class Left(Arrow):
     _immutable_ = True
     def run(self, x): return L(x)
+    def types(self, cs):
+        rv = cs.fresh()
+        return rv, cs.functor("sum", [rv, cs.fresh()])
 
 class Right(Arrow):
     _immutable_ = True
     def run(self, x): return R(x)
+    def types(self, cs):
+        rv = cs.fresh()
+        return rv, cs.functor("sum", [cs.fresh(), rv])
 
 class Case(Arrow):
     _immutable_ = True
     def __init__(self, f, g):
         self.f = f
         self.g = g
-    def run(self, x):
-        return x.tagged(self.f, self.g)
+    def run(self, x): return x.tagged(self.f, self.g)
+    def types(self, cs):
+        fdom, fcod = self.f.types(cs)
+        gdom, gcod = self.g.types(cs)
+        cs.unify(fcod, gcod)
+        return fdom, cs.functor("sum", [fdom, gdom])
 
 class Curry(Arrow):
     _immutable_ = True
-    def __init__(self, f):
-        self._f = f
-
-    def run(self, x):
-        return H(self._f, x)
+    def __init__(self, f): self._f = f
+    def run(self, x): return H(self._f, x)
+    def types(self, cs):
+        fdom, fcod = self._f.types(cs)
+        x = cs.fresh()
+        y = cs.fresh()
+        cs.unify(fdom, cs.functor("pair", [x, y]))
+        return x, cs.functor("hom", [y, fcod])
 
 class Uncurry(Arrow):
     _immutable_ = True
-    def __init__(self, f):
-        self._f = f
-
-    def run(self, x):
-        return self._f.run(x.first()).apply(x.second())
+    def __init__(self, f): self._f = f
+    def run(self, x): return self._f.run(x.first()).apply(x.second())
+    def types(self, cs):
+        fdom, fcod = self._f.types(cs)
+        x = cs.fresh()
+        y = cs.fresh()
+        cs.unify(fcod, cs.functor("hom", [x, y]))
+        return cs.functor("pair", [fdom, x]), y
 
 class Either(Arrow):
     _immutable_ = True
-    def run(self, x):
-        return L(T()) if x.b() else R(T())
+    def run(self, x): return L(T()) if x.b() else R(T())
+    def types(self, cs):
+        one = cs.concrete("1")
+        return cs.concrete("2"), cs.functor("sum", [one, one])
+
+class TrueArr(Arrow):
+    _immutable_ = True
+    def run(self, x): return B(True)
+    def types(self, cs): return cs.concrete("1"), cs.concrete("2")
+
+class FalseArr(Arrow):
+    _immutable_ = True
+    def run(self, x): return B(False)
+    def types(self, cs): return cs.concrete("1"), cs.concrete("2")
+
+class NotArr(Arrow):
+    _immutable_ = True
+    def run(self, x): return B(not x.b())
+    def types(self, cs): return cs.concrete("2"), cs.concrete("2")
+
+class Conj(Arrow):
+    _immutable_ = True
+    def run(self, x): return B(x.first().b() and x.second().b())
+    def types(self, cs):
+        two = cs.concrete("2")
+        return cs.functor("pair", [two, two]), two
+
+class Disj(Arrow):
+    _immutable_ = True
+    def run(self, x): return B(x.first().b() or x.second().b())
+    def types(self, cs):
+        two = cs.concrete("2")
+        return cs.functor("pair", [two, two]), two
 
 class Zero(Arrow):
     _immutable_ = True
     def run(self, x): return N(rbigint.fromint(0))
+    def types(self, cs): return cs.concrete("1"), cs.concrete("N")
 
 class Succ(Arrow):
     _immutable_ = True
     def run(self, x): return N(x.n().int_add(1))
+    def types(self, cs): return cs.concrete("N"), cs.concrete("N")
 
 pr_driver = JitDriver(name="pr",
         greens=["pr"], reds=["n", "rv"],
@@ -208,13 +281,27 @@ class PrimRec(Arrow):
             rv = self._f.run(rv)
         return rv
 
+    def types(self, cs):
+        xdom, xcod = self._x.types(cs)
+        fdom, fcod = self._f.types(cs)
+        cs.unify(xdom, cs.concrete("1"))
+        cs.unify(xcod, fcod)
+        cs.unify(fdom, fcod)
+        return cs.concrete("N"), fcod
+
 class Nil(Arrow):
     _immutable_ = True
     def run(self, x): return Xs([])
+    def types(self, cs):
+        return cs.concrete("1"), cs.functor("list", [cs.fresh()])
 
 class Cons(Arrow):
     _immutable_ = True
     def run(self, x): return Xs([x.first()] + x.second().l())
+    def types(self, cs):
+        x = cs.fresh()
+        xs = cs.functor("list", [x])
+        return cs.functor("pair", [x, xs]), xs
 
 fold_driver = JitDriver(name="fold",
         greens=["fold"], reds=["element"],
@@ -234,23 +321,35 @@ class Fold(Arrow):
         for e in x.l():
             rv = driveFold(self._c, P(e, rv))
         return rv
+    def types(self, cs):
+        ndom, ncod = self._n.types(cs)
+        cdom, ccod = self._c.types(cs)
+        cs.unify(ndom, cs.concrete("1"))
+        x = cs.fresh()
+        cs.unify(cdom, cs.functor("pair", [ccod, x]))
+        cs.unify(ncod, ccod)
+        return cs.functor("list", [x]), ccod
 
 class FZero(Arrow):
     _immutable_ = True
     def run(self, x): return F(0.0)
+    def types(self, cs): return cs.concrete("1"), cs.concrete("F")
 
 class FOne(Arrow):
     _immutable_ = True
     def run(self, x): return F(1.0)
+    def types(self, cs): return cs.concrete("1"), cs.concrete("F")
 
 class FPi(Arrow):
     _immutable_ = True
     def run(self, x): return F(math.pi)
+    def types(self, cs): return cs.concrete("1"), cs.concrete("F")
 
 def sign(f): return math.copysign(1.0, f) > 0.0
 class FSign(Arrow):
     _immutable_ = True
     def run(self, x): return B(sign(x.f()))
+    def types(self, cs): return cs.concrete("F"), cs.concrete("2")
 
 class FFloor(Arrow):
     _immutable_ = True
@@ -259,10 +358,14 @@ class FFloor(Arrow):
             return L(F(float(math.floor(x.f()))))
         except (ValueError, OverflowError):
             return R(T())
+    def types(self, cs):
+        return (cs.concrete("F"),
+                cs.functor("sum", [cs.concrete("F"), cs.concrete("1")]))
 
 class FNegate(Arrow):
     _immutable_ = True
     def run(self, x): return F(-x.f())
+    def types(self, cs): return cs.concrete("F"), cs.concrete("F")
 
 INF = float("inf")
 class FRecip(Arrow):
@@ -274,6 +377,7 @@ class FRecip(Arrow):
             return F(math.copysign(INF, f))
         else:
             return F(1.0 / f)
+    def types(self, cs): return cs.concrete("F"), cs.concrete("F")
 
 class FLT(Arrow):
     _immutable_ = True
@@ -281,6 +385,9 @@ class FLT(Arrow):
         f1 = x.first().f()
         f2 = x.second().f()
         return B(True) if f1 == -0.0 and f2 == 0.0 else B(f1 < f2)
+    def types(self, cs):
+        f = cs.concrete("F")
+        return cs.functor("pair", [f, f]), cs.concrete("2")
 
 class FAdd(Arrow):
     _immutable_ = True
@@ -298,6 +405,9 @@ class FAdd(Arrow):
             if math.isnan(rv):
                 rv = 0.0
         return F(rv)
+    def types(self, cs):
+        f = cs.concrete("F")
+        return cs.functor("pair", [f, f]), f
 
 MUL_SPECIALS = 0.0, -0.0, INF, -INF
 class FMul(Arrow):
@@ -316,24 +426,35 @@ class FMul(Arrow):
             if math.isnan(rv):
                 rv = 0.0 * math.copysign(1.0, y) * math.copysign(1.0, z)
         return F(rv)
+    def types(self, cs):
+        f = cs.concrete("F")
+        return cs.functor("pair", [f, f]), f
 
 class FSqrt(Arrow):
     _immutable_ = True
     def run(self, x):
         f = x.f()
         return L(F(math.sqrt(f))) if sign(f) else R(T())
+    def types(self, cs):
+        f = cs.concrete("F")
+        return f, cs.functor("sum", [f, cs.concrete("1")])
 
 class FSin(Arrow):
     _immutable_ = True
     def run(self, x): return F(math.sin(x.f()))
+    def types(self, cs): return cs.concrete("F"), cs.concrete("F")
 
 class FCos(Arrow):
     _immutable_ = True
     def run(self, x): return F(math.cos(x.f()))
+    def types(self, cs): return cs.concrete("F"), cs.concrete("F")
 
 class FATan2(Arrow):
     _immutable_ = True
     def run(self, x): return F(math.atan2(x.first().f(), x.second().f()))
+    def types(self, cs):
+        f = cs.concrete("F")
+        return cs.functor("pair", [f, f]), f
 
 
 class BuildProblem(Exception):
@@ -348,6 +469,11 @@ unaryFunctors = {
     "left": Left(),
     "right": Right(),
     "either": Either(),
+    "t": TrueArr(),
+    "f": FalseArr(),
+    "not": NotArr(),
+    "conj": Conj(),
+    "disj": Disj(),
     "zero": Zero(),
     "succ": Succ(),
     "nil": Nil(),

--- /dev/null
+++ b/cammy-rpy/cammylib/types.py
@@ -0,0 +1,97 @@
+from cammylib.sexp import Atom, Functor, Hole
+
+class UnificationFailed(Exception):
+    def __init__(self, message):
+        self.message = message
+
+class ConstraintStore(object):
+    "A Kanren-style constraint store."
+
+    def __init__(self):
+        self.i = 0
+        self.constraints = []
+
+    def fresh(self):
+        rv = self.i
+        self.i += 1
+        self.constraints.append(Hole(rv))
+        return rv
+
+    def concrete(self, symbol):
+        rv = self.i
+        self.i += 1
+        self.constraints.append(Atom(symbol))
+        return rv
+
+    def functor(self, constructor, arguments):
+        rv = self.i
+        self.i += 1
+        args = [Hole(arg) for arg in arguments]
+        self.constraints.append(Functor(constructor, args))
+        return rv
+
+    def walkArg(self, var):
+        if isinstance(var, Atom):
+            return var
+        elif isinstance(var, Functor):
+            return Functor(var.constructor,
+                    [self.walkArg(arg) for arg in var.arguments])
+        elif isinstance(var, Hole):
+            return self.walk(var.index)
+        assert False, "impossible"
+
+    def walk(self, i):
+        var = self.constraints[i]
+        if isinstance(var, Hole) and var.index == i:
+            return var
+        else:
+            return self.walkArg(var)
+
+    def unify(self, i, j):
+        return self.unifyArg(self.walk(i), self.walk(j))
+
+    def unifyArg(self, vi, vj):
+        print "unifying", vi.asStr(), vj.asStr()
+        if isinstance(vi, Hole):
+            self.constraints[vi.index] = vj
+        elif isinstance(vj, Hole):
+            self.constraints[vj.index] = vi
+        elif isinstance(vi, Atom) and isinstance(vj, Atom):
+            if vi.symbol != vj.symbol:
+                raise UnificationFailed(
+                    "Can't unify constant types: %s vs. %s" %
+                    (vi.symbol, vj.symbol))
+        elif isinstance(vi, Functor) and isinstance(vj, Functor):
+            if vi.constructor != vj.constructor:
+                raise UnificationFailed(
+                    "Can't unify compound types: %s vs. %s" %
+                    (vi.constructor, vj.constructor))
+            if len(vi.arguments) != len(vj.arguments):
+                raise UnificationFailed("Compound types have different arity?")
+            for i, argi in enumerate(vi.arguments):
+                self.unifyArg(argi, vj.arguments[i])
+        else:
+            raise UnificationFailed("Quite different types: %s. vs %s" %
+                    (vi.asStr(), vj.asStr()))
+
+def formatType(sexp):
+    if isinstance(sexp, Hole):
+        return "_%d" % sexp.index
+    elif isinstance(sexp, Atom):
+        return sexp.symbol
+    elif isinstance(sexp, Functor):
+        if sexp.constructor == "hom":
+            return "[%s, %s]" % (formatType(sexp.arguments[0]),
+                    formatType(sexp.arguments[1]))
+        elif sexp.constructor == "pair":
+            return "(%s x %s)" % (formatType(sexp.arguments[0]),
+                    formatType(sexp.arguments[1]))
+        elif sexp.constructor == "sum":
+            return "(%s + %s)" % (formatType(sexp.arguments[0]),
+                    formatType(sexp.arguments[1]))
+        elif sexp.constructor == "list":
+            return "[%s]" % formatType(sexp.arguments[0])
+        else:
+            assert False, "whoops"
+    else:
+        assert False, "not whoops"

--- a/cammy-rpy/repl.py
+++ b/cammy-rpy/repl.py
@@ -1,13 +1,22 @@
 # Inspired by https://www.pypy.org/posts/2018/11/guest-post-implementing-calculator-repl-6271483514675006846.html
 
+import os
+import sys
+
 from rpython.rlib.rfile import create_stdio
 
 from cammylib.arrows import buildArrow, BuildProblem
 from cammylib.hive import Hive, MissingAtom
 from cammylib.parser import parse
+from cammylib.types import ConstraintStore, formatType, UnificationFailed
 
 LINE_BUFFER_LENGTH = 1024
 
+def command(code, line):
+    if code == "e":
+        # Edit a file
+        os.system("$EDITOR")
+
 def repl(hive, stdin, stdout):
     while True:
         stdout.write("> ")
@@ -15,6 +24,10 @@ def repl(hive, stdin, stdout):
         if not line:
             # Empty read means EOF.
             break
+        if line.startswith(":"):
+            if len(line) < 2:
+                print "Not a full command"
+            command(line[1], line[3:])
         sexp, trail = parse(line)
         print "Got:", line
         print "S-expression:", sexp.asStr()
@@ -27,8 +40,13 @@ def repl(hive, stdin, stdout):
         try:
             arrow = buildArrow(sexp)
             print "Arrow:", arrow
+            cs = ConstraintStore()
+            domain, codomain = arrow.types(cs)
+            print "Type:", formatType(cs.walk(domain)), "->", formatType(cs.walk(codomain))
         except BuildProblem as bp:
             print "Couldn't build arrow:", bp.message
+        except UnificationFailed as uf:
+            print "Couldn't check type:", uf.message
     return 0
 
 def main(argv):
@@ -40,3 +58,6 @@ def main(argv):
 def target(driver, *args):
     driver.exe_name = "cammy-repl"
     return main, None
+
+if __name__ == "__main__":
+    main(sys.argv)

--- a/hive/fractal-membership.cammy
+++ b/hive/fractal-membership.cammy
@@ -4,3 +4,8 @@
     (list/filter (f/ltpair v2/norm (fun/const f/2)))
     (comp list/len
       (f/divpair nat/to-f (fun/const (comp @1 nat/to-f))))))
+
+Measure the degree to which a fractal diverges. Given a maximum number of
+steps, we iterate the IFS for a fractal in the complex plane until its
+absolute value exceeds 2, and return a value in [0,1] indicating how many
+steps were taken before divergence.

--- a/hive/graph-fun.cammy
+++ b/hive/graph-fun.cammy
@@ -1 +1,5 @@
 (comp @0 (v3/triple id id (fun/const f-one)))
+
+Graph a real function on the plane. When interpreted as a red/green/blue
+triple, the codomain varies from blue to white as the value of the function
+varies from zero to one.

--- a/hive/h2rgb.cammy
+++ b/hive/h2rgb.cammy
@@ -12,3 +12,5 @@
           (fun/const f/3))
         f/abs)
       (fun/const f-one))))
+
+Convert a hue to its red, green, and blue components.

--- a/hive/hv2rgb.cammy
+++ b/hive/hv2rgb.cammy
@@ -1,3 +1,5 @@
 (comp
   (pair (comp fst h2rgb) (v3/broadcast snd))
   (v3/map2 f-mul))
+
+Convert a hue/value pair to a red/green/blue triple.

--- a/hive/iter-fractal.cammy
+++ b/hive/iter-fractal.cammy
@@ -3,3 +3,6 @@
     (fun/const (comp @1 nonempty/unfold))
     (pair (comp (fun/const f-zero) fun/dup) @0))
   snd)
+
+Iterate an [IFS](https://en.wikipedia.org/wiki/Iterated_function_system) for a
+given number of steps.

--- a/todo.txt
+++ b/todo.txt
@@ -13,6 +13,12 @@
     * cammy-draw ...: take an expression and canvas params, make a PNG
     * cammy-frame $HIVE: take an expression on stdin, return framed expression
       on stdout
+* REPL improvements
+  * allow mid-functor newlines
+  * jellification
+    * : commands
+      * help, describe commands
+      * edit an atom's trail
 * Other entrypoints
   * Split and cleanup movelist
     * cammy-typecheck: take an expression on stdin, print its type