提交: 83402fcc7add55f224434c3f7938d765977e2415 - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: 83402fcc7add55f224434c3f7938d765977e2415 (tree)
• 时间: 2022-09-12 01:49:26
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Check in a bunch of random files that I've had sitting around.

更改概述

• add: .envrc
• modified: honey.yaml
• add: jellyserver.py
• add: proof.txt
• add: ski2cammy.py
• add: wallpapers/burning-ship-color.png
• add: wallpapers/burning-ship.png

差异

--- /dev/null
+++ b/.envrc
@@ -0,0 +1,5 @@
+# export NIX_PATH=nixpkgs=/home/simpson/nixpkgs
+use nix
+eval $(keychain --eval --agents ssh)
+
+# export CAMMY_HIVE="$(pwd)/hive/"

--- a/honey.yaml
+++ b/honey.yaml
@@ -8,6 +8,7 @@ components:
       type: string
     Token:
       type: integer
+      format: int64
     Functor:
       type: array
       items:

--- /dev/null
+++ b/jellyserver.py
@@ -0,0 +1,79 @@
+#!/usr/bin/env nix-shell
+#! nix-shell -i python3 -p python3
+
+# This is a simple HTTP service written in Python 3. It exposes jelly to the
+# network by allowing requests to implicitly call jelly via an opaque
+# membrane. The quality of jelly is not guaranteed.
+
+import hashlib
+import http.server
+import json
+import urllib.parse
+import sys
+import threading
+
+# Expressions are stored in cache, rather than durable storage. The current
+# storage is a dict protected by a reader-writer lock.
+
+cache = {}
+cacheLock = threading.Lock()
+
+# Expressions are keyed by unguessable tokens.
+
+def makeToken(expr):
+    return hashlib.sha256(expr).hexdigest()
+TOKEN_LENGTH = len(makeToken(b"id"))
+
+class JellyHandler(http.server.BaseHTTPRequestHandler):
+
+    # All responses will be valid JSON.
+
+    def finish_JSON(self, value):
+        encoded = json.dumps(value).encode("utf-8")
+        self.send_response(http.server.HTTPStatus.OK)
+        self.send_header("Content-Type", "application/json")
+        self.send_header("Content-Length", len(encoded))
+        self.end_headers()
+        self.wfile.write(encoded)
+
+    # When a token is requested, look for an equivalent expression.
+
+    def do_GET(self):
+        url = urllib.parse.urlparse(self.path)
+        # Remove the leading slash.
+        key = url.path[1:]
+        if len(key) != TOKEN_LENGTH:
+            self.send_error(http.server.HTTPStatus.NOT_FOUND)
+            return
+
+        try:
+            # XXX timing attacks happen here
+            with cacheLock:
+                expr = cache[key]
+        except KeyError:
+            self.send_error(http.server.HTTPStatus.NOT_FOUND)
+            return
+
+        self.finish_JSON(expr)
+
+    def do_PUT(self):
+        exprLength = int(self.headers.get("Content-Length"))
+        expr = self.rfile.read(exprLength)
+        decoded = expr.decode("utf-8")
+        key = makeToken(expr)
+        with cacheLock:
+            cache[key] = decoded
+
+        self.finish_JSON(key)
+
+PORT = 8000
+
+def main():
+    print("Token length is %d" % TOKEN_LENGTH, file=sys.stderr)
+    print("Starting HTTP server on port %d" % PORT, file=sys.stderr)
+    server = http.server.ThreadingHTTPServer(("", PORT), JellyHandler)
+    server.serve_forever()
+    return 0
+
+if __name__ == "__main__":
+    sys.exit(main())

--- /dev/null
+++ b/proof.txt
@@ -0,0 +1,30 @@
+What's the smallest expression implementing nat/add?
+
+nat/add : N × N → N
+
+Must be uncurried from primitive recursion:
+
+(curry nat/add) = (pr X F) : N → [N, N]
+X : 1 → [N, N]
+F : [N, N] → [N, N]
+
+Forall n, 0 + n = n, so:
+
+(comp (pair zero id) nat/add) = id : N → N
+
+This means that X must name a function N → N which sends every n to n:
+
+X = (name id) = (curry snd) : 1 → [N, N]
+
+F must be uncurried:
+
+(uncurry F) : [N, N] × N → N
+
+We need to apply and +1. This is the smallest way to do that:
+
+(comp app succ) = (comp (uncurry id) succ) : [N, N] × N → N
+
+So:
+
+(uncurry F) = (comp app succ) : [N, N] × N → N
+F = (curry (comp app succ)) : [N, N] → [N, N]

--- /dev/null
+++ b/ski2cammy.py
@@ -0,0 +1,36 @@
+#!/usr/bin/env python3
+# nix-shell -i python3 -p python3
+
+# A simple parser and translator from SKI combinator calculus to Cammy.
+# Well-formedness of input and well-typedness of output are not enforced.
+
+def parse(expr):
+    stack = [[]]
+    for char in expr:
+        if char == "(":
+            stack.append([])
+        elif char == ")":
+            row = stack.pop()
+            stack[-1].append(row)
+        elif char in "SKIBCW":
+            stack[-1].append(char)
+    return stack[-1]
+
+expr = parse("S(K(S(S K K)(S K K)))(S(S(K S)(S(K K)(S K K)))(K(S(S K K)(S K K))))")
+
+print(expr)
+
+templates = {
+    "K": "(curry fst)",
+    "S": "(curry (curry (comp (pair (comp (pair (comp fst fst) snd) app) (comp (pair (comp fst snd) snd) app)) app)))",
+}
+
+def translate(tree):
+    if isinstance(tree, str):
+        return templates[tree]
+    else:
+        # Trust input; don't check arity.
+        expr = translate(tree[0])
+        for t in tree[1:]:
+            expr = "(comp (pair %s %s) app)" % (expr, translate(t))
+        return expr

Binary files /dev/null and b/wallpapers/burning-ship-color.png differ

Binary files /dev/null and b/wallpapers/burning-ship.png differ