A categorical programming language
| 修订版 | 9640f4207ce3d8b2dcde993aff87999e7e330bfc (tree) |
|---|---|
| 时间 | 2021-08-25 12:21:08 |
| 作者 | Corbin <cds@corb...> |
| Commiter | Corbin |
movelist: Change cammy° to a ternary relation.
We obtain the desired consequence: For a little less code overall, we
can now provide input and output types, and search for Cammy expressions
which implement the given types.
movelist.scm (diff)
todo.txt (diff)| @@ -2,73 +2,65 @@ | ||
| 2 | 2 | (import (matchable)) |
| 3 | 3 | (import (mini-kanren)) |
| 4 | 4 | |
| 5 | -(define type-goal | |
| 6 | - (match-lambda | |
| 7 | - ['id (lambda (s t) (== s t))] | |
| 8 | - [('comp f g) | |
| 9 | - (lambda (x z) (fresh (y) ((type-goal f) x y) ((type-goal g) y z)))] | |
| 10 | - ['ignore (lambda (s t) (== t 'unit))] | |
| 11 | - ['fst (lambda (s t) (fresh (x) (== s (cons t x))))] | |
| 12 | - ['snd (lambda (s t) (fresh (x) (== s (cons x t))))] | |
| 13 | - [('pair f g) | |
| 14 | - (lambda (s t) | |
| 15 | - (fresh (p1 p2) | |
| 16 | - (== t (cons p1 p2)) ((type-goal f) s p1) ((type-goal g) s p2)))] | |
| 17 | - ['dup (type-goal '(pair id id))] | |
| 18 | - ['swap (lambda (s t) (fresh (x y) (== s (cons x y)) (== t (cons y x))))] | |
| 19 | - ['left (lambda (s t) (fresh (x) (== t (list 'sum s x))))] | |
| 20 | - ['right (lambda (s t) (fresh (x) (== t (list 'sum x s))))] | |
| 21 | - [('case f g) | |
| 22 | - (lambda (s t) | |
| 23 | - (fresh (s1 s2) | |
| 24 | - (== s (list 'sum s1 s2)) ((type-goal f) s1 t) ((type-goal g) s2 t)))] | |
| 25 | - ['assl | |
| 26 | - (lambda (s t) | |
| 27 | - (fresh (x y z) (== s (cons x (cons y z))) (== t (cons (cons x y) z))))] | |
| 28 | - ['assr | |
| 29 | - (lambda (s t) | |
| 30 | - (fresh (x y z) (== s (cons (cons x y) z)) (== t (cons x (cons y z)))))] | |
| 31 | - [('curry f) | |
| 32 | - (lambda (s t) | |
| 33 | - (fresh (x y z) | |
| 34 | - ((type-goal f) (cons x y) z) (== s x) (== t (list 'hom y z))))] | |
| 35 | - [('uncurry f) | |
| 36 | - (lambda (s t) | |
| 37 | - (fresh (x y z) | |
| 38 | - ((type-goal f) x (list 'hom y z)) (== s (cons x y)) (== t z)))] | |
| 39 | - ['app (lambda (s t) (fresh (x) (== s (cons (list 'hom x t) x))))] | |
| 40 | - [('name f) | |
| 41 | - (lambda (s t) | |
| 42 | - (fresh (x y) ((type-goal f) x y) (== s 'unit) (== t (list 'hom x y))))] | |
| 43 | - ['t (lambda (s t) (== (list s t) '(unit truth)))] | |
| 44 | - ['f (lambda (s t) (== (list s t) '(unit truth)))] | |
| 45 | - ['not (lambda (s t) (== (list s t) '(truth truth)))] | |
| 46 | - ['conj (lambda (s t) (== (list s t) '((truth . truth) truth)))] | |
| 47 | - ['disj (lambda (s t) (== (list s t) '((truth . truth) truth)))] | |
| 48 | - ['zero (lambda (s t) (== (list s t) '(unit N)))] | |
| 49 | - ['succ (lambda (s t) (== (list s t) '(N N)))] | |
| 50 | - [('pr x f) | |
| 51 | - (lambda (s t) | |
| 52 | - (fresh () (== s 'N) ((type-goal x) 'unit t) ((type-goal f) t t)))] | |
| 53 | - ['nil (lambda (s t) (fresh (l) (== s 'unit) (== t (list 'list l))))] | |
| 54 | - ['cons | |
| 55 | - (lambda (s t) | |
| 56 | - (fresh (l) (let ((x (list 'list l))) (== s (cons l x)) (== t x))))] | |
| 57 | - [('fold x f) | |
| 58 | - (lambda (s t) | |
| 59 | - (fresh (l) | |
| 60 | - (== s (list 'list l)) | |
| 61 | - ((type-goal x) 'unit t) | |
| 62 | - ((type-goal f) (cons l t) t)))] | |
| 63 | - [('map f) | |
| 64 | - (lambda (s t) | |
| 65 | - (fresh (x y) | |
| 66 | - ((type-goal f) x y) | |
| 67 | - (== s (list 'list x)) | |
| 68 | - (== t (list 'list y))))])) | |
| 5 | +; Relate a Cammy expression to its input and output types. | |
| 6 | +; cammy° is functional; expr fixes s and t together. | |
| 7 | +(define (cammyo expr s t) | |
| 8 | + ; Clauses are ordered so that expr can become grounded quickly. Since we are | |
| 9 | + ; functional in expr, we prefer literal types first, followed by structural | |
| 10 | + ; recursion (on s and t!), and finally free composition of polymorphic functors. | |
| 11 | + (conde | |
| 12 | + ; Literal t. | |
| 13 | + ((== expr 'ignore) (== t 'unit)) | |
| 14 | + ; Literal s and t. | |
| 15 | + ((== expr 't) (== s 'unit) (== t 'truth)) | |
| 16 | + ((== expr 'f) (== s 'unit) (== t 'truth)) | |
| 17 | + ((== expr 'not) (== s 'truth) (== t 'truth)) | |
| 18 | + ((== expr 'conj) (== s (cons 'truth 'truth)) (== t 'truth)) | |
| 19 | + ((== expr 'disj) (== s (cons 'truth 'truth)) (== t 'truth)) | |
| 20 | + ((== expr 'zero) (== s 'unit) (== t 'N)) | |
| 21 | + ((== expr 'succ) (== s 'N) (== t 'N)) | |
| 22 | + ; Literal s, recursive t. | |
| 23 | + ((== expr 'nil) (== s 'unit) (fresh (l) (== t (list 'list l)))) | |
| 24 | + ((fresh (f x y) (== expr (list 'name f)) | |
| 25 | + (== s 'unit) (== t (list 'hom x y)) (cammyo f x y))) | |
| 26 | + ((fresh (x f) (== expr (list 'pr x f)) | |
| 27 | + (== s 'N) (cammyo x 'unit t) (cammyo f t t))) | |
| 28 | + ; Parametric polymorphism with structural recursion on both sides. | |
| 29 | + ((== expr 'swap) (fresh (x y) (== s (cons x y)) (== t (cons y x)))) | |
| 30 | + ((== expr 'assl) | |
| 31 | + (fresh (x y z) (== s (cons x (cons y z))) (== t (cons (cons x y) z)))) | |
| 32 | + ((== expr 'assr) | |
| 33 | + (fresh (x y z) (== s (cons (cons x y) z)) (== t (cons x (cons y z))))) | |
| 34 | + ((== expr 'cons) (fresh (l) (== s (cons l t)) (== t (list 'list l)))) | |
| 35 | + ((fresh (f y z) (== expr (list 'curry f)) | |
| 36 | + (== t (list 'hom y z)) (cammyo f (cons s y) z))) | |
| 37 | + ((fresh (f x y) (== expr (list 'uncurry f)) | |
| 38 | + (== s (cons x y)) (cammyo f x (list 'hom y t)))) | |
| 39 | + ((fresh (x f l) (== expr (list 'fold x f)) | |
| 40 | + (== s (list 'list l)) (cammyo x 'unit t) (cammyo f (cons l t) t))) | |
| 41 | + ((fresh (f x y) (== expr (list 'map f)) | |
| 42 | + (== s (list 'list x)) (== t (list 'list y)) (cammyo f x y))) | |
| 43 | + ; Parametric polymorphism on both sides, but one side recurses. | |
| 44 | + ((== expr 'fst) (fresh (x) (== s (cons t x)))) | |
| 45 | + ((== expr 'snd) (fresh (x) (== s (cons x t)))) | |
| 46 | + ((fresh (f g p1 p2) (== expr (list 'pair f g)) | |
| 47 | + (== t (cons p1 p2)) (cammyo f s p1) (cammyo g s p2))) | |
| 48 | + ((== expr 'dup) (== t (cons s s))) | |
| 49 | + ((== expr 'left) (fresh (x) (== t (list 'sum s x)))) | |
| 50 | + ((== expr 'right) (fresh (x) (== t (list 'sum x s)))) | |
| 51 | + ((fresh (f g s1 s2) (== expr (list 'case f g)) | |
| 52 | + (== s (list 'sum s1 s2)) (cammyo f s1 t) (cammyo g s2 t))) | |
| 53 | + ((== expr 'app) (fresh (x) (== s (cons (list 'hom x t) x)))) | |
| 54 | + ; Parametric polymorphism on both sides. | |
| 55 | + ((== expr 'id) (== s t)) | |
| 56 | + ((fresh (f g y) (== expr (list 'comp f g)) | |
| 57 | + (cammyo f s y) (cammyo g y t))))) | |
| 69 | 58 | |
| 70 | 59 | (define (type-check expr) |
| 71 | - (run 1 (q) (fresh (s t) (== q (list s t)) ((type-goal expr) s t)))) | |
| 60 | + (car (run 1 (q) (fresh (s t) (== q (list s t)) (cammyo expr s t))))) | |
| 61 | + | |
| 62 | +(define (djinn x s t) | |
| 63 | + (run x (q) (cammyo q s t))) | |
| 72 | 64 | |
| 73 | 65 | (begin |
| 74 | 66 | (display (type-check (read))) |
| @@ -2,6 +2,7 @@ | ||
| 2 | 2 | * list/zip : [X] × [Y] → [X × Y] |
| 3 | 3 | * list/tail : [X] → [X] |
| 4 | 4 | * list/unfold : [Y, X × Y + 1] → [Y, [X]] |
| 5 | +* list/append : [X] × [X] → [X] | |
| 5 | 6 | * rat |
| 6 | 7 | * jelly: zero (pr ...), succ (pr ...), nil (fold ...), cons (fold ...) can all |
| 7 | 8 | be unrolled one step, allowing for loops to be inlined |
Fork