#lang typed/racket
(: + (→ Number Number
Number))
(define +
(λ (n m)
(cond
[(zero? n) m]
#|(+ (sub1 n) m) is the natural recursion
+ recurs on n, because (zero? n) terminates recursion
so at each step, (sub1 n) makes recursion closer to termination.
|#
#|(add1 ..) is a wrapper that takes the result of natural recursion
to the result we want|#
[else (add1 (+ (sub1 n) m))])))
#;
(+ 17 5)
(: * (→ Number Number
Number))
(define *
(λ (n m)
(cond
[(zero? n) 0]
[else (+ m (* (sub1 n) m))])))
(: ↑ (→ Number Number
Number))
(define ↑
(λ (n m)
(cond
[(zero? m) 1]
[else (* n (↑ n (sub1 m)))])))
#;
(↑ 3 5)
(: count-occurs (All (A) (→ A (Listof A)
Number)))
(define count-occurs
(λ (x ls)
(cond
[(null? ls) 0]
#|car takes the first one from the list|#
#|cdr takes everything but the first one from the list|#
[(eqv? (car ls) x) (add1 (count-occurs x (cdr ls)))]
[else (count-occurs x (cdr ls))])))
#;
(count-occurs ‘b ‘(a b c b))
#;
(count-occurs 42 ‘(1 2 42 42 3))
(: member? (All (A) (→ A (Listof A)
Boolean)))
(define member?
(λ (x ls)
(cond
[(null? ls) #f]
[else (or (eqv? (car ls) x) (member? x (cdr ls)))])))
#;
(member? ‘cat ‘(cat dog dog))
#;
(define count-occurs*
(λ (x ls)
(cond
[(null? ls) 0]
[(pair? (car ls)) (+ (count-occurs* x (car ls))
(count-occurs* x (cdr ls)))]
[(eqv? (car ls) x) (add1 (count-occurs* x (cdr ls)))]
[else (count-occurs* x (cdr ls))])))
#;
(count-occurs 42 ‘(1 2 42 42 42 3))
#lang typed/racket
#||#
#;
(: + (→ Number Number Number))
#;
(define +
(λ (n m)
(cond
[(zero? m) n]
[else (add1 (+ n (sub1 m)))])))
#;
(: * (→ Number Number Number))
#;
(define *
(λ (n m)
(cond
[(zero? m) 0]
[else (+ n (* n (sub1 m)))])))
#;
(: ↑ (→ Number Number Number))
#;
(define ↑
(λ (n m)
(cond
[(zero? m) 1]
[else (* n (↑ n (sub1 m)))])))
#;
(: ⇑ (→ Number Number Number))
#;
(define ⇑
(λ (n m)
(cond
[(zero? m) 1]
[else (↑ n (⇑ n (sub1 m)))])))
#|We are gonna use higher-order functions(functions whose inputs and outputs
can be other functions) to generate an arrow with 100 hats|#
#|G takes an index(number) and spits out a function that looks like one of
the above|#
#|a variation of the Ackermann function,
the first known general recursion function|#
(: G (→ Number (→ Number Number Number)))
(define G
(λ (i)
(λ (n m)
(cond
[(zero? i)
(cond
[(zero? m) n]
[else (add1 ((G 0) n (sub1 m)))])]
[(zero? m)
(cond
[(zero? (sub1 i)) 0]
[else 1])]
[else
((G (sub1 i)) n ((G i) n (sub1 m)))]))))
#|higher-order functions are not really needed here|#
#;
(: G (→ Number Number Number Number))
#;
(define G
(λ (i n m)
(cond
[(zero? i)
(cond
[(zero? m) n]
[else (add1 (G 0 n (sub1 m)))])]
[(zero? m)
(cond
[(zero? (sub1 i)) 0]
[else 1])]
[else
(G (sub1 i) n (G i n (sub1 m)))])))
#|the Ackermann function|#
(: A (→ Number Number Number))
(define A
(λ (m n)
(cond
[(zero? m)
(add1 n)]
[(zero? n)
(A (sub1 m) 1)]
[else
(A (sub1 m) (A m (sub1 n)))])))
#lang typed/racket/no-check
#|
– match
|#
;(: some-sentence (Listof Symbol))
(: some-sentence (List ‘mary ‘had Number ‘little ‘lamb))
(define some-sentence
‘(mary had 1 little lamb))
#|
‘(mary had a little lamb) is the short hand for
(cons ‘mary (cons ‘had (cons ‘a (cons ‘little (cons ‘lamb ‘())))))
|#
#|
quasiquote (`) is like quote (‘) — named by Willard Van Orman Quine
except that you can use commas (,) inside the sentence
commas introduce variables
|#
#;
((λ (x)
(match x
[`(,person had ,n little ,animal) `(,person ,n ,animal)]
[whatever ‘nothing-matched]))
some-sentence)
#|
λ-calculus:
a λ-expression is one of the following.
– y if y is a symbol
– (λ (x) body) if x is symbol and body is a λ-expression
– (rator rand) if rator and rand are λ-expressions
|#
(define-type Exp
(U Symbol
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
#|tabNine|#
(: exp? (→ Any Boolean))
(define exp?
(λ (x)
(match x
[`,y
#:when (symbol? y)
#t]
[`(λ (,x) ,body)
(and (symbol? x) (exp? body))]
[`(,rator ,rand)
(and (exp? rator) (exp? rand))]
[`,whatever
#f])
#;
#|Something’s not quite right here.|#
(cond
[(symbol? x) #t]
[(and (pair? x)
(eqv? (car x) ‘λ)
(and (pair? (car (cdr x)))
(symbol? (car (car (cdr x))))
(null? (cdr (car (cdr x)))))
(exp? (car (cdr (cdr x))))
(null? (cdr (cdr (cdr x)))))
#t]
[(and (pair? x)
(exp? (car x))
(exp? (car (cdr x)))
(null? (cdr (cdr x))))
#t]
[else
#f])))
#;
(exp? `((λ (x) (x x)) (λ (x) (x x))))
#|
L0
– Number
– `(pluz L0 L0)
– `(monus L0 L0)
|#
(define-type L0
(U Number
(List ‘pluz L0 L0)
(List ‘monus L0 L0)))
(: L0? (→ Any Boolean))
(define L0?
(λ (x)
(match x
[`,n
#:when (number? n)
#t]
[`(pluz ,e₁ ,e₂)
(and (L0? e₁) (L0? e₂))]
[`(monus ,e₁ ,e₂)
(and (L0? e₁) (L0? e₂))]
[`,whatever
#f])))
(: valof (→ L0 Number))
(define valof
(λ (e)
(match e
[`,n
#:when (number? n)
n]
[`(pluz ,e₁ ,e₂)
(+ (valof e₁) (valof e₂))]
[`(monus ,e₁ ,e₂)
(- (valof e₁) (valof e₂))])))
(valof ‘(monus (pluz (pluz 3 5) 10) 8))
#lang typed/racket/no-check
(require typed/rackunit)
(define-type Exp
(U Symbol
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
#|λ-encoding of three|#
(define three
(λ (step)
(λ (base)
(step (step (step base))))))
#|
(λ (x) (y (λ (x) x)))
y occurs free
x occurs bound
|#
(: occurs-free? (→ Symbol Exp
Boolean))
(define occurs-free?
(λ (a e)
(match e
[`,y
#:when (symbol? y)
(eqv? y a)]
[`(λ (,x) ,body)
(and (not (eqv? x a)) (occurs-free? a body))]
[`(,rator ,rand)
#|Always start with the last line!|#
(or (occurs-free? a rator) (occurs-free? a rand))])))
(check-eqv? (occurs-free? ‘x ‘y) #f)
(check-eqv? (occurs-free? ‘x ‘x) #t)
(check-eqv? (occurs-free? ‘z ‘(x y)) #f)
(check-eqv? (occurs-free? ‘z ‘(x z)) #t)
(check-eqv? (occurs-free? ‘z ‘((x z) (x y))) #t)
(check-eqv? (occurs-free? ‘z ‘(λ (z) ((x z) (x y)))) #f)
(: occurs-bound? (→ Symbol Exp
Boolean))
(define occurs-bound?
(λ (a e)
(match e
[`,y
#:when (symbol? y)
#f]
[`(λ (,x) ,body)
(or (and (eqv? x a) (occurs-free? a body))
(occurs-bound? a body))]
[`(,rator ,rand)
(or (occurs-bound? a rator) (occurs-bound? a rand))])))
(check-eqv? (occurs-bound? ‘x ‘y) #f)
(check-eqv? (occurs-bound? ‘x ‘x) #f)
(check-eqv? (occurs-bound? ‘x ‘(λ (x) (λ (x) x))) #t)
(check-eqv? (occurs-bound? ‘z ‘(λ (z) (x y))) #f)
(check-eqv? (occurs-bound? ‘z ‘(x z)) #f)
(check-eqv? (occurs-bound? ‘z ‘((x z) (x y))) #f)
(check-eqv? (occurs-bound? ‘z ‘(λ (z) ((x z) (x y)))) #t)
#|
de Bruijn indices: a means to compare expressions without worrying about the names
for example:
(λ (a) (λ (b) (a b))) and (λ (x) (λ (y) (x y)))
are two different Exp.
But we can convert them using de Bruijn indices and
(λ (λ (1 0))) and (λ (λ (1 0)))
are the same DExp.
|#
(define-type DExp
(U Number #|variables are now represented by numbers|#
(List ‘λ DExp) #|names are not nessesary here|#
(List DExp DExp)))
#|
for example
(λ (a)
(a (λ (b)
((λ (a)
(λ (c)
(λ (a)
(λ (d)
((a c) d))))) b))))
converts to
(λ
(0 (λ
((λ
(λ
(λ
(λ
((1 2) 0))))) 0))))
|#
#lang typed/racket
(define-type Exp
(U Symbol
Number
Boolean
(List ‘+ Exp Exp)
(List ‘- Exp Exp)
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
#|An environment can look up a symbol and return a Val|#
(define-type Env
(→ Symbol Val))
(define-type Closure
(→ Val Val))
(define-type Val
(U Number
Boolean
Closure))
#|An interpreter converts an Exp together with an Env to a Val|#
(: valof (→ Exp Env
Val))
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`,b
#:when (boolean? b)
b]
[`(+ ,e₁ ,e₂)
(let ([r₁ (valof e₁ env)]
[r₂ (valof e₂ env)])
(cond
[(and (number? r₁) (number? r₂))
(+ r₁ r₂)]
[else (error “don’t be silly”)]))]
[`(- ,e₁ ,e₂)
(let ([r₁ (valof e₁ env)]
[r₂ (valof e₂ env)])
(cond
[(and (number? r₁) (number? r₂))
(- r₁ r₂)]
[else (error “don’t be silly”)]))]
[`(λ (,x) ,body)
(λ ([a : Val]) (valof body (λ ([y : Symbol]) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
(let ([clos (valof rator env)]
[a (valof rand env)])
(cond
[(or (number? clos) (boolean? clos)) (error “don’t be silly”)]
[else (clos a)]))])))
#;
(valof ‘(((λ (x) (λ (y) (+ x y))) 3) 5)
(λ (y) (error “oops”)))
(valof ‘(((λ (x) (λ (y) (- y x))) 5) 6)
(λ (y) (error “oops”)))
#;
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`(λ (,x) ,body)
(λ (a) (valof body (λ (y) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
((valof rator env) (valof rand env))])))
#lang typed/racket
#|
Representation Independence
How to get rid of higher-order functions:
A higher-order function is a function that is passed
as an input to another function, or a function that is
used as the result of another function.
|#
(define-type Exp
(U Symbol
Number
(List ‘+ Exp Exp)
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
(define-type Env
(Listof (Pairof Symbol Val))
#;
(→ Symbol Val))
(define-type Closure
(→ Val Val))
(define-type Val
(U Number
Boolean
Closure))
(: init-env (→ Env))
(define init-env
(λ ()
‘()
#;
(λ (y) (error “unbound variable” y))))
(: extend-env (→ Symbol Val Env
Env))
(define extend-env
(λ (x a env)
`((,x . ,a) . ,env)
#;
(λ (y) (if (eqv? y x) a (apply-env env y)))))
(: apply-env (→ Env Symbol
Val))
(define apply-env
(λ (env y)
(match env
[`() (error “unbound variable” y)]
[`((,x . ,a) . ,env^) (if (eqv? y x) a (apply-env env^ y))])
#;
(env y)))
(: valof (→ Exp Env
Val))
(define valof
(λ (exp env)
(displayln exp)
(displayln env)
(match exp
[`,y
#:when (symbol? y)
(apply-env env y)]
[`,n
#:when (number? n)
n]
[`(+ ,e₁ ,e₂)
(let ([r₁ (valof e₁ env)]
[r₂ (valof e₂ env)])
(cond
[(and (number? r₁) (number? r₂))
(+ r₁ r₂)]
[else (error “adding non-numbers”)]))]
[`(λ (,x) ,body)
(λ ([a : Val]) (valof body (extend-env x a env)))]
[`(,rator ,rand)
(let ([clos (valof rator env)]
[a (valof rand env)])
(cond
[(or (number? clos) (boolean? clos)) (error “your rator is not a function”)]
[else (clos a)]))])))
(valof ‘(((λ (x) (λ (y) (+ y x))) 5) 6) (init-env))
#lang typed/racket
(: memv (All (A) (→ A (Listof A) (U (Listof A) False))))
(define memv
(λ (a as)
(match as
[‘() #f]
[`(,a^ . ,d)
(if (eqv? a^ a)
as
(memv a d))])
#;
(cond
[(null? as) #f]
[else (if (eqv? (car as) a)
as
(memv a (cdr as)))])))
#;
(memv ‘x ‘(a a y z))
(let ([a 5]
[b 6])
`(a b (+ a b)))
(define minus
(lambda (n1 n2)
(cond
[(zero? n2) n1]
[else (sub1
(minus n1 (sub1 n2)))])))
#lang typed/racket
;(require racket/trace)
#|
– context
– factorial
– CPS-rules
— tail call & serious call
– stack
|#
#|
Serious calls are the functions you defined,
especially the recursive ones.
Simple calls are those from Racket.
A tail call is function calls with no immediate context.
e.g. g in (g x) is a tail call, g in (f (g x)) is not a
tail call.
|#
#|
rules to CPS:
1, change the names, add -cps to every function
2, use lets to move the serious calls to tail position
3, add a k parameter to every lambda
4, rewrite lets using lambdas, note that every function
now takes an extra argument.
5, return the simple values by applying k to it, note that
lambdas are simple
|#
#;
(define fib
(λ (n)
(cond
[(zero? n) 1]
[(zero? (sub1 n)) 1]
[else (let ([hole₁ (fib (sub1 n))])
(let ([hole₂ (fib (sub1 (sub1 n)))])
(+ hole₁ hole₂)))])))
(: fib-cps (→ Number (→ Number Number)
Number))
(define fib-cps
(λ (n k)
(cond
[(zero? n) (k 1)]
[(zero? (sub1 n)) (k 1)]
[else (fib-cps (sub1 n)
(λ (hole₁)
(fib-cps (sub1 (sub1 n))
(λ (hole₂)
(k (+ hole₁ hole₂))))))])))
#;
(trace fib-cps)
#;
(fib-cps 10 (λ (v) v))
(: plus (→ Number (→ Number Number)))
(define plus
(λ (m)
(λ (n)
(+ m n))))
#;
(let ([f (plus 3)])
(f 5))
(: plus-cps (→ Number (→ (→ Number (→ Number Number) Number) (→ Number (→ Number Number) Number))
(→ Number (→ Number Number) Number)))
(define plus-cps
(λ (m k)
(k (λ (n k)
(k (+ m n))))))
#;
(plus-cps 3 (λ (f) (f 5 (λ (v) v))))
(: map-cps (All (A B) (→ (→ A (→ B (Listof B)) (Listof B)) (Listof A) (→ (Listof B) (Listof B))
(Listof B))))
(define map-cps
(λ (f-cps ls k)
(cond
[(null? ls) (k ‘())]
[else (map-cps f-cps (cdr ls)
(λ ([d : (Listof B)])
(f-cps (car ls)
(λ ([a : B])
(k (cons a d))))))]
#;
[else (let ([a (f-cps (car ls))]
[d (map-cps f-cps (cdr ls))])
(cons a d))])))
#;
(define add1-cps
(λ (n k)
(k (add1 n))))
#;
(map-cps add1-cps ‘(1 2 3) (λ (v) v))
#lang racket
(require racket/trace)
(define !-cps
(λ (n k)
(cond
[(zero? n) (k 1)]
[else (!-cps (sub1 n)
(λ (!-of-sub1)
(k (* n !-of-sub1))))])))
(define fib
(λ (n)
(cond
[(zero? n) 1]
[(zero? (sub1 n)) 1]
[else (+ (fib (sub1 n))
(fib (sub1 (sub1 n))))])))
(trace fib)
#;
(fib 10)
(define fib-cps
(λ (n k)
(cond
[(zero? n) (k 1)]
[(zero? (sub1 n)) (k 1)]
[else (fib-cps (sub1 n)
(λ (fib-of-sub1)
(fib-cps (sub1 (sub1 n))
(λ (fib-of-sub2)
(k (+ fib-of-sub1 fib-of-sub2))))))])))
(trace fib-cps)
#;
(fib-cps 10 (λ (v) v))
#|
In a cps-ed function, all serious calls have to be in tail positions.
|#
(define valof-cps
(λ (exp env k)
(match exp
[`,y
#:when (symbol? y)
(k (env y))]
[`,n
#:when (number? n)
(k n)]
[`(+ ,e₁ ,e₂)
(valof-cps e₁ env
(λ (n₁)
(valof-cps e₂ env
(λ (n₂)
(k (+ n₁ n₂))))))]
#|(let/cc kvar body) is like (let ([kvar k]) body) where k is the current continuation|#
[`(let/cc ,kvar ,body)
(valof-cps body (λ (y) (if (eqv? y kvar) k (env y))) k)]
[`(throw ,ke ,ve)
(valof-cps ke env
(λ (k^)
(valof-cps ve env
k^
#;
(λ (v)
(k^ v)))))]
[`(λ (,x) ,body)
#|this is the short-hand of the following|#
(k (λ (a k^) (valof-cps body (λ (y) (if (eqv? y x) a (env y)))
k^)))
#;
(k (λ (a k^) (valof-cps body (λ (y) (if (eqv? y x) a (env y)))
(λ (v) (k^ v)))))]
[`(,rator ,rand)
(valof-cps rator env
(λ (closure)
(valof-cps rand env
(λ (a)
#|this is the short-hand of the following|#
(closure a k)
#;
(closure a (λ (v) (k v)))))))])))
(valof-cps ‘(let/cc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10))
(λ (y) (error “unbound ” y))
(λ (v) v))
#lang racket
#;
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`(+ ,e₁ ,e₂)
(+ (valof e₁ env) (valof e₂ env))]
[`(letcc ,kvar ,body)
#|cc means current-continuation|#
(let/cc cc (valof body (λ (y) (if (eqv? y kvar) cc (env y)))))]
[`(throw ,kexp ,vexp)
((valof kexp env) (valof vexp env))]
[`(λ (,x) ,b)
(λ (a) (valof b (λ (y) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
((valof rator env) (valof rand env))])))
#;
(valof ‘(+ 1 (letcc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y)))
(define valof-cps
(λ (exp env cc)
(match exp
[`,y
#:when (symbol? y)
(env y cc)]
[`,n
#:when (number? n)
(apply-k cc n)]
[`(+ ,e₁ ,e₂)
(valof-cps e₁ env
(λ (n₁)
(valof-cps e₂ env
(λ (n₂)
(apply-k cc (+ n₁ n₂))))))]
[`(let/cc ,kvar ,body)
#|when valof is cpsed, we don’t need Racket’s let/cc to implement ours|#
(valof-cps body (λ (y k) (if (eqv? y kvar) (apply-k k cc) (env y k))) cc)]
[`(throw ,kexp ,vexp)
(valof-cps kexp env
(λ (k)
(valof-cps vexp env k)))]
[`(λ (,x) ,body)
(apply-k cc (λ (a k₁) (valof-cps body (λ (y k₂) (if (eqv? y x) (apply-k k₂ a) (env y k₂))) k₁)))]
[`(,rator ,rand)
(valof-cps rator env
(λ (closure)
(valof-cps rand env
(λ (a)
(closure a cc)))))])))
(define apply-k
(λ (cc v)
(cc v)))
(valof-cps ‘(+ 1 (let/cc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y))
(λ (v) v))
#lang racket
#;
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`(+ ,e₁ ,e₂)
(+ (valof e₁ env) (valof e₂ env))]
[`(letcc ,kvar ,body)
#|cc means current-continuation|#
(let/cc cc (valof body (λ (y) (if (eqv? y kvar) cc (env y)))))]
[`(throw ,kexp ,vexp)
((valof kexp env) (valof vexp env))]
[`(λ (,x) ,b)
(λ (a) (valof b (λ (y) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
((valof rator env) (valof rand env))])))
#;
(valof ‘(+ 1 (letcc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y)))
(define valof-cps
(λ (exp env cc)
(match exp
[`,y
#:when (symbol? y)
(env y cc)]
[`,n
#:when (number? n)
(apply-k cc n)]
[`(+ ,e₁ ,e₂)
(valof-cps e₁ env (make-k-+-e₁ e₂ env cc))]
[`(let/cc ,kvar ,body)
#|when valof is cpsed, we don’t need Racket’s let/cc to implement ours|#
(valof-cps body (λ (y k) (if (eqv? y kvar) (apply-k k cc) (env y k))) cc)]
[`(throw ,kexp ,vexp)
(valof-cps kexp env (make-k-throw vexp env))]
[`(λ (,x) ,body)
(apply-k cc (λ (a k₁) (valof-cps body (λ (y k₂) (if (eqv? y x) (apply-k k₂ a) (env y k₂))) k₁)))]
[`(,rator ,rand)
(valof-cps rator env (make-k-rator rand env cc))])))
(define make-k-+-e₁
(λ (e₂ env cc)
(λ (n₁)
(valof-cps e₂ env (make-k-+-e₂ cc n₁)))))
(define make-k-+-e₂
(λ (cc n₁)
(λ (n₂)
(apply-k cc (+ n₁ n₂)))))
(define make-k-throw
(λ (vexp env)
(λ (k)
(valof-cps vexp env k))))
(define make-k-rator
(λ (rand env cc)
(λ (closure)
(valof-cps rand env (make-k-rand closure cc)))))
(define make-k-rand
(λ (closure cc)
(λ (a)
(closure a cc))))
(define make-init-k
(λ ()
(λ (v) v)))
(define apply-k
(λ (cc v)
(cc v)))
(valof-cps ‘(+ 1 (let/cc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y))
(make-init-k))
#lang racket
#;
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`(+ ,e₁ ,e₂)
(+ (valof e₁ env) (valof e₂ env))]
[`(letcc ,kvar ,body)
#|cc means current-continuation|#
(let/cc cc (valof body (λ (y) (if (eqv? y kvar) cc (env y)))))]
[`(throw ,kexp ,vexp)
((valof kexp env) (valof vexp env))]
[`(λ (,x) ,b)
(λ (a) (valof b (λ (y) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
((valof rator env) (valof rand env))])))
#;
(valof ‘(+ 1 (letcc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y)))
(define valof-cps
(λ (exp env cc)
(match exp
[`,y
#:when (symbol? y)
(env y cc)]
[`,n
#:when (number? n)
(apply-k cc n)]
[`(+ ,e₁ ,e₂)
(valof-cps e₁ env (make-k-+-e₁ e₂ env cc))]
[`(let/cc ,kvar ,body)
#|when valof is cpsed, we don’t need Racket’s let/cc to implement ours|#
(valof-cps body (λ (y k) (if (eqv? y kvar) (apply-k k cc) (env y k))) cc)]
[`(throw ,kexp ,vexp)
(valof-cps kexp env (make-k-throw vexp env))]
[`(λ (,x) ,body)
(apply-k cc (λ (a k₁) (valof-cps body (λ (y k₂) (if (eqv? y x) (apply-k k₂ a) (env y k₂))) k₁)))]
[`(,rator ,rand)
(valof-cps rator env (make-k-rator rand env cc))])))
(define make-k-+-e₁
(λ (e₂ env cc)
(λ (v)
(valof-cps e₂ env (make-k-+-e₂ cc v)))))
(define make-k-+-e₂
(λ (cc n₁)
(λ (v)
(apply-k cc (+ n₁ v)))))
(define make-k-throw
(λ (vexp env)
(λ (v)
(valof-cps vexp env v))))
(define make-k-rator
(λ (rand env cc)
(λ (v)
(valof-cps rand env (make-k-rand v cc)))))
(define make-k-rand
(λ (closure cc)
(λ (v)
(closure v cc))))
(define make-init-k
(λ ()
(λ (v)
v)))
(define apply-k
(λ (cc v)
(cc v)))
(valof-cps ‘(+ 1 (let/cc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y))
(make-init-k))
#lang racket
#;
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`(+ ,e₁ ,e₂)
(+ (valof e₁ env) (valof e₂ env))]
[`(letcc ,kvar ,body)
#|cc means current-continuation|#
(let/cc cc (valof body (λ (y) (if (eqv? y kvar) cc (env y)))))]
[`(throw ,kexp ,vexp)
((valof kexp env) (valof vexp env))]
[`(λ (,x) ,b)
(λ (a) (valof b (λ (y) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
((valof rator env) (valof rand env))])))
#;
(valof ‘(+ 1 (letcc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y)))
(define valof-cps
(λ (exp env cc)
(match exp
[`,y
#:when (symbol? y)
(env y cc)]
[`,n
#:when (number? n)
(apply-k cc n)]
[`(+ ,e₁ ,e₂)
(valof-cps e₁ env (make-k-+-e₁ e₂ env cc))]
[`(let/cc ,kvar ,body)
#|when valof is cpsed, we don’t need Racket’s let/cc to implement ours|#
(valof-cps body (λ (y k) (if (eqv? y kvar) (apply-k k cc) (env y k))) cc)]
[`(throw ,kexp ,vexp)
(valof-cps kexp env (make-k-throw vexp env))]
[`(λ (,x) ,body)
(apply-k cc (λ (a k₁) (valof-cps body (λ (y k₂) (if (eqv? y x) (apply-k k₂ a) (env y k₂))) k₁)))]
[`(,rator ,rand)
(valof-cps rator env (make-k-rator rand env cc))])))
(define make-k-+-e₁
(λ (e₂ env cc)
`(k-+-e₁ ,e₂ ,env ,cc)
#;
(λ (v)
(valof-cps e₂ env (make-k-+-e₂ cc v)))))
(define make-k-+-e₂
(λ (cc n₁)
`(k-+-e₂ ,cc ,n₁)
#;
(λ (v)
(apply-k cc (+ n₁ v)))))
(define make-k-throw
(λ (vexp env)
`(k-throw ,vexp ,env)
#;
(λ (v)
(valof-cps vexp env v))))
(define make-k-rator
(λ (rand env cc)
`(k-rator ,rand ,env ,cc)
#;
(λ (v)
(valof-cps rand env (make-k-rand v cc)))))
(define make-k-rand
(λ (closure cc)
`(k-rand ,closure ,cc)
#;
(λ (v)
(closure v cc))))
(define make-init-k
(λ ()
`(init-k)
#;
(λ (v)
v)))
(define apply-k
(λ (cc v)
(match cc
[`(init-k) v]
[`(k-+-e₁ ,e₂ ,env ,cc) (valof-cps e₂ env (make-k-+-e₂ cc v))]
[`(k-+-e₂ ,cc ,n₁) (apply-k cc (+ n₁ v))]
[`(k-throw ,vexp ,env) (valof-cps vexp env v)]
[`(k-rator ,rand ,env ,cc)
(valof-cps rand env (make-k-rand v cc))]
[`(k-rand ,closure ,cc) (closure v cc)]
#;
[whatever (cc v)])))
(valof-cps ‘(+ 1 (let/cc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y))
(make-init-k))
#lang racket
#;
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`(+ ,e₁ ,e₂)
(+ (valof e₁ env) (valof e₂ env))]
[`(letcc ,kvar ,body)
#|cc means current-continuation|#
(let/cc cc (valof body (λ (y) (if (eqv? y kvar) cc (env y)))))]
[`(throw ,kexp ,vexp)
((valof kexp env) (valof vexp env))]
[`(λ (,x) ,b)
(λ (a) (valof b (λ (y) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
((valof rator env) (valof rand env))])))
#;
(valof ‘(+ 1 (letcc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y)))
(define valof-cps
(λ (exp env cc)
(match exp
[`,y
#:when (symbol? y)
(env y cc)]
[`,n
#:when (number? n)
(apply-k cc n)]
[`(+ ,e₁ ,e₂)
(valof-cps e₁ env (make-k-+-e₁ e₂ env cc))]
[`(let/cc ,kvar ,body)
#|when valof is cpsed, we don’t need Racket’s let/cc to implement ours|#
(valof-cps body (λ (y k) (if (eqv? y kvar) (apply-k k cc) (env y k))) cc)]
[`(throw ,kexp ,vexp)
(valof-cps kexp env (make-k-throw vexp env))]
[`(λ (,x) ,body)
(apply-k cc (λ (a k₁) (valof-cps body (λ (y k₂) (if (eqv? y x) (apply-k k₂ a) (env y k₂))) k₁)))]
[`(,rator ,rand)
(valof-cps rator env (make-k-rator rand env cc))])))
(define make-k-+-e₁
(λ (e₂ env cc)
`(k-+-e₁ ,e₂ ,env ,cc)
#;
(λ (v)
(valof-cps e₂ env (make-k-+-e₂ cc v)))))
(define make-k-+-e₂
(λ (cc n₁)
`(k-+-e₂ ,cc ,n₁)
#;
(λ (v)
(apply-k cc (+ n₁ v)))))
(define make-k-throw
(λ (vexp env)
`(k-throw ,vexp ,env)
#;
(λ (v)
(valof-cps vexp env v))))
(define make-k-rator
(λ (rand env cc)
`(k-rator ,rand ,env ,cc)
#;
(λ (v)
(valof-cps rand env (make-k-rand v cc)))))
(define make-k-rand
(λ (closure cc)
`(k-rand ,closure ,cc)
#;
(λ (v)
(closure v cc))))
(define make-init-k
(λ ()
`(init-k)
#;
(λ (v)
v)))
(define apply-k
(λ (cc v)
(match cc
[`(init-k) v]
[`(k-+-e₁ ,e₂ ,env ,cc) (valof-cps e₂ env (make-k-+-e₂ cc v))]
[`(k-+-e₂ ,cc ,n₁) (apply-k cc (+ n₁ v))]
[`(k-throw ,vexp ,env) (valof-cps vexp env v)]
[`(k-rator ,rand ,env ,cc)
(valof-cps rand env (make-k-rand v cc))]
[`(k-rand ,closure ,cc) (closure v cc)]
#;
[whatever (cc v)])))
(valof-cps ‘(+ 1 (let/cc k (((λ (x) (λ (y) (+ y (throw k (+ (throw k y) x))))) 5) 10)))
(λ (y) (error “unbound ” y))
(make-init-k))
#lang racket
(require racket/trace)
(define fib-k #f)
(define fib-n #f)
(define apply-k-k #f)
(define apply-k-v #f)
(define fib-cps
(λ () ; fib-n fib-k
(cond
[(zero? fib-n) (begin [set! apply-k-k fib-k]
[set! apply-k-v 1]
(apply-k))]
[(zero? (sub1 fib-n)) (begin [set! apply-k-k fib-k]
[set! apply-k-v 1]
(apply-k))]
[else (begin [set! fib-k (make-k-sub1 fib-n fib-k)]
[set! fib-n (sub1 fib-n)]
(fib-cps))])))
(trace fib-cps)
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)))
(define make-k-init
(λ ()
‘(init)))
(define apply-k
(λ () ;apply-k-k apply-k-v
(match apply-k-k
[‘(init) apply-k-v]
[`(sub2 ,k ,v₁) (begin [set! apply-k-k k]
[set! apply-k-v (+ v₁ apply-k-v)]
(apply-k))]
[`(sub1 ,n ,k)
(begin [set! fib-k (make-k-sub2 k apply-k-v)]
[set! fib-n (sub1 (sub1 n))]
(fib-cps))])))
(trace apply-k)
(begin [set! fib-k (make-k-init)]
[set! fib-n 5]
(fib-cps))
#lang racket
(define fib-cps
(λ (n k)
(cond
[(zero? n) (apply-k k 1)]
[(zero? (sub1 n)) (apply-k k 1)]
[else (fib-cps (sub1 n) (make-k-sub1 n k))])))
(define make-k-sub1
(λ (n k)
(λ (v₁)
(fib-cps (sub1 (sub1 n)) (make-k-sub2 k v₁)))))
(define make-k-sub2
(λ (k v₁)
(λ (v₂)
(apply-k k (+ v₁ v₂)))))
(define apply-k
(λ (k v)
(k v)))
(fib-cps 5 (λ (v) v))
#lang racket
(define fib-cps
(λ (n k)
(cond
[(zero? n) (apply-k k 1)]
[(zero? (sub1 n)) (apply-k k 1)]
[else (fib-cps (sub1 n) (make-k-sub1 n k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)
#;
(λ (v)
(fib-cps (sub1 (sub1 n)) (make-k-sub2 k v)))))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)
#;
(λ (v)
(apply-k k (+ v₁ v)))))
(define make-k-init
(λ ()
‘(init)
#;
(λ (v) v)))
(define apply-k
(λ (k v)
(match k
[‘(init) v]
[`(sub2 ,k ,v₁) (apply-k k (+ v₁ v))]
[`(sub1 ,n ,k) (fib-cps (sub1 (sub1 n)) (make-k-sub2 k v))]
[_ (k v)])))
(fib-cps 5 (make-k-init))
#lang racket
(define fib-cps
(λ (n k)
(cond
[(zero? n) (apply-k k 1)]
[(zero? (sub1 n)) (apply-k k 1)]
[else (fib-cps (sub1 n) (make-k-sub1 n k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)
#;
(λ (v)
(fib-cps (sub1 (sub1 n)) (make-k-sub2 k v)))))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)
#;
(λ (v)
(apply-k k (+ v₁ v)))))
(define make-k-init
(λ ()
‘(init)
#;
(λ (v) v)))
(define apply-k
(λ (k v)
(match k
[‘(init) v]
[`(sub2 ,k ,v₁) (apply-k k (+ v₁ v))]
[`(sub1 ,n ,k) (fib-cps (sub1 (sub1 n)) (make-k-sub2 k v))])))
(fib-cps 5 (make-k-init))
#lang racket
(define fib-cps
(λ (n cc)
(cond
[(zero? n) (let* ([k cc]
[v 1])
(apply-k k v))]
[(zero? (sub1 n)) (let* ([k cc]
[v 1])
(apply-k k v))]
[else (let* ([k (make-k-sub1 n cc)]
[n (sub1 n)])
(fib-cps n k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)))
(define make-k-init
(λ ()
‘(init)))
(define apply-k
(λ (k v)
(match k
[‘(init) v]
[`(sub2 ,k ,v₁) (apply-k k (+ v₁ v))]
[`(sub1 ,n ,k) (fib-cps (sub1 (sub1 n)) (make-k-sub2 k v))])))
(fib-cps 5 (make-k-init))
#lang racket
#|fib in A-normal form|#
(define fib-cps
(λ (n cc)
(cond
[(zero? n) (let* ([k cc]
[v 1])
(apply-k k v))]
[(zero? (sub1 n)) (let* ([k cc]
[v 1])
(apply-k k v))]
[else (let* ([k (make-k-sub1 n cc)]
[n (sub1 n)])
(fib-cps n k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)))
(define make-k-init
(λ ()
‘(init)))
(define apply-k
(λ (k v)
(match k
[‘(init) v]
[`(sub2 ,k ,v₁) (let* ([k k]
[v (+ v₁ v)])
(apply-k k v))]
[`(sub1 ,n ,k)
(let* ([k (make-k-sub2 k v)]
[n (sub1 (sub1 n))])
(fib-cps n k))])))
(let* ([k (make-k-init)]
[n 5])
(fib-cps n k))
#lang racket
(define fib-k #f)
(define fib-n #f)
(define apply-k-k #f)
(define apply-k-v #f)
(define fib-cps
(λ (fib-n fib-k)
(cond
[(zero? fib-n) (let* ([apply-k-k fib-k]
[apply-k-v 1])
(apply-k apply-k-k apply-k-v))]
[(zero? (sub1 fib-n)) (let* ([apply-k-k fib-k]
[apply-k-v 1])
(apply-k apply-k-k apply-k-v))]
[else (let* ([fib-k (make-k-sub1 fib-n fib-k)]
[fib-n (sub1 fib-n)])
(fib-cps fib-n fib-k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)))
(define make-k-init
(λ ()
‘(init)))
(define apply-k
(λ (k v)
(match k
[‘(init) v]
[`(sub2 ,k ,v₁) (let* ([k k]
[v (+ v₁ v)])
(apply-k k v))]
[`(sub1 ,n ,k)
(let* ([k (make-k-sub2 k v)]
[n (sub1 (sub1 n))])
(fib-cps n k))])))
(let* ([k (make-k-init)]
[n 5])
(fib-cps n k))
#lang racket
(define fib-k #f)
(define fib-n #f)
(define apply-k-k #f)
(define apply-k-v #f)
(define fib-cps
(λ (fib-n fib-k)
(cond
[(zero? fib-n) (let* ([apply-k-k fib-k]
[apply-k-v 1])
(apply-k apply-k-k apply-k-v))]
[(zero? (sub1 fib-n)) (let* ([apply-k-k fib-k]
[apply-k-v 1])
(apply-k apply-k-k apply-k-v))]
[else (let* ([fib-k (make-k-sub1 fib-n fib-k)]
[fib-n (sub1 fib-n)])
(fib-cps fib-n fib-k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)))
(define make-k-init
(λ ()
‘(init)))
(define apply-k
(λ (apply-k-k apply-k-v)
(match apply-k-k
[‘(init) apply-k-v]
[`(sub2 ,k ,v₁) (let* ([apply-k-k k]
[apply-k-v (+ v₁ apply-k-v)])
(apply-k apply-k-k apply-k-v))]
[`(sub1 ,n ,k)
(let* ([fib-k (make-k-sub2 k apply-k-v)]
[fib-n (sub1 (sub1 n))])
(fib-cps fib-n fib-k))])))
(let* ([fib-k (make-k-init)]
[fib-n 5])
(fib-cps fib-n fib-k))
#lang racket
(define fib-k #f)
(define fib-n #f)
(define apply-k-k #f)
(define apply-k-v #f)
(define fib-cps
(λ () ; fib-n fib-k
(cond
[(zero? fib-n) (begin [set! apply-k-k fib-k]
[set! apply-k-v 1]
(apply-k))]
[(zero? (sub1 fib-n)) (begin [set! apply-k-k fib-k]
[set! apply-k-v 1]
(apply-k))]
[else (begin [set! fib-k (make-k-sub1 fib-n fib-k)]
[set! fib-n (sub1 fib-n)]
(fib-cps))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)))
(define make-k-init
(λ ()
‘(init)))
(define apply-k
(λ () ;apply-k-k apply-k-v
(match apply-k-k
[‘(init) apply-k-v]
[`(sub2 ,k ,v₁) (begin [set! apply-k-k k]
[set! apply-k-v (+ v₁ apply-k-v)]
(apply-k))]
[`(sub1 ,n ,k)
(begin [set! fib-k (make-k-sub2 k apply-k-v)]
[set! fib-n (sub1 (sub1 n))]
(fib-cps))])))
(begin [set! fib-k (make-k-init)]
[set! fib-n 5]
(fib-cps))
#lang typed/racket
(require typed/rackunit)
(define-type Store (Listof (Pairof Real Real)))
#;
(: store (Listof (Pairof Real Real)))
#;
(define store
‘())
#;
(: fib (→ Real Real))
#;
(define fib
(λ (n)
(cond
[(assv n store)
=>
(λ ([pr : (Pairof Real Real)])
(cdr pr))]
[(zero? n) 1]
[(zero? (sub1 n)) 1]
[else (let ([r₁ (fib (sub1 n))]
[r₂ (fib (sub1 (sub1 n)))])
(let ([r (+ r₁ r₂)])
(begin (set! store `((,n . ,r) . ,store))
r)))])))
#;
(let* ([x 5]
[y x])
(+ x y))
(define-syntax define/trace
(syntax-rules ()
[(_ name (λ (arg …) body))
(define name
(λ (arg …)
(begin
(displayln ‘name)
(displayln arg) …
(displayln “”)
body)))]))
(: fib (→ Real Store
(List Real Store)))
(define/trace fib
(λ (n store)
(cond
[(assv n store)
=>
(λ ([pr : (Pairof Real Real)])
(list (cdr pr) store))]
[(zero? n) (list 1 store)]
[(zero? (sub1 n)) (list 1 store)]
[else (match-let* ([`(,r₁ ,store) (fib (sub1 n) store)]
[`(,r₂ ,store) (fib (sub1 (sub1 n)) store)])
(let ([r (+ r₁ r₂)])
(list r `((,n . ,r) . ,store))))]
#;
[else (let ([r₁ (fib (sub1 n))]
[r₂ (fib (sub1 (sub1 n)))])
(let ([r (+ r₁ r₂)])
(begin (set! store `((,n . ,r) . ,store))
r)))])))
(: best-price (→ (Listof Real) Real
(List Real Real)))
(define best-price
(λ (l highest)
(cond
[(null? l) (list 0 highest)]
[else (match (best-price (cdr l) highest)
[(list max-profit highest)
(let ([max-profit (max max-profit (- highest (car l)))]
[highest (max (car l) highest)])
(list max-profit highest))])])))
(define-syntax test-runner
(syntax-rules (>)
[(_) ‘done]
[(_ > test result more …)
(begin (check-equal? test ‘result)
(test-runner more …))]))
(: remv-1st (→ Symbol (Listof Symbol)
(Listof Symbol)))
(define remv-1st
(λ (x ls)
(cond
[(null? ls) ‘()]
[(eqv? (car ls) x) (cdr ls)]
[else (cons (car ls) (remv-1st x (cdr ls)))])))
(test-runner
> (remv-1st ‘x ‘(x y z x))
(y z x)
> (remv-1st ‘y ‘(y z y x))
(x z y x)
> (remv-1st ‘z ‘(a b c))
(a b c))
#lang typed/racket
#|This is a call-by-name interpreter.|#
(define-type Exp
(U Symbol
Number
(List ‘+ Exp Exp)
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
(define-type Env
(Listof (Pairof Symbol (→ Val))))
(define-type Closure
(→ (→ Val) Val))
(define-type Val
(U Number
Boolean
Closure
Void))
(: init-env Env)
(define init-env ‘())
(: ext-env (→ Symbol (→ Val) Env Env))
(define ext-env
(λ (x th env)
`((,x . ,th) . ,env)))
(: apply-env (→ Env Symbol Val))
(define apply-env
(λ (env y)
(match env
[‘() (error “unbound ” y)]
[`((,x . ,th) . ,env)
(if (eqv? y x) (th) (apply-env env y))])))
(: valof (→ Exp Env
Val))
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(apply-env env y)]
[`,n
#:when (number? n)
(begin (displayln ‘got-a-number)
n)]
[`(+ ,e₁ ,e₂)
(let ([r₁ (valof e₁ env)]
[r₂ (valof e₂ env)])
(cond
[(and (number? r₁) (number? r₂))
(+ r₁ r₂)]
[else (error “don’t be silly”)]))]
[`(λ (,x) ,body)
(λ ([th : (→ Val)]) (valof body (ext-env x th env)))]
[`(,rator ,rand)
(let ([clos (valof rator env)]
[th (λ () (valof rand env))])
(cond
[(or (number? clos) (boolean? clos) (void? clos)) (error “don’t be silly”)]
[else (clos th)]))])))
(valof ‘((λ (x) (+ x x)) 5)
init-env)
#;
(valof ‘((λ (x) 5) ((λ (x) (x x)) (λ (x) (x x))))
init-env)
#;
(valof ‘((λ (x) ((λ (y) (+ x y)) x)) 10)
init-env)
#lang typed/racket/no-check
#|This is a call-by-need interpreter.|#
(define-type Exp
(U Symbol
Number
(List ‘+ Exp Exp)
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
(define-type Env
(Listof (Pairof Symbol (Boxof (→ Val)))))
(define-type Closure
(→ (Boxof (→ Val)) Val))
(define-type Val
(U Number
Boolean
Closure))
(: init-env Env)
(define init-env ‘())
(: ext-env (→ Symbol (Boxof (→ Val)) Env Env))
(define ext-env
(λ (x b env)
`((,x . ,b) . ,env)))
(: apply-env (→ Env Symbol Val))
(define apply-env
(λ (env y)
(match env
[‘() (error “unbound ” y)]
[`((,x . ,b) . ,env)
(if (eqv? y x)
(let ([th (unbox b)])
(let ([v (th)])
(begin (set-box! b (λ () v))
v)))
(apply-env env y))])))
(: valof (→ Exp Env
Val))
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(apply-env env y)]
[`,n
#:when (number? n)
(begin (displayln ‘got-a-number)
n)]
[`(+ ,e₁ ,e₂)
(let ([r₁ (valof e₁ env)]
[r₂ (valof e₂ env)])
(cond
[(and (number? r₁) (number? r₂))
(+ r₁ r₂)]
[else (error “don’t be silly”)]))]
[`(λ (,x) ,body)
(λ ([b : (Boxof (→ Val))]) (valof body (ext-env x b env)))]
[`(,rator ,x)
#:when (symbol? x)
(cond
[(assv x env)
=>
(λ ([pr : (Pairof Symbol (Boxof (→ Val)))])
(let ([clos (valof rator env)]
[b (cdr pr)])
(cond
[(or (number? clos) (boolean? clos) (void? clos)) (error “don’t be silly”)]
[else (clos b)])))]
[else (error “unbound ” x)])]
[`(,rator ,rand)
(let ([clos (valof rator env)]
[b (box (λ () (valof rand env)))])
(cond
[(or (number? clos) (boolean? clos) (void? clos)) (error “don’t be silly”)]
[else (clos b)]))])))
(valof ‘((λ (x) (+ x x)) 5)
init-env)
(define-syntax kons
(syntax-rules ()
[(_ a d) (cons (box (λ () a)) (box (λ () d)))]))
(define-syntax kar
(syntax-rules ()
[(_ pr) (let ([b (car pr)])
(let ([th (unbox b)])
(let ([a (th)])
(begin (set-box! b (λ () a))
a))))]))
(define-syntax kdr
(syntax-rules ()
[(_ pr) (let ([b (cdr pr)])
(let ([th (unbox b)])
(let ([d (th)])
(begin (set-box! b (λ () d))
d))))]))
(define nats
(λ (n)
(kons n (nats (add1 n)))))
(define nat
(nats 0))
(define take
(λ ($ n)
(cond
[(null? $) ‘()]
[(zero? n) ‘()]
[(pair? $) (cons (kar $) (take (kdr $) (sub1 n)))]
[else (take ($) n)])))
#;
(take nat 1000)
#lang typed/racket
(define-type Exp
(U Symbol
Number
(List ‘+ Exp Exp)
(List ‘begin Exp Exp)
(List ‘set! Symbol Exp)
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
(define-type Env
(Listof (Pairof Symbol (Boxof Val))))
(define-type Closure
(→ (Boxof Val) Val))
(define-type Val
(U Number
Boolean
Closure
Void))
(: init-env Env)
(define init-env ‘())
(: ext-env (→ Symbol (Boxof Val) Env Env))
(define ext-env
(λ (x b env)
`((,x . ,b) . ,env)))
(: apply-env (→ Env Symbol Val))
(define apply-env
(λ (env y)
(match env
[‘() (error “unbound ” y)]
[`((,x . ,(box v)) . ,env)
(if (eqv? y x) v (apply-env env y))])))
(: valof (→ Exp Env
Val))
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(apply-env env y)]
[`,n
#:when (number? n)
n]
[`(begin ,e₁ ,e₂)
(begin (valof e₁ env)
(valof e₂ env))]
[`(set! ,x ,e)
(let ([v (valof e env)])
(cond
[(assv x env)
=>
(λ ([pr : (Pairof Symbol (Boxof Val))])
(set-box! (cdr pr) v))
]
[else (error “oops”)]))]
[`(+ ,e₁ ,e₂)
(let ([r₁ (valof e₁ env)]
[r₂ (valof e₂ env)])
(cond
[(and (number? r₁) (number? r₂))
(+ r₁ r₂)]
[else (error “don’t be silly”)]))]
[`(λ (,x) ,body)
(λ ([a : (Boxof Val)]) (valof body (ext-env x a env)))]
[`(,rator ,x)
#:when (symbol? x)
(cond
[(assv x env)
=>
(λ ([pr : (Pairof Symbol (Boxof Val))])
(let ([clos (valof rator env)]
[b (cdr pr)])
(cond
[(or (number? clos) (boolean? clos) (void? clos)) (error “don’t be silly”)]
[else (clos b)])))]
[else (error “unbound ” x)])]
[`(,rator ,rand)
(let ([clos (valof rator env)]
[a (valof rand env)])
(cond
[(or (number? clos) (boolean? clos) (void? clos)) (error “don’t be silly”)]
[else (clos (box a))]))])))
(valof ‘((λ (x) ((λ (y) (begin (set! y 5) y)) x)) 10)
init-env)
#lang typed/racket
(define-type Exp
(U Symbol
Number
(List ‘+ Exp Exp)
(List ‘begin Exp Exp)
(List ‘set! Symbol Exp)
(List ‘λ (List Symbol) Exp)
(List Exp Exp)))
(define-type Env
(Listof (Pairof Symbol (Boxof Val))))
(define-type Closure
(→ Val Val))
(define-type Val
(U Number
Boolean
Closure
Void))
(: init-env Env)
(define init-env ‘())
(: ext-env (→ Symbol Val Env Env))
(define ext-env
(λ (x v env)
`((,x . ,(box v)) . ,env)))
(: apply-env (→ Env Symbol Val))
(define apply-env
(λ (env y)
(match env
[‘() (error “unbound ” y)]
[`((,x . ,(box v)) . ,env)
(if (eqv? y x) v (apply-env env y))])))
(: valof (→ Exp Env
Val))
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(apply-env env y)]
[`,n
#:when (number? n)
n]
[`(begin ,e₁ ,e₂)
(begin (valof e₁ env)
(valof e₂ env))]
[`(set! ,x ,e)
(let ([v (valof e env)])
(cond
[(assv x env)
=>
(λ ([pr : (Pairof Symbol (Boxof Val))])
(set-box! (cdr pr) v))
]
[else (error “oops”)]))]
[`(+ ,e₁ ,e₂)
(let ([r₁ (valof e₁ env)]
[r₂ (valof e₂ env)])
(cond
[(and (number? r₁) (number? r₂))
(+ r₁ r₂)]
[else (error “don’t be silly”)]))]
[`(λ (,x) ,body)
(λ ([a : Val]) (valof body (ext-env x a env)))]
[`(,rator ,rand)
(let ([clos (valof rator env)]
[a (valof rand env)])
(cond
[(or (number? clos) (boolean? clos) (void? clos)) (error “don’t be silly”)]
[else (clos a)]))])))
(valof ‘((λ (x) 5) ((λ (x) (x x)) (λ (x) (x x))))
init-env)
#lang racket
#|miniKanren|#
(require “mk.rkt”)
(require “numbers.rkt”)
#;
(run 10 (numerator denominator value remainder)
(/o numerator denominator value remainder))
(define append
(λ (xs ys)
(cond
[(null? xs) ys]
[else (let ([a (car xs)]
[d (cdr xs)])
(let ([r (append d ys)])
(cons a r)))])))
(defrel (nullᵒ x)
(≡ ‘() x))
#|rewrite the append function to the appendᵒ relation|#
(defrel (appendᵒ xs ys o)
(condᵉ
[(nullᵒ xs) (== ys o)]
[(fresh (a d)
(== `(,a . ,d) xs)
(fresh (r)
(== `(,a . ,r) o)
(appendᵒ d ys r)))]))
(run 10 (xs ys o)
(appendᵒ xs ys o))
#lang racket
(provide defrel
conde conda condu
condᵉ
fresh
run run*
== ≡ =/= ≠ absento numbero symbolo numberᵒ symbolᵒ absentᵒ
succeed fail
prt)
#|microKanren, Ch 10|#
(define nothing
(vector))
(define (var sym scp)
(vector sym scp nothing))
(define var? vector?)
(define (var-has-val? x)
(not (equal? nothing (vector-ref x 2))))
(define (var-val x)
(vector-ref x 2))
(define (set-var-val! x v)
(vector-set! x 2 v))
(define (var-scp x)
(vector-ref x 1))
#;
(struct State
(s
scp
t
neqs
abs))
(struct Scope
())
(define State
(λ (s scp t neqs abs)
`(,s ,scp ,t ,neqs ,abs)))
(define init-S
(State (make-immutable-hasheqv) (Scope) (make-immutable-hasheqv) ‘()
(make-immutable-hasheqv)))
(define (walk v s)
(cond
[(var? v)
(cond
[(var-has-val? v)
(walk (var-val v) s)]
[(hash-ref s v #f)
=>
(λ (v) (walk v s))]
[else v])]
[else v]))
(define (ext-s x v s)
(cond
[(occurs? x v s) #f]
[else (hash-set s x v)]))
(define (occurs? x v s)
(let ([v (walk v s)])
(cond
[(var? v) (eqv? v x)]
[(pair? v) (or (occurs? x (car v) s)
(occurs? x (cdr v) s))]
[else #f])))
(define (unify u v s scp new-pairs)
(let ([u (walk u s)]
[v (walk v s)])
(cond
[(eqv? u v) (cons s new-pairs)]
[(var? u) (cond
[(eqv? (var-scp u) scp)
(if (occurs? u v s)
#f
(begin (set-var-val! u v)
(cons s `((,u . ,v) . ,new-pairs))))]
[else
(go-on ([s (ext-s u v s)])
(cons s `((,u . ,v) . ,new-pairs)))])]
[(var? v) (cond
[(eqv? (var-scp v) scp)
(if (occurs? v u s)
#f
(begin (set-var-val! v u)
(cons s `((,v . ,u) . ,new-pairs))))]
[else
(go-on ([s (ext-s v u s)])
(cons s `((,v . ,u) . ,new-pairs)))])]
[(and (pair? u) (pair? v))
(go-on ([`(,s . ,new-pairs) (unify (car u) (car v) s scp new-pairs)]
[`(,s . ,new-pairs) (unify (cdr u) (cdr v) s scp new-pairs)])
(cons s new-pairs))]
[else #f])))
(define (== u v)
(λS (S @ s scp t neqs abs)
(go-on ( [`(,s . ,new-pairs) (unify u v s scp ‘())]
[neqs (validate-neqs neqs s)]
[t (validate-types new-pairs t)]
[`(,neqs . ,abs) (validate-abs new-pairs neqs abs s)])
`(,(State s scp t neqs abs))
‘())))
(define (succeed S) `(,S))
(define (fail S) ‘())
(define ((disj₂ g₁ g₂) S)
($append (g₁ S) (g₂ S)))
(define ($append $₁ $₂)
(cond
[(null? $₁) $₂]
[(pair? $₁) (cons (car $₁) ($append (cdr $₁) $₂))]
[else (λ () ($append $₂ ($₁)))]))
(define ($take n $)
(cond
[(and n (zero? n)) ‘()]
[(null? $) ‘()]
[(pair? $) (cons (car $) ($take (and n (sub1 n)) (cdr $)))]
[else ($take n ($))]))
(define ((conj₂ g₁ g₂) S)
($append-map g₂ (g₁ S)))
(define ($append-map g $)
(cond
[(null? $) ‘()]
[(pair? $) ($append (g (car $)) ($append-map g (cdr $)))]
[else (λ () ($append-map g ($)))]))
(define call/fresh
(λ (name f)
(λS (S @ s scp t neqs abs)
((f (var name scp)) S))))
(define (reify-name n)
(string->symbol (string-append “_” (number->string n))))
(define (walk* v s)
(let ([v (walk v s)])
(cond
[(var? v) v]
[(pair? v) (cons (walk* (car v) s)
(walk* (cdr v) s))]
[else v])))
(define (reify-s v s)
(let ([v (walk v s)])
(cond
[(var? v) (let ([n (hash-count s)])
(let ([rn (reify-name n)])
(hash-set s v rn)))]
[(pair? v) (let ([s (reify-s (car v) s)])
(reify-s (cdr v) s))]
[else s])))
(define (reify v)
(λS (S @ s scp t neqs abs)
(let ([v (walk* v s)])
(let ([names (reify-s v (make-immutable-hasheqv))])
(walk* v names)))))
(define (run-goal n g)
($take n (g init-S)))
(define ((ifte g₁ g₂ g₃) S)
(let loop ([$ (g₁ S)])
(cond
[(null? $) (g₃ S)]
[(pair? $)
($append-map g₂ $)]
[else (λ () (loop ($)))])))
(define ((once g) S)
(let loop ([$ (g S)])
(cond
[(null? $) ‘()]
[(pair? $) (cons (car $) ‘())]
[else (λ () (loop ($)))])))
#|macros, connecting wires|#
(define-syntax disj
(syntax-rules ()
[(disj) fail]
[(disj g) g]
[(disj g₀ g …) (disj₂ g₀ (disj g …))]))
(define-syntax conj
(syntax-rules ()
[(conj) succeed]
[(conj g) g]
[(conj g₀ g …) (conj₂ g₀ (conj g …))]))
(define-syntax defrel
(syntax-rules ()
[(defrel (name x …) g …)
(define (name x …)
(λ (s)
(λ ()
((conj g …) s))))]))
(define-syntax run
(syntax-rules ()
[(run n (x₀ x …) g …)
(run n q (fresh (x₀ x …)
(== `(,x₀ ,x …) q)
g …))]
[(run n q g …)
(let ([q (var ‘q (Scope))])
(map (reify q) (run-goal n (conj g …))))]))
(define-syntax run*
(syntax-rules ()
[(run* q g …) (run #f q g …)]))
(define-syntax fresh
(syntax-rules ()
[(fresh () g …) (conj g …)]
[(fresh (x₀ x …) g …)
(call/fresh ‘x₀
(λ (x₀)
(fresh (x …) g …)))]))
(define-syntax conde
(syntax-rules ()
[(conde (g …) …) ((call/new-scope) (disj (conj g …) …))]))
(define-syntax condᵉ
(syntax-rules ()
[(condᵉ (g …) …) ((call/new-scope) (disj (conj g …) …))]))
(define-syntax conda
(syntax-rules ()
[(conda (g₀ g …)) (conj g₀ g …)]
[(conda (g₀ g …) ln …)
(ifte g₀ (conj g …) (conda ln …))]))
(define-syntax condu
(syntax-rules ()
[(condu (g₀ g …) …)
(conda ((once g₀) g …) …)]))
(define (call/new-scope)
(λ (g)
(λS (S @ s scp t neqs abs)
(g (State s (Scope) t neqs abs)))))
#|other constraints|#
(define ((prt c) S)
(let ([s (State-s S)])
(begin (displayln (walk* c s))
`(,S))))
(define (validate-neqs neqs s)
(cond
[(null? neqs) ‘()]
[else (go-on ([new-car (unify-all (car neqs) s ‘())])
(if (null? new-car)
#f
(go-on ([new-cdr (validate-neqs (cdr neqs) s)])
(cons new-car new-cdr)))
(validate-neqs (cdr neqs) s))]))
(define (unify-all ls s new-pairs)
(cond
[(null? ls) new-pairs]
[else (go-on ([`(,s . ,new-pairs)
(unify (car (car ls)) (cdr (car ls)) s (Scope) new-pairs)])
(unify-all (cdr ls) s new-pairs))]))
(define (validate-types ls types)
(cond
[(null? ls) types]
[else (go-on ([types (propogate-type (car ls) types)]
[types (validate-types (cdr ls) types)])
types)]))
(define (propogate-type pr types)
(let ([u (car pr)]
[v (cdr pr)])
(cond
[(var? v) (let ([u-type (hash-ref types u #f)]
[v-type (hash-ref types v #f)])
(cond
[(and u-type v-type) (and (eqv? u-type v-type) types)]
[u-type (hash-set types v u-type)]
[v-type (hash-set types u v-type)]
[else types]))]
[else (let ([u-type (hash-ref types u #f)])
(cond
[u-type (and (u-type v) types)]
[else types]))])))
(define (unicons x ls)
(if (memv x ls) ls (cons x ls)))
(define (not-appears u v neqs abs s)
(let ([u (walk u s)]
[v (walk v s)])
(cond
[(var? v) (let ([v-abs (hash-ref abs v #f)])
(cons (cons `((,v . ,u)) neqs)
(hash-set abs v (unicons u (or v-abs ‘())))))]
[(pair? v) (go-on ([`(,neqs . ,abs) (not-appears u (car v) neqs abs s)])
(not-appears u (cdr v) neqs abs s))]
[else (and (not (eqv? u v)) (cons neqs abs))])))
(define (validate-abs ls neqs abs s)
(cond
[(null? ls) (cons neqs abs)]
[else (let ([pr (car ls)])
(let ([u (car pr)]
[v (cdr pr)])
(let ([u-abs (hash-ref abs u #f)])
(if u-abs
(go-on ([`(,neqs . ,abs)
(propogate-abs u-abs v neqs abs s)])
(validate-abs (cdr ls) neqs abs s))
(validate-abs (cdr ls) neqs abs s)))))]))
(define (propogate-abs ls t neqs abs s)
(cond
[(null? ls) (cons neqs abs)]
[else (go-on ([`(,neqs . ,abs) (not-appears (car ls) t neqs abs s)])
(propogate-abs (cdr ls) t neqs abs s))]))
(define ≡ ==)
(define (=/= u v)
(λS (S @ s scp t neqs abs)
(go-on ([`(,s^ . ,new-pairs) (unify u v s (Scope) ‘())])
(if (null? new-pairs)
‘()
`(,(State s scp t (cons new-pairs neqs) abs)))
`(,S))))
(define ≠ =/=)
(define (booleano u)
(typeo boolean? u))
(define (numbero u)
(typeo number? u))
(define numberᵒ numbero)
(define (symbolo u)
(typeo symbol? u))
(define symbolᵒ symbolo)
(define (typeo pred u)
(λS (S @ s scp t neqs abs)
(let ([u (walk u s)])
(cond
[(var? u) (let ([u-type (hash-ref t u #f)])
(cond
[u-type (if (eqv? u-type pred) `(,S) ‘())]
[else `(,(State s scp (hash-set t u pred) neqs abs))]))]
[(pred u) `(,S)]
[else ‘()]))))
(define (absento u v)
(λS (S @ s scp t neqs abs)
(go-on ([`(,neqs . ,abs) (not-appears u v neqs abs s)])
`(,(State s scp t neqs abs))
‘())))
(define absentᵒ absento)
#|syntax sugars|#
(define-syntax go-on
(syntax-rules ()
[(_ () then) then]
[(_ () then alter) then]
[(_ ([p₀ e₀] [p e] …) then)
(cond
[e₀ => (λ (v) (match v
[p₀ (go-on ([p e] …) then)]))]
[else #f])]
[(_ ([p₀ e₀] [p e] …) then alter)
(cond
[e₀ => (λ (v) (match v
[p₀ (go-on ([p e] …) then alter)]))]
[else alter])]))
(define (State-s S)
(car S))
(define (State-scp S)
(car (cdr S)))
(define (State-t S)
(car (cdr (cdr S))))
(define (State-neqs S)
(car (cdr (cdr (cdr S)))))
(define (State-abs S)
(car (cdr (cdr (cdr (cdr S))))))
(define-syntax λS
(syntax-rules (@)
[(_ (S @ s scp t neqs abs) b)
(λ (S)
(let ([s (State-s S)]
[scp (State-scp S)]
[t (State-t S)]
[neqs (State-neqs S)]
[abs (State-abs S)])
b))]))
#lang racket
(require “mk.rkt”)
(provide (all-defined-out))
(defrel (appendo l s out)
(conde
[(== ‘() l) (== s out)]
[(fresh (a d res)
(== `(,a . ,d) l)
(== `(,a . ,res) out)
(appendo d s res))]))
(define build-num
(lambda (n)
(cond
((odd? n)
(cons 1
(build-num (quotient (- n 1) 2))))
((and (not (zero? n)) (even? n))
(cons 0
(build-num (quotient n 2))))
((zero? n) ‘()))))
(defrel (zeroo n)
(== ‘() n))
(defrel (poso n)
(fresh (a d)
(== `(,a . ,d) n)))
(defrel (>1o n)
(fresh (a ad dd)
(== `(,a ,ad . ,dd) n)))
(defrel (full-addero b x y r c)
(conde
((== 0 b) (== 0 x) (== 0 y) (== 0 r) (== 0 c))
((== 1 b) (== 0 x) (== 0 y) (== 1 r) (== 0 c))
((== 0 b) (== 1 x) (== 0 y) (== 1 r) (== 0 c))
((== 1 b) (== 1 x) (== 0 y) (== 0 r) (== 1 c))
((== 0 b) (== 0 x) (== 1 y) (== 1 r) (== 0 c))
((== 1 b) (== 0 x) (== 1 y) (== 0 r) (== 1 c))
((== 0 b) (== 1 x) (== 1 y) (== 0 r) (== 1 c))
((== 1 b) (== 1 x) (== 1 y) (== 1 r) (== 1 c))))
(defrel (addero d n m r)
(conde
((== 0 d) (== ‘() m) (== n r))
((== 0 d) (== ‘() n) (== m r)
(poso m))
((== 1 d) (== ‘() m)
(addero 0 n ‘(1) r))
((== 1 d) (== ‘() n) (poso m)
(addero 0 ‘(1) m r))
((== ‘(1) n) (== ‘(1) m)
(fresh (a c)
(== `(,a ,c) r)
(full-addero d 1 1 a c)))
((== ‘(1) n) (gen-addero d n m r))
((== ‘(1) m) (>1o n) (>1o r)
(addero d ‘(1) n r))
((>1o n) (gen-addero d n m r))))
(defrel (gen-addero d n m r)
(fresh (a b c e x y z)
(== `(,a . ,x) n)
(== `(,b . ,y) m) (poso y)
(== `(,c . ,z) r) (poso z)
(full-addero d a b c e)
(addero e x y z)))
(defrel (pluso n m k)
(addero 0 n m k))
(defrel (minuso n m k)
(pluso m k n))
(defrel (*o n m p)
(conde
((== ‘() n) (== ‘() p))
((poso n) (== ‘() m) (== ‘() p))
((== ‘(1) n) (poso m) (== m p))
((>1o n) (== ‘(1) m) (== n p))
((fresh (x z)
(== `(0 . ,x) n) (poso x)
(== `(0 . ,z) p) (poso z)
(>1o m)
(*o x m z)))
((fresh (x y)
(== `(1 . ,x) n) (poso x)
(== `(0 . ,y) m) (poso y)
(*o m n p)))
((fresh (x y)
(== `(1 . ,x) n) (poso x)
(== `(1 . ,y) m) (poso y)
(odd-*o x n m p)))))
(defrel (odd-*o x n m p)
(fresh (q)
(bound-*o q p n m)
(*o x m q)
(pluso `(0 . ,q) m p)))
(defrel (bound-*o q p n m)
(conde
((== ‘() q) (poso p))
((fresh (a0 a1 a2 a3 x y z)
(== `(,a0 . ,x) q)
(== `(,a1 . ,y) p)
(conde
((== ‘() n)
(== `(,a2 . ,z) m)
(bound-*o x y z ‘()))
((== `(,a3 . ,z) n)
(bound-*o x y z m)))))))
(defrel (=lo n m)
(conde
((== ‘() n) (== ‘() m))
((== ‘(1) n) (== ‘(1) m))
((fresh (a x b y)
(== `(,a . ,x) n) (poso x)
(== `(,b . ,y) m) (poso y)
(=lo x y)))))
(defrel (
((fresh (a x b y)
(== `(,a . ,x) n) (poso x)
(== `(,b . ,y) m) (poso y)
(
((== ‘(1) b) (poso q) (pluso r ‘(1) n))
((== ‘() b) (poso q) (== r n))
((== ‘(0 1) b)
(fresh (a ad dd)
(poso dd)
(== `(,a ,ad . ,dd) n)
(exp2 n ‘() q)
(fresh (s)
(splito n dd r s))))
((fresh (a ad add ddd)
(conde
((== ‘(1 1) b))
((== `(,a ,ad ,add . ,ddd) b))))
(
(fresh (s)
(splito n b s ‘(1))))
((fresh (q1 b2)
(== `(0 . ,q1) q)
(poso q1)
(
(fresh (q1 nq1)
(pluso q1 ‘(1) q)
(repeated-mul n q1 nq1)
(*o nq1 n nq)))))
(defrel (expo b q n)
(logo n b q ‘()))
#lang typed/racket
(struct var
([name : Symbol])
#:transparent)
(define-type term
(U var
Symbol
Null
(Pairof term term)))
(define-type Substitution
(Listof (Pairof var term)))
(: walk (→ term Substitution
term))
(define walk
(λ (v s)
(let ([a (and (var? v) (assv v s))])
(cond
[(pair? a) (walk (cdr a) s)]
[else v]))))
#|an example of substitution|#
#;
(let ([x (var ‘x)]
[y (var ‘y)]
[z (var ‘z)])
(walk x `((,x . ,z) (,y . ,x) (,z . (,x ,x ,x)))))
(: ext-s (→ var term Substitution
(U Substitution False)))
(define ext-s
(λ (x v s)
(cond
[(occurs? x v s) #f]
[else (cons `(,x . ,v) s)])))
(: occurs? (→ var term Substitution
Boolean))
(define occurs?
(λ (x v s)
(let ([v (walk v s)])
(cond
[(var? v) (eqv? v x)]
[(pair? v)
(or (occurs? x (car v) s)
(occurs? x (cdr v) s))]
[else #f]))))
#|this ext-s fails (returns #f) because it violates occurrence check|#
#;
(let ([x (var ‘x)]
[y (var ‘y)])
(let ([s `((,y . (,x)))])
(ext-s x `(a ,y) s)))
(: unify (→ term term Substitution
(U Substitution False)))
(define unify
(λ (u v s)
(let ([u (walk u s)]
[v (walk v s)])
(cond
[(eqv? u v) s]
[(var? u) (ext-s u v s)]
[(var? v) (ext-s v u s)]
[(and (pair? u) (pair? v))
(let ([s (unify (car u) (car v) s)])
(and s (unify (cdr u) (cdr v) s)))]
[else #f]))))
(define-type (Stream A)
(U Null
(Pairof A (Stream A))
(→ (Stream A))))
(define-type Goal
(→ Substitution (Stream Substitution)))
(: ≡ (→ term term
Goal))
(define ≡
(λ (u v)
(λ (s)
(let ([s (unify u v s)])
(if s `(,s) ‘())))))
(: disj₂ (→ Goal Goal
Goal))
(define (disj₂ g₁ g₂)
(λ (s)
(append-inf (g₁ s) (g₂ s))))
(: append-inf (All (A) (→ (Stream A) (Stream A)
(Stream A))))
(define append-inf
(λ ($₁ $₂)
(cond
[(null? $₁) $₁]
[(pair? $₁)
(cons (car $₁) (append-inf (cdr $₁) $₂))]
[else
(λ () (append-inf $₂ ($₁)))])))
(: conj₂ (→ Goal Goal
Goal))
(define conj₂
(λ (g₁ g₂)
(λ (s)
(append-map-inf g₂ (g₁ s)))))
(: append-map-inf (All (A) (→ (→ A (Stream A)) (Stream A)
(Stream A))))
(define append-map-inf
(λ (g $)
(cond
[(null? $) ‘()]
[(pair? $) (append-inf (g (car $))
(append-map-inf g (cdr $)))]
[else
(λ () (append-map-inf g ($)))])))
(: take-inf (All (A) (→ (U Number False) (Stream A)
(Listof A))))
(define take-inf
(λ (n $)
(cond
[(and n (zero? n)) ‘()]
[(null? $) ‘()]
[(pair? $)
(cons (car $)
(take-inf (and n (sub1 n))
(cdr $)))]
[else (take-inf n ($))])))
(: succeed Goal)
(define succeed
(λ (s)
`(,s)))
(: fail Goal)
(define fail
(λ (s)
‘()))
(define-syntax disj
(syntax-rules ()
[(disj) fail]
[(disj g) g]
[(disj g₀ g …) (disj₂ g₀ (disj g …))]))
(define-syntax conj
(syntax-rules ()
[(conj) succeed]
[(conj g) g]
[(conj g₀ g …) (conj₂ g₀ (conj g …))]))
(define-syntax conde
(syntax-rules ()
[(conde (g …) …)
(disj (conj g …) …)]))
((let ([x (var ‘x)]
[y (var ‘y)])
(≡ `(,x ,y) `(cat cat)))
‘())
#lang racket
(require racket/trace)
#|Don’t mind this.|#
(define sub2 (compose sub1 sub1))
(define one? (compose zero? sub1))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k fib-of-sub1)
`(sub2 ,k ,fib-of-sub1)))
(define make-k-init
(λ (jumpout)
`(init ,jumpout)))
(define make-k-fact
(λ (n k)
`(fact ,n ,k)))
(define fib-cps
(λ (n k)
(λ ()
(cond
[(zero? n) (apply-k k 1)]
[(one? n) (apply-k k 1)]
[else (fib-cps (sub1 n)
(make-k-sub1 n k))]))))
(define fact-cps
(λ (n k)
(λ ()
(cond
[(zero? n) (apply-k k 1)]
[else (fact-cps (sub1 n)
(make-k-fact n k))]))))
(define apply-k
(λ (k v)
(λ ()
(match k
[`(sub1 ,n ,k)
(fib-cps (sub2 n)
(make-k-sub2 k v))]
[`(sub2 ,k ,fib-of-sub1)
(apply-k k (+ fib-of-sub1 v))]
[`(fact ,n ,k) (apply-k k (* n v))]
[`(init ,jumpout) (jumpout v)]))))
(define trampoline
(λ (th)
(trampoline (th))))
(define dt
(λ (th₁ th₂)
(dt th₂ (th₁))))
(define lot
(λ (l)
(let ([a (car l)]
[d (cdr l)])
(lot (append d (list (a)))))))
(let/cc jumpout
(lot
(list
(fact-cps 5 (make-k-init jumpout))
(fib-cps 5 (make-k-init jumpout))
(fact-cps 3 (make-k-init jumpout)))))
#lang racket
(require racket/trace)
#|Don’t mind this.|#
(define sub2 (compose sub1 sub1))
(define one? (compose zero? sub1))
#|cpsed fib|#
(define fib-cps
(λ (n k)
(cond
[(zero? n) (k 1)]
[(one? n) (k 1)]
[else (fib-cps (sub1 n)
(λ (fib-of-sub1)
(fib-cps (sub2 n)
(λ (fib-of-sub2)
(k (+ fib-of-sub1 fib-of-sub2))))))])))
(trace fib-cps)
(fib-cps 5 (λ (v) v))
#lang racket
(require racket/trace)
#|Don’t mind this.|#
(define sub2 (compose sub1 sub1))
(define one? (compose zero? sub1))
#|fib-cpsed and ri|#
(define fib-cps
(λ (n k)
(cond
[(zero? n) (apply-k k 1)]
[(one? n) (apply-k k 1)]
[else (fib-cps (sub1 n)
(make-k-sub1 n k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k fib-of-sub1)
`(sub2 ,k ,fib-of-sub1)))
(define make-k-init
(λ ()
`(init)))
(define apply-k
(λ (k v)
(match k
[`(sub1 ,n ,k)
(fib-cps (sub2 n)
(make-k-sub2 k v))]
[`(sub2 ,k ,fib-of-sub1)
(apply-k k (+ fib-of-sub1 v))]
[`(init) v])))
#;
(trace fib-cps)
(fib-cps 5 (make-k-init))
#lang racket
(provide defrel
conde conda condu
condᵉ
fresh
run run*
== ≡ =/= ≠ absento numbero symbolo numberᵒ symbolᵒ absentᵒ
succeed fail
prt)
#|microKanren, Ch 10|#
(define nothing
(vector))
(define (var sym scp)
(vector sym scp nothing))
(define var? vector?)
(define (var-has-val? x)
(not (equal? nothing (vector-ref x 2))))
(define (var-val x)
(vector-ref x 2))
(define (set-var-val! x v)
(vector-set! x 2 v))
(define (var-scp x)
(vector-ref x 1))
#;
(struct State
(s
scp
t
neqs
abs))
(struct Scope
())
(define State
(λ (s scp t neqs abs)
`(,s ,scp ,t ,neqs ,abs)))
(define init-S
(State (make-immutable-hasheqv) (Scope) (make-immutable-hasheqv) ‘()
(make-immutable-hasheqv)))
(define (walk v s)
(cond
[(var? v)
(cond
[(var-has-val? v)
(walk (var-val v) s)]
[(hash-ref s v #f)
=>
(λ (v) (walk v s))]
[else v])]
[else v]))
(define (ext-s x v s)
(cond
[(occurs? x v s) #f]
[else (hash-set s x v)]))
(define (occurs? x v s)
(let ([v (walk v s)])
(cond
[(var? v) (eqv? v x)]
[(pair? v) (or (occurs? x (car v) s)
(occurs? x (cdr v) s))]
[else #f])))
(define (unify u v s scp new-pairs)
(let ([u (walk u s)]
[v (walk v s)])
(cond
[(eqv? u v) (cons s new-pairs)]
[(var? u) (cond
[(eqv? (var-scp u) scp)
(if (occurs? u v s)
#f
(begin (set-var-val! u v)
(cons s `((,u . ,v) . ,new-pairs))))]
[else
(go-on ([s (ext-s u v s)])
(cons s `((,u . ,v) . ,new-pairs)))])]
[(var? v) (cond
[(eqv? (var-scp v) scp)
(if (occurs? v u s)
#f
(begin (set-var-val! v u)
(cons s `((,v . ,u) . ,new-pairs))))]
[else
(go-on ([s (ext-s v u s)])
(cons s `((,v . ,u) . ,new-pairs)))])]
[(and (pair? u) (pair? v))
(go-on ([`(,s . ,new-pairs) (unify (car u) (car v) s scp new-pairs)]
[`(,s . ,new-pairs) (unify (cdr u) (cdr v) s scp new-pairs)])
(cons s new-pairs))]
[else #f])))
(define (== u v)
(λS (S @ s scp t neqs abs)
(go-on ( [`(,s . ,new-pairs) (unify u v s scp ‘())]
[neqs (validate-neqs neqs s)]
[t (validate-types new-pairs t)]
[`(,neqs . ,abs) (validate-abs new-pairs neqs abs s)])
`(,(State s scp t neqs abs))
‘())))
(define (succeed S) `(,S))
(define (fail S) ‘())
(define ((disj₂ g₁ g₂) S)
($append (g₁ S) (g₂ S)))
(define ($append $₁ $₂)
(cond
[(null? $₁) $₂]
[(pair? $₁) (cons (car $₁) ($append (cdr $₁) $₂))]
[else (λ () ($append $₂ ($₁)))]))
(define ($take n $)
(cond
[(and n (zero? n)) ‘()]
[(null? $) ‘()]
[(pair? $) (cons (car $) ($take (and n (sub1 n)) (cdr $)))]
[else ($take n ($))]))
(define ((conj₂ g₁ g₂) S)
($append-map g₂ (g₁ S)))
(define ($append-map g $)
(cond
[(null? $) ‘()]
[(pair? $) ($append (g (car $)) ($append-map g (cdr $)))]
[else (λ () ($append-map g ($)))]))
(define call/fresh
(λ (name f)
(λS (S @ s scp t neqs abs)
((f (var name scp)) S))))
(define (reify-name n)
(string->symbol (string-append “_” (number->string n))))
(define (walk* v s)
(let ([v (walk v s)])
(cond
[(var? v) v]
[(pair? v) (cons (walk* (car v) s)
(walk* (cdr v) s))]
[else v])))
(define (reify-s v s)
(let ([v (walk v s)])
(cond
[(var? v) (let ([n (hash-count s)])
(let ([rn (reify-name n)])
(hash-set s v rn)))]
[(pair? v) (let ([s (reify-s (car v) s)])
(reify-s (cdr v) s))]
[else s])))
(define (reify v)
(λS (S @ s scp t neqs abs)
(let ([v (walk* v s)])
(let ([names (reify-s v (make-immutable-hasheqv))])
(walk* v names)))))
(define (run-goal n g)
($take n (g init-S)))
(define ((ifte g₁ g₂ g₃) S)
(let loop ([$ (g₁ S)])
(cond
[(null? $) (g₃ S)]
[(pair? $)
($append-map g₂ $)]
[else (λ () (loop ($)))])))
(define ((once g) S)
(let loop ([$ (g S)])
(cond
[(null? $) ‘()]
[(pair? $) (cons (car $) ‘())]
[else (λ () (loop ($)))])))
#|macros, connecting wires|#
(define-syntax disj
(syntax-rules ()
[(disj) fail]
[(disj g) g]
[(disj g₀ g …) (disj₂ g₀ (disj g …))]))
(define-syntax conj
(syntax-rules ()
[(conj) succeed]
[(conj g) g]
[(conj g₀ g …) (conj₂ g₀ (conj g …))]))
(define-syntax defrel
(syntax-rules ()
[(defrel (name x …) g …)
(define (name x …)
(λ (s)
(λ ()
((conj g …) s))))]))
(define-syntax run
(syntax-rules ()
[(run n (x₀ x …) g …)
(run n q (fresh (x₀ x …)
(== `(,x₀ ,x …) q)
g …))]
[(run n q g …)
(let ([q (var ‘q (Scope))])
(map (reify q) (run-goal n (conj g …))))]))
(define-syntax run*
(syntax-rules ()
[(run* q g …) (run #f q g …)]))
(define-syntax fresh
(syntax-rules ()
[(fresh () g …) (conj g …)]
[(fresh (x₀ x …) g …)
(call/fresh ‘x₀
(λ (x₀)
(fresh (x …) g …)))]))
(define-syntax conde
(syntax-rules ()
[(conde (g …) …) ((call/new-scope) (disj (conj g …) …))]))
(define-syntax condᵉ
(syntax-rules ()
[(condᵉ (g …) …) ((call/new-scope) (disj (conj g …) …))]))
(define-syntax conda
(syntax-rules ()
[(conda (g₀ g …)) (conj g₀ g …)]
[(conda (g₀ g …) ln …)
(ifte g₀ (conj g …) (conda ln …))]))
(define-syntax condu
(syntax-rules ()
[(condu (g₀ g …) …)
(conda ((once g₀) g …) …)]))
(define (call/new-scope)
(λ (g)
(λS (S @ s scp t neqs abs)
(g (State s (Scope) t neqs abs)))))
#|other constraints|#
(define ((prt c) S)
(let ([s (State-s S)])
(begin (displayln (walk* c s))
`(,S))))
(define (validate-neqs neqs s)
(cond
[(null? neqs) ‘()]
[else (go-on ([new-car (unify-all (car neqs) s ‘())])
(if (null? new-car)
#f
(go-on ([new-cdr (validate-neqs (cdr neqs) s)])
(cons new-car new-cdr)))
(validate-neqs (cdr neqs) s))]))
(define (unify-all ls s new-pairs)
(cond
[(null? ls) new-pairs]
[else (go-on ([`(,s . ,new-pairs)
(unify (car (car ls)) (cdr (car ls)) s (Scope) new-pairs)])
(unify-all (cdr ls) s new-pairs))]))
(define (validate-types ls types)
(cond
[(null? ls) types]
[else (go-on ([types (propogate-type (car ls) types)]
[types (validate-types (cdr ls) types)])
types)]))
(define (propogate-type pr types)
(let ([u (car pr)]
[v (cdr pr)])
(cond
[(var? v) (let ([u-type (hash-ref types u #f)]
[v-type (hash-ref types v #f)])
(cond
[(and u-type v-type) (and (eqv? u-type v-type) types)]
[u-type (hash-set types v u-type)]
[v-type (hash-set types u v-type)]
[else types]))]
[else (let ([u-type (hash-ref types u #f)])
(cond
[u-type (and (u-type v) types)]
[else types]))])))
(define (unicons x ls)
(if (memv x ls) ls (cons x ls)))
(define (not-appears u v neqs abs s)
(let ([u (walk u s)]
[v (walk v s)])
(cond
[(var? v) (let ([v-abs (hash-ref abs v #f)])
(cons (cons `((,v . ,u)) neqs)
(hash-set abs v (unicons u (or v-abs ‘())))))]
[(pair? v) (go-on ([`(,neqs . ,abs) (not-appears u (car v) neqs abs s)])
(not-appears u (cdr v) neqs abs s))]
[else (and (not (eqv? u v)) (cons neqs abs))])))
(define (validate-abs ls neqs abs s)
(cond
[(null? ls) (cons neqs abs)]
[else (let ([pr (car ls)])
(let ([u (car pr)]
[v (cdr pr)])
(let ([u-abs (hash-ref abs u #f)])
(if u-abs
(go-on ([`(,neqs . ,abs)
(propogate-abs u-abs v neqs abs s)])
(validate-abs (cdr ls) neqs abs s))
(validate-abs (cdr ls) neqs abs s)))))]))
(define (propogate-abs ls t neqs abs s)
(cond
[(null? ls) (cons neqs abs)]
[else (go-on ([`(,neqs . ,abs) (not-appears (car ls) t neqs abs s)])
(propogate-abs (cdr ls) t neqs abs s))]))
(define ≡ ==)
(define (=/= u v)
(λS (S @ s scp t neqs abs)
(go-on ([`(,s^ . ,new-pairs) (unify u v s (Scope) ‘())])
(if (null? new-pairs)
‘()
`(,(State s scp t (cons new-pairs neqs) abs)))
`(,S))))
(define ≠ =/=)
(define (booleano u)
(typeo boolean? u))
(define (numbero u)
(typeo number? u))
(define numberᵒ numbero)
(define (symbolo u)
(typeo symbol? u))
(define symbolᵒ symbolo)
(define (typeo pred u)
(λS (S @ s scp t neqs abs)
(let ([u (walk u s)])
(cond
[(var? u) (let ([u-type (hash-ref t u #f)])
(cond
[u-type (if (eqv? u-type pred) `(,S) ‘())]
[else `(,(State s scp (hash-set t u pred) neqs abs))]))]
[(pred u) `(,S)]
[else ‘()]))))
(define (absento u v)
(λS (S @ s scp t neqs abs)
(go-on ([`(,neqs . ,abs) (not-appears u v neqs abs s)])
`(,(State s scp t neqs abs))
‘())))
(define absentᵒ absento)
#|syntax sugars|#
(define-syntax go-on
(syntax-rules ()
[(_ () then) then]
[(_ () then alter) then]
[(_ ([p₀ e₀] [p e] …) then)
(cond
[e₀ => (λ (v) (match v
[p₀ (go-on ([p e] …) then)]))]
[else #f])]
[(_ ([p₀ e₀] [p e] …) then alter)
(cond
[e₀ => (λ (v) (match v
[p₀ (go-on ([p e] …) then alter)]))]
[else alter])]))
(define (State-s S)
(car S))
(define (State-scp S)
(car (cdr S)))
(define (State-t S)
(car (cdr (cdr S))))
(define (State-neqs S)
(car (cdr (cdr (cdr S)))))
(define (State-abs S)
(car (cdr (cdr (cdr (cdr S))))))
(define-syntax λS
(syntax-rules (@)
[(_ (S @ s scp t neqs abs) b)
(λ (S)
(let ([s (State-s S)]
[scp (State-scp S)]
[t (State-t S)]
[neqs (State-neqs S)]
[abs (State-abs S)])
b))]))
#lang racket
(require “mk.rkt”)
(define Γ₀
‘((x . ℕ) (y . Bool) (z . ℕ)))
(defrel (lookupᵒ Γ x t)
(fresh (x^ t^ Γ^)
(== `((,x^ . ,t^) . ,Γ^) Γ)
(conde
[(== x^ x) (== t^ t)]
[(=/= x^ x)
(lookupᵒ Γ^ x t)])))
#;
(run 1 τ
(lookupᵒ Γ₀ ‘x τ))
(defrel (⊢ Γ e τ)
(conde
[(numbero e)
(== τ ‘ℕ)]
[(conde
[(== e #t)]
[(== e #f)])
(== τ ‘𝔹)]
[(fresh (e₁ e₂)
(== `(* ,e₁ ,e₂) e)
(⊢ Γ e₁ ‘ℕ)
(⊢ Γ e₂ ‘ℕ)
(== τ ‘ℕ))]
[(fresh (e₁ e₂ e₃)
(== `(if ,e₁ ,e₂ ,e₃) e)
(⊢ Γ e₁ ‘𝔹)
(⊢ Γ e₂ τ)
(⊢ Γ e₃ τ))]
[(fresh (e₁)
(== `(sub1 ,e₁) e)
(⊢ Γ e₁ ‘ℕ)
(== τ ‘ℕ))]
[(fresh (e₁)
(== `(zero? ,e₁) e)
(⊢ Γ e₁ ‘ℕ)
(== τ ‘𝔹))]
[(symbolo e)
(lookupᵒ Γ e τ)]
[(fresh (x body)
(== `(λ (,x) ,body) e)
(fresh (τin τout)
(== `(→ ,τin ,τout) τ)
(⊢ `((,x . ,τin) . ,Γ) body τout)))]
[(fresh (rator rand)
(== `(,rator ,rand) e)
(fresh (τin)
(⊢ Γ rator `(→ ,τin ,τ))
(⊢ Γ rand τin)))]
[(fresh (x body)
(== `(fix (λ (,x) ,body)) e)
(⊢ `((,x . ,τ) . ,Γ) body τ))]))
#|self application does NOT have a type|#
#;
(run 1 τ
(⊢ ‘() ‘(fix (λ (fact)
(λ (n)
(if (zero? n)
1
(* n (fact (sub1 n)))))))
τ))
#;
(((λ (x) (x x))
(λ (fact)
(λ (n)
(if (zero? n)
1
(* n ((fact fact) (sub1 n)))))))
5)
#|Type checking does not require running the program (at least here).|#
(run 1 τ
(⊢ ‘() ‘((fix (λ (fact)
(λ (n)
(* n (fact (sub1 n))))))
5)
τ))
#|
Try to add Pair type and List type to this small language.
And make up the inference rules for those operators (kons, kar, kdr, etc).
|#
#|
Further reading: Hindley-Milner type system.
|#
#|
Change define thunks to define labels.
|#
(define-registers fib-cps-n apply-k-v cc)
(define-program-counter pc)
(define-union continuation
(init jumpout)
(sub1 n k)
(sub2 k v₁))
(define-label fib-cps
(cond
[(zero? fib-cps-n)
(begin [set! cc cc]
[set! apply-k-v 1]
(set! pc apply-k))]
[(zero? (sub1 fib-cps-n))
(begin [set! cc cc]
[set! apply-k-v 1]
(set! pc apply-k))]
[else (begin [set! cc (continuation_sub1 fib-cps-n cc)]
[set! fib-cps-n (sub1 fib-cps-n)]
(set! pc fib-cps))]))
(define-label apply-k
(union-case cc continuation
[(init jumpout) (dismount-trampoline jumpout)]
[(sub2 k v₁)
(begin [set! cc k]
[set! apply-k-v (+ v₁ apply-k-v)]
(set! pc apply-k))]
[(sub1 n k)
(begin [set! cc (continuation_sub2 k apply-k-v)]
[set! fib-cps-n (sub1 (sub1 n))]
(set! pc fib-cps))]))
(define-label main
(begin
[set! fib-cps-n 5]
(set! pc fib-cps)
#|mount trampoline after setting everything else|#
(mount-trampoline continuation_init cc pc)
(printf “~s\n” apply-k-v)))
#lang racket
(require “parenthec.rkt”)
#|
1, introduce the union for continuations
2, change every place where you build a continuation, now use union
3, change the match that matches a continuation, now it uses union-case
|#
(define-union continuation
(init)
(sub1 n k)
(sub2 k v₁))
#;
(define-types Continuation
(U (List ‘init)
(List ‘sub1 Number Continuation)
(List ‘sub2 Continuation Value)))
#|
(define-union expression
)
(define-union environment
)
(define-union closure
)
|#
(define fib-cps
(λ (n k)
(cond
[(zero? n) (apply-k k 1)]
[(zero? (sub1 n)) (apply-k k 1)]
[else (fib-cps (sub1 n) (continuation_sub1 n k))])))
(define make-k-sub1
(λ (n k)
`(sub1 ,n ,k)))
(define make-k-sub2
(λ (k v₁)
`(sub2 ,k ,v₁)))
(define make-k-init
(λ ()
‘(init)))
(define apply-k
(λ (k v)
#|You need to specify the type of the union in union-case.|#
(union-case k continuation
[(init) v]
[(sub2 k v₁) (apply-k k (+ v₁ v))]
[(sub1 n k) (fib-cps (sub1 (sub1 n)) (continuation_sub2 k v))])))
(fib-cps 5 (continuation_init))
#lang racket
(require “parenthec.rkt”)
#|
Use let* to make all serious functions in A-normal form.
|#
(define-union continuation
(init)
(sub1 n k)
(sub2 k v₁))
(define fib-cps
(λ (n k)
(cond
[(zero? n)
(let* ([k k]
[v 1])
(apply-k k v))]
[(zero? (sub1 n))
(let* ([k k]
[v 1])
(apply-k k v))]
[else (let* ([k (continuation_sub1 n k)]
[n (sub1 n)])
(fib-cps n k))])))
(define apply-k
(λ (k v)
#|You need to specify the type of the union in union-case.|#
(union-case k continuation
[(init) v]
[(sub2 k v₁)
(let* ([k k]
[v (+ v₁ v)])
(apply-k k v))]
[(sub1 n k)
(let* ([k (continuation_sub2 k v)]
[n (sub1 (sub1 n))])
(fib-cps n k))])))
(let* ([k (continuation_init)]
[n 5])
(fib-cps n k))
#lang racket
(require “parenthec.rkt”)
#|
Registerize all serious functions.
|#
(define-registers fib-cps-n apply-k-v cc)
(define-union continuation
(init)
(sub1 n k)
(sub2 k v₁))
(define fib-cps
(λ (fib-cps-n cc)
(cond
[(zero? fib-cps-n)
(let* ([cc cc]
[apply-k-v 1])
(apply-k cc apply-k-v))]
[(zero? (sub1 fib-cps-n))
(let* ([cc cc]
[apply-k-v 1])
(apply-k cc apply-k-v))]
[else (let* ([cc (continuation_sub1 fib-cps-n cc)]
[fib-cps-n (sub1 fib-cps-n)])
(fib-cps fib-cps-n cc))])))
(define apply-k
(λ (k v)
#|You need to specify the type of the union in union-case.|#
(union-case k continuation
[(init) v]
[(sub2 k v₁)
(let* ([k k]
[v (+ v₁ v)])
(apply-k k v))]
[(sub1 n k)
(let* ([k (continuation_sub2 k v)]
[n (sub1 (sub1 n))])
(fib-cps n k))])))
(let* ([k (continuation_init)]
[n 5])
(fib-cps n k))
#lang racket
(require “parenthec.rkt”)
#|
Before registerizing your code, α-rename the local variables in the serious functions.
|#
(define-registers fib-cps-n apply-k-v cc)
(define-union continuation
(init)
(sub1 n k)
(sub2 k v₁))
(define fib-cps
(λ (fib-cps-n cc)
(cond
[(zero? fib-cps-n)
(let* ([cc cc]
[apply-k-v 1])
(apply-k cc apply-k-v))]
[(zero? (sub1 fib-cps-n))
(let* ([cc cc]
[apply-k-v 1])
(apply-k cc apply-k-v))]
[else (let* ([cc (continuation_sub1 fib-cps-n cc)]
[fib-cps-n (sub1 fib-cps-n)])
(fib-cps fib-cps-n cc))])))
(define apply-k
(λ (cc apply-k-v)
#|You need to specify the type of the union in union-case.|#
(union-case cc continuation
[(init) apply-k-v]
[(sub2 k v₁)
(let* ([cc k]
[apply-k-v (+ v₁ apply-k-v)])
(apply-k cc apply-k-v))]
[(sub1 n k)
(let* ([cc (continuation_sub2 k apply-k-v)]
[fib-cps-n (sub1 (sub1 n))])
(fib-cps fib-cps-n cc))])))
(let* ([cc (continuation_init)]
[fib-cps-n 5])
(fib-cps fib-cps-n cc))
#lang racket
(require “parenthec.rkt”)
#|
Registerize the renamed programs.
|#
(define-registers fib-cps-n apply-k-v cc)
(define-union continuation
(init)
(sub1 n k)
(sub2 k v₁))
(define fib-cps
(λ () ;fib-cps-n cc
(cond
[(zero? fib-cps-n)
(begin [set! cc cc]
[set! apply-k-v 1]
(apply-k))]
[(zero? (sub1 fib-cps-n))
(begin [set! cc cc]
[set! apply-k-v 1]
(apply-k))]
[else (begin [set! cc (continuation_sub1 fib-cps-n cc)]
[set! fib-cps-n (sub1 fib-cps-n)]
(fib-cps))])))
(define apply-k
(λ ()
(union-case cc continuation
[(init) apply-k-v]
[(sub2 k v₁)
(begin [set! cc k]
[set! apply-k-v (+ v₁ apply-k-v)]
(apply-k))]
[(sub1 n k)
(begin [set! cc (continuation_sub2 k apply-k-v)]
[set! fib-cps-n (sub1 (sub1 n))]
(fib-cps))])))
(begin [set! cc (continuation_init)]
[set! fib-cps-n 5]
(fib-cps))
#lang racket
(require “parenthec.rkt”)
#|
Change define thunks to define labels.
|#
(define-registers fib-cps-n apply-k-v cc)
(define-union continuation
(init)
(sub1 n k)
(sub2 k v₁))
(define-label fib-cps
(cond
[(zero? fib-cps-n)
(begin [set! cc cc]
[set! apply-k-v 1]
(apply-k))]
[(zero? (sub1 fib-cps-n))
(begin [set! cc cc]
[set! apply-k-v 1]
(apply-k))]
[else (begin [set! cc (continuation_sub1 fib-cps-n cc)]
[set! fib-cps-n (sub1 fib-cps-n)]
(fib-cps))]))
(define-label apply-k
(union-case cc continuation
[(init) apply-k-v]
[(sub2 k v₁)
(begin [set! cc k]
[set! apply-k-v (+ v₁ apply-k-v)]
(apply-k))]
[(sub1 n k)
(begin [set! cc (continuation_sub2 k apply-k-v)]
[set! fib-cps-n (sub1 (sub1 n))]
(fib-cps))]))
(begin [set! cc (continuation_init)]
[set! fib-cps-n 5]
(fib-cps))
#lang racket
(module help racket
(provide pc-err
**pc-func-name-table**
pc-add-func-name!
pc-func-name-exists?
pc-error-check:define-label
**pc-union-type-table**
pc-add-union-type!
pc-union-type-exists?
pc-check-set-of-vars
pc-error-check:define-union
pc-error-check:general-union-case
pc-valid-variant?)
(define pc-valid-variant?
(lambda (union-type variant)
(and
(list? variant)
(>= (length variant) 2)
(let ([ut (car variant)]
[st (cadr variant)]
[arg-count (length (cddr variant))])
(and
(eqv? union-type ut)
(printf “utt ~a” **pc-union-type-table**)
(let ([type (assoc union-type **pc-union-type-table**)])
(and type
(member `(,st . ,arg-count) (cadr type)))))))))
(define lookup-union
(lambda (name)
(let loop ([reg **pc-union-type-table**])
(cond
[(null? reg) (error ‘lookup-union
“union type `~a’ not defined ~n” name)]
[(eq? name (caar reg)) (car reg)]
[else (loop (cdr reg))]))))
(define check-union-case
(lambda (expr name type case)
(cond
[(and (null? type) (not (null? case)))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nsuperfluous cases for union type `~a’: ~a”
(get-output-string s) name case))]
[(and (null? case) (not (null? type)))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nunmatched cases for union type `~a’: ~a”
(get-output-string s) name type))]
[(and (null? type) (null? case)) #t]
[(not (memq (car case) type))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nvariant `~a’ is not in union type `~a'”
(get-output-string s) (car case) name))]
[(memq (car case) (cdr case))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nduplicated cases `~a’ in union-case of type `~a'”
(get-output-string s) (car case) name))]
[else (check-union-case expr name (remq (car case) type) (cdr case))])))
(define pc-union-type-does-not-exist?
(lambda (who var ut st* arg** body**)
(let* ([arg-count* (map length arg**)]
[sub-type* (map cons st* arg-count*)]
[type `(,ut ,sub-type*)])
(check-union-case
`(,who ,var ,ut
,(map (lambda (st arg* body*)
(cons (cons st arg*) body*))
st* arg** body**))
ut (map car (cadr (lookup-union ut))) (map car sub-type*)))))
(define-syntax pc-err
(syntax-rules ()
[(_ who code (str arg …))
(begin
(printf “\nParentheC Error – In Expression:\n\n”)
(pretty-print code)
(error who str arg …))]))
;;; Table needed for define-label
(define **pc-func-name-table** ‘())
(define pc-add-func-name!
(lambda (func-name)
(set! **pc-func-name-table**
(cons func-name **pc-func-name-table**))))
(define pc-func-name-exists?
(lambda (fn)
(memv fn **pc-func-name-table**)))
;;; Table needed for define-union
(define **pc-union-type-table** `())
(define pc-add-union-type!
(lambda (union-type sub-tn* arg-count*)
(set! **pc-union-type-table**
(cons `(,union-type ,(map cons sub-tn* arg-count*)) **pc-union-type-table**))))
(define pc-union-type-exists?
(lambda (union-type)
(assv union-type **pc-union-type-table**)))
(define pc-error-check:define-label
(lambda (code)
(match code
[`(define-label ,fn)
(pc-err ‘define-label code (“must have at least one body”))]
[`(define-label (,fn . ,p*) ,body)
(pc-err ‘define-label code (“cannot have any parameters”))]
[`(define-label ,fn ,body . ,body*)
(if (pc-func-name-exists? fn)
(pc-err ‘define-label code
(“function name ~s already exists” fn))
(void))]
[else (pc-err ‘define-label code (“invalid syntax”))])))
(define pc-error-check:define-union
(lambda (code)
(match code
[`(define-union ,union-type)
(pc-err ‘define-union code
(“must have at least one sub-type in union-type: ~s” union-type))]
[`(define-union ,union-type . ,c*)
(let ((sub-tn* (map car c*))
(arg** (map cdr c*)))
(pc-check-set-of-vars ‘define-union code sub-tn*)
(for-each
(lambda (arg*)
(pc-check-set-of-vars ‘define-union code arg*))
arg**)
(if (pc-union-type-exists? union-type)
(pc-err ‘define-union code
(“union-type ~s already exists” union-type))
(void)))]
[else (pc-err ‘define-union code (“invalid syntax”))])))
(define pc-error-check:general-union-case
(lambda (code who)
(match code
[`(general-union-case ,label ,var ,union-type)
(pc-err who code (“all union-type must have at least one sub-type”))]
[`(general-union-case ,label ,var ,union-type . ,c*)
(let* ((test* (map car c*))
(sub-tn* (map car test*))
(arg** (map cdr test*))
(body** (map cdr c*)))
(pc-check-set-of-vars who code `(,var ,union-type))
(pc-check-set-of-vars who code sub-tn*)
(for-each
(lambda (arg*)
(pc-check-set-of-vars who code arg*))
arg**)
(if (ormap null? body**)
(pc-err who code
(“all union-case clause must contain at least one body”))
(void))
(pc-union-type-does-not-exist? who var union-type
sub-tn* arg** body**))]
[else (pc-err who code (“invalid syntax”))])))
(define pc-check-set-of-vars
(letrec
([set-of-vars?
(lambda (ls)
(or (null? ls)
(and (not (memv (car ls) (cdr ls))) (set-of-vars? (cdr ls)))))])
(lambda (who code vars)
(if (not (set-of-vars? vars))
(pc-err who code (“duplicate variable used: ~s” vars))
(void))))))
(require ‘help (for-syntax ‘help))
(provide define-program-counter
define-registers
define-label
mount-trampoline
dismount-trampoline
define-union
union-case
union-case/free)
;;*************************************************************************************
;;*************************************************************************************
;; Syntax: define-label,
;; mount-trampoline,
;; dismount-trampoline,
;; define-union,
;; union-case,
;; union-case/free
(define-syntax define-label
(lambda (x)
(pc-error-check:define-label (syntax->datum x))
(syntax-case x ()
[(_ fn body …)
(pc-add-func-name! (syntax->datum #’fn))
#'(define fn (lambda () body …))])))
(define-syntax define-union
(lambda (x)
(pc-error-check:define-union (syntax->datum x))
(syntax-case x ()
[(__ union-type [sub-tn arg* …] …)
(let ([ut-val (syntax->datum #’union-type)]
[st*-val (syntax->datum #'(sub-tn …))]
[arg-count*-val (map length (syntax->datum #'((arg* …) …)))])
(with-syntax
([(constructor-fn* …)
(datum->syntax #’__
(map (lambda (st-val)
(string->symbol (format “~s_~s” ut-val st-val)))
st*-val))]
[(arg-count* …)
(datum->syntax #’__ arg-count*-val)])
(pc-add-union-type! ut-val st*-val arg-count*-val)
#'(begin
(define constructor-fn*
(lambda n-arg
(if (eq? (length n-arg) arg-count*)
`(union-type sub-tn ,@n-arg)
(pc-err ‘constructor-fn* `(constructor-fn* ,@n-arg)
(“wrong number of arguments to constructor: expected ~s”
arg-count*)))))
…)))])))
(define-syntax union-case
(lambda (x)
(syntax-case x ()
[(_ exp union-type [(sub-tn arg* …) body* …] …)
#'(general-union-case union-case exp union-type
[(sub-tn arg* …) body* …] …)])))
(define-syntax union-case/free
(lambda (x)
(syntax-case x ()
[(_ exp union-type [(sub-tn arg* …) body* …] …)
#'(general-union-case union-case/free exp union-type
[(sub-tn arg* …) body* …] …)])))
(define-syntax general-union-case
(lambda (x)
(let ([code (syntax->datum x)])
(pc-error-check:general-union-case code (cadr code)))
(syntax-case x ()
[(_ label var union-type [(sub-tn arg* …) body] …)
#'(let ([code ‘(label var union-type [(sub-tn arg* …) body] …)])
;;(if (not (pc-valid-variant? ‘union-type var))
;; (pc-err ‘label code
;; (“invalid datum for union-type \”~s\”: ~s” ‘union-type var))
;; (void))
(case (cadr var)
[(sub-tn) (apply (lambda (arg* …) body) (cddr var))]
…
[else (pc-err
‘label code
(“It should never come here: ~s, ~s” var ‘union-type))]))])))
;; this version has “macro expansion time” error checking and “runtime” error checking.
;; Helper functions should not interfere with correct parentheC code because all
;; helper functions have a “-“(minus) in them. Which you cannot use.
;; Test codes.
(define-syntax define-registers
(syntax-rules ()
((_ reg1 reg2 …)
(begin
(define reg1 0)
(define reg2 0)
…))))
(define-syntax define-program-counter
(syntax-rules ()
((_ pc)
(define-registers pc))))
(define-syntax mount-trampoline
(lambda (x)
(syntax-case x ()
[(_ construct reg pc)
#'(if (not (procedure? construct))
(error ‘mount-trampoline
“~s must evaluate to 1 arity #
(call/cc
(lambda (dismount-var)
(set! reg (construct dismount-var))
(let trampoline ()
(pc)
(trampoline)))))])))
(define-syntax dismount-trampoline
(lambda (x)
(syntax-case x ()
[(_ var)
#'(if (not (procedure? var))
(error ‘dismount-trampoline
“~s must evaluate to 1 arity #
(var 0))])))
#lang racket
(provide pc2c compile/run)
(define reg-funcs ‘())
(define reg-pc ‘no-pc)
(define dismount-var ‘no-dis)
(define construct-var ‘no-const)
(define add-func
(lambda (func)
(set! reg-funcs (cons func reg-funcs))))
(define is-func?
(lambda (func)
(assv func reg-funcs)))
(define reg-unions ‘())
(define check-args
(lambda (union args)
(cond
[(null? args) #t]
[(memq (car args) (cdr args))
(error ‘define-union “duplicated variant `~a’ in union `~a’\n” (car args) (car union))]
[else (check-args union (cdr args))])))
(define add-union
(lambda (union)
(if (not (lookup-union (car union)))
(begin (check-args union (cadr union))
(set! reg-unions (cons union reg-unions)))
(error ‘define-union “duplicated definition of union-type `~a’\n” (car union)))))
(define reg-regs ‘())
(define init-storage
(lambda ()
(set! reg-funcs ‘())
(set! reg-unions ‘())
(set! reg-regs ‘())))
(define new-safe-char
(lambda (char)
(cond
[(eq? #\? char) “r__q__”]
[(eq? #\! char) “r__f__”]
[(eq? #\. char) “r__d__”]
[(eq? #\+ char) “r__p__”]
[(eq? #\- char) “r__m__”]
[(eq? #\* char) “r__t__”]
[(eq? #\/ char) “r__di__”]
[(eq? #\< char) "r__lt__"]
[(eq? #\> char) “r__gt__”]
[(eq? #\: char) “r__co__”]
[(eq? #\$ char) “r__do__”]
[(eq? #\% char) “r__pe__”]
[(eq? #\^ char) “r__ex__”]
[(eq? #\& char) “r__am__”]
[(eq? #\~ char) “r__ti__”]
[(eq? #\_ char) “r_”]
[(and (char>=? char #\0) (char<=? char #\9))
(string-append "r" (list->string `(,char)))]
[else (list->string `(,char))])))
(define safe
(lambda (sym)
(if (symbol? sym)
(let loop ([l (string->list (symbol->string sym))])
(cond
[(null? l) “”]
[else (string-append (new-safe-char (car l)) (loop (cdr l)))]))
sym)))
(define join
(lambda (lst separater)
(let loop ([lst lst]
[result “”]
[is-first? #t])
(cond
[(null? lst) result]
[is-first? (loop (cdr lst) (format “~a” (car lst)) #f)]
[else (loop (cdr lst) (string-append result
(format “~a~a” separater (car lst))) #f)]))))
(define file->list
(lambda (fname)
(let ([file (open-input-file fname)])
(let ([data
(let recurse ([decl (read file)])
(if (eof-object? decl)
‘()
(cons decl (recurse (read file)))))])
(close-input-port file)
data))))
(define pc2c
(lambda (file-name source-name header-name)
;; WARNING: pc2c will erase existing files when generating new ones!
(when (file-exists? source-name) (delete-file source-name))
(when (file-exists? header-name) (delete-file header-name))
(init-storage)
(let ([decl* (file->list file-name)])
(let ([src (open-output-file source-name)]
[hdr (open-output-file header-name)])
(dynamic-wind
(lambda () #f)
(lambda ()
;; write a generated header file to header-name
(display (pc2c-header decl*) hdr)
(check-correct-info)
;; write a generated source file source-name
(display (pc2c-source header-name) src))
(lambda ()
(close-output-port src)
(close-output-port hdr)))))))
(define check-correct-info
(lambda ()
(begin
(if (null? reg-regs)
(display “Warning: you have defined no registers.\n”)
(void)))))
(define pc2c-append
(lambda args
(apply string-append
(map (lambda (elt)
(cond
[(symbol? elt) (format “~a” elt)]
[(number? elt) (format “~s” elt)]
[(string? elt) elt]
[else (error ‘pc2c-append “Invalid argument ~s” elt)]))
args))))
(define pc2c-gen-unions
(lambda (union)
(let ([name (safe (car union))]
[tag* (cadr union)]
[field** (caddr union)])
(apply string-append
(map (lambda (tag field*)
(let ([tag (safe tag)])
(pc2c-append
(pc2c-fn-proto (pc2c-append name “r_” tag) field*) ” {\n”
name “* _data = (” name “*)malloc(sizeof(” name “));\n”
“if(!_data) {\n”
” fprintf(stderr, \”Out of memory\\n\”);\n”
” exit(1);\n”
“}\n”
” _data->tag = _” tag “_” name “;\n”
(apply string-append
(map (lambda (field)
(let ([field (safe field)])
(format ” _data->u._~a._~a = ~a;\n”
tag field field)))
field*))
” return (void *)_data;\n”
“}\n\n”)))
tag* field**)))))
;; added by wy for constructor argument name binding
;; lookup-arg looks up the argument name of name.tag at position pos
(define lookup-union
(lambda (name)
(let loop ([reg reg-unions])
(cond
[(null? reg) #f]
[(eq? name (caar reg)) (car reg)]
[else (loop (cdr reg))]))))
(define get-arg-list
(lambda (name tag)
(let ([u (lookup-union name)])
(if (not u) (error ‘lookup-union
“union type `~a’ not defined\n” name)
(let loop ([tags (cadr u)] [args (caddr u)])
(cond
[(null? tags)
(error ‘lookup-arg
“union type `~a’ doesn’t have a tag `~a’~n” name tag)]
[(eq? tag (car tags)) (car args)]
[else (loop (cdr tags) (cdr args))]))))))
(define lookup-arg
(lambda (name tag pos)
(list-ref (get-arg-list name tag) pos)))
(define check-union-case
(lambda (expr name type case)
(cond
[(and (null? type) (not (null? case)))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nsuperfluous cases for union type `~a’: ~a”
(get-output-string s) name case))]
[(and (null? case) (not (null? type)))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nunmatched cases for union type `~a’: ~a”
(get-output-string s) name type))]
[(and (null? type) (null? case)) #t]
[(not (memq (car case) type))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nvariant `~a’ is not in union type `~a'”
(get-output-string s) (car case) name))]
[(memq (car case) (cdr case))
(let ([s (open-output-string)])
(pretty-print expr s)
(error ‘union-case “~a\nduplicated cases `~a’ in union-case of type `~a'”
(get-output-string s) (car case) name))]
[else (check-union-case expr name (remq (car case) type) (cdr case))])))
(define case-env
(lambda (env var*)
(let loop ([env env] [var* var*])
(if (null? var*)
env
(extend-env (car var*) (car var*) (loop env (cdr var*)))))))
(define handle-union-case-case
(lambda (name env)
(lambda (template body)
(match template
[`(,tag . ,var*) #:when (list? var*)
(let ([sname (safe name)]
[stag (safe tag)])
(let ([given (length var*)] [expected (length (get-arg-list name tag))])
(if (not (= given expected))
(error ‘union-case
“~a\nwrong number of arguments to constructor `~a’ of union-type `~a’: expected: ~a, given: ~a”
template tag name expected given)
(pc2c-append
“case _” stag “_” sname “: {\n”
(let loop ([var* var*] [n 0])
(cond
[(null? var*) “”]
[else (string-append
(pc2c-append
“void *” (safe (car var*)) ” = _c->u._” stag
“._” (safe (lookup-arg name tag n)) “;\n”)
(loop (cdr var*) (add1 n)))]))
((parse-function-body #t (case-env env var*)) body)
“break; }\n”))))]
;; Cannot possibly be effective, commented JBH 12/13
;; [else (string-append “default {\n”
;; ((parse-function-body #t (case-env env var*)) body)
;; “}\n”)]
))))
(define get-last
(lambda (ls)
(cond
((null? ls) #f)
((null? (cdr ls)) (car ls))
(else (get-last (cdr ls))))))
;; this is for error checking
(define get-body
(lambda (c)
(match c
[`(,test ,body) body])))
(define remove-last
(lambda (ls)
(match ls
[`((else ,body)) ‘()]
[`((,test ,body) . ,c*) `((,test ,body) . ,(remove-last c*))])))
(define apply-env
(lambda (env x)
(match env
[`(empty-env) (error ’empty-env “unbound variable: ~s” x)]
[`(extend-env ,x^ ,a ,env)
(if (eq? x^ x) a (apply-env env x))])))
(define extend-env
(lambda (x a env)
`(extend-env ,x ,a ,env)))
(define empty-env
(lambda ()
`(empty-env)))
(define parse-function-body
(lambda (tail env)
(if tail
(lambda (expr)
(match expr
[`(error ,name ,msg)
(pc2c-append
“fprintf(stderr, \”” msg “\”);\n exit(1);\n”)]
[`(if ,test ,conseq ,alt)
(let ((test ((parse-function-body #f env) test))
(conseq ((parse-function-body #t env) conseq))
(alt ((parse-function-body #t env) alt)))
(pc2c-append
“if(” test “) {\n”
” ” conseq “\n”
“} else {\n”
” ” alt “\n”
“}\n”))]
[`(cond (else ,body))
(let ((body ((parse-function-body #t env) body)))
body)]
[`(cond . ,c*)
(let ((last (get-last c*))
(c* (remove-last c*)))
(cond
[(eq? (car last) ‘else)
(let* ((test0 ((parse-function-body #f env) (caar c*)))
(body0 ((parse-function-body #t env) (get-body (car c*))))
(test* (map (parse-function-body #f env) (map car (cdr c*))))
(body* (map (parse-function-body #t env) (map get-body (cdr c*))))
(body ((parse-function-body #t env) (cadr last))))
(pc2c-append
“if(” test0 “) {\n”
” ” body0 “\n”
“}”
(apply string-append
(map (lambda (x y)
(pc2c-append ” else if(” x “) {\n”
y
“}\n”))
test* body*))
” else {\n”
” ” body “\n”
“}\n”))]
[else
(let* ((test0 ((parse-function-body #f env) (caar c*)))
(body0 ((parse-function-body #t env) (cadar c*)))
(test* (map (parse-function-body #f env) (map car (cdr c*))))
(body* (map (parse-function-body #t env) (map cadr (cdr c*)))))
(pc2c-append
“if(” test0 “) {\n”
” ” body0 “\n”
“}”
(apply string-append
(map (lambda (x y)
(pc2c-append “else if(” x “) {\n”
y
“}\n”))
test* body*))))]))]
[`(begin . ,expr*)
(apply string-append (map (parse-function-body #t env) expr*))]
[`(set! ,var ,var1) #:when (eq? var var1) “”]
[`(set! ,var ,val)
(let ((val ((parse-function-body #f env) val)))
(if (equal? (safe var) reg-pc)
(pc2c-append (safe var) ” = &” val “;\n”)
(pc2c-append (safe var) ” = (void *)” val “;\n”)))]
[`(union-case ,val ,name . ,c*)
(let ((template* (map car c*))
(body* (map get-body c*)))
(if (not (check-union-case expr name
(cadr (or (lookup-union name)
(error ‘lookup-union
“union type `~a’ not defined ~n” name)))
(map car template*)))
(error ‘union-case “union-case doesn’t match definition: `~a’\n”
name)
(let ([sname (safe name)]
[val (safe val)])
(pc2c-append
sname “* _c = (” sname “*)” val “;\n”
“switch (_c->tag) {\n”
(apply string-append
(map (handle-union-case-case name env) template* body*))
“}\n”
))))]
[`(let ,bind* ,body)
(let ((lhs* (map car bind*))
(rhs* (map (parse-function-body #f env) (map cadr bind*))))
(pc2c-append
“{\n”
(apply string-append
(map (lambda (x y)
(pc2c-append
“void *” (safe x) ” = (void *)” y “;\n”))
lhs* rhs*))
body
“}\n”))]
[`(printf ,str . ,parms*)
(let ([str (list->string
(let loop ([str (string->list str)])
(if (null? str)
‘()
(if (char=? (car str) #\~)
(if (and (not (null? (cdr str)))
(not (char=? (cadr str) #\ )))
(cons #\% (cons #\d (loop (cddr str))))
(cons #\% (loop (cdr str))))
(cons (car str) (loop (cdr str)))))))]
[parms (map safe parms*)])
(string-append
“printf(” (join (cons (format “~s” str) parms)
“, (int)”) “);”))]
[`(mount-trampoline ,construct ,dismount ,pc)
(set! construct-var (safe construct))
(set! dismount-var (safe dismount))
(pc2c-append
“mount_tram();\n”)]
[`(dismount-trampoline ,dismount)
(pc2c-append
“_trstr *trstr = (_trstr *)” (safe dismount) “;\n”
“longjmp(*trstr->jmpbuf, 1);\n”
)]
[`(,func) #:when (is-func? func)
(pc2c-append reg-pc ” = &” (safe func) “;\n”)]
[`,elsee
(let ((elsee ((parse-function-body #f env) elsee)))
(pc2c-append “return(” elsee “);\n”))]
))
(lambda (expr)
(match expr
;; [(error ,name ,msg)
;; (pc2c-append
;; “fprintf(stderr, \”” msg “\”);\n exit(1);\n”)]
[`#t (pc2c-append “(void *)” 1)]
[`#f (pc2c-append “(void *)” 0)]
[`,x #:when (symbol? x) (safe (apply-env env x))]
[`,x #:when (integer? x) (pc2c-append “(void *)” x)]
[`(zero? ,x)
(let ((x ((parse-function-body #f env) x)))
(pc2c-append “(” x ” == 0)”))]
[`(and ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(” a ” && ” b “)”))]
[`(or ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(” a ” || ” b “)”))]
[`(not ,x)
(let ((x ((parse-function-body #f env) x)))
(pc2c-append “(!” x “)”))]
[`(< ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append "(" a " < " b ")"))]
[`(> ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(” a ” > ” b “)”))]
[`(<= ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append "(" a " <= " b ")"))]
[`(>= ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(” a ” >= ” b “)”))]
[`(+ ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(void *)((int)” a ” + (int)” b “)”))]
[`(* ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(void *)((int)” a ” * (int)” b “)”))]
[`(- ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(void *)((int)” a ” – (int)” b “)”))]
[`(/ ,a ,b)
(let ((a ((parse-function-body #f env) a))
(b ((parse-function-body #f env) b)))
(pc2c-append “(void *)((int)” a ” / (int)” b “)”))]
[`(sub1 ,a)
(let ((a ((parse-function-body #f env) a)))
(pc2c-append “(void *)((int)” a ” – 1)”))]
[`(add1 ,a)
(let ((a ((parse-function-body #f env) a)))
(pc2c-append “(void *)((int)” a ” + 1)”))]
[`(random ,x)
(let ((x ((parse-function-body #f env) x)))
(pc2c-append “(void *)(rand() % (int)” x “)”))]
[`(if ,test ,conseq ,alt)
(let ((test ((parse-function-body #f env) test))
(conseq ((parse-function-body #f env) conseq))
(alt ((parse-function-body #f env) alt)))
(pc2c-append “(” test ” ? ” conseq ” : ” alt “)”))]
[`(,func . ,args*) #:when (symbol? func)
(let ((args* (map (parse-function-body #f env) args*)))
(pc2c-append
(safe func) “(” (join args* “,”) “)”))])))))
(define pc2c-gen-funcs
(lambda (env)
(lambda (func)
(let ([name (safe (car func))]
[body (cadr func)])
(pc2c-append
(if (equal? name “main”)
“int ”
“void “) name “()\n”
“{\n”
((parse-function-body #t env) body)
“}\n\n”
)))))
(define global-env
(lambda ()
(let loop ([env (empty-env)]
[reg (append (map car reg-funcs) reg-regs)])
(if (null? reg)
env
(extend-env (car reg) (car reg) (loop env (cdr reg)))))))
(define pc2c-source
(lambda (header-name)
(let* ([s1 (apply string-append (map pc2c-gen-unions reg-unions))]
[s2 (apply string-append (map (pc2c-gen-funcs (global-env)) reg-funcs))])
(let ([s3 (pc2c-append
“int mount_tram ()\n”
“{\n”
“srand (time (NULL));\n”
“jmp_buf jb;\n”
“_trstr trstr;\n”
“void *dismount;\n”
“int _status = setjmp(jb);\n”
“trstr.jmpbuf = &jb;\n”
“dismount = &trstr;\n”
“if(!_status) {\n”
dismount-var “= (void *)” construct-var “(dismount);\n”
“for(;;) {\n”
reg-pc “();\n”
“}\n”
“}\n”
“return 0;\n”
“}\n”)])
(string-append
“#include
“#include
“#include
“#include
“#include \”” header-name “\”\n”
“\n”
s1
s2
s3)))))
(define pc2c-header
(lambda (decl*)
(string-append
(apply string-append
(map pc2c-header-parse decl*))
“int mount_tram();\n\n”
“struct _trstr;\n”
“typedef struct _trstr _trstr;\n”
“struct _trstr {\n”
” jmp_buf *jmpbuf;\n”
” int value;\n”
“};\n\n”)))
(define pc2c-header-parse
(lambda (decl)
(match decl
[`(load ,file . ,file*) “”]
[`(exit) “”]
[`(display ,anything . ,anything*) “”]
[`(pretty-print ,anything . ,anything*) “”]
[`(define-registers . ,reg*)
(set! reg-regs reg*)
(if (null? reg*)
“”
(string-append
“void *”
(join (map safe reg*) “, *”)
“;\n\n”))]
[`(define-program-counter ,pc) (set! reg-pc (safe pc))
(string-append “void (*” reg-pc “)();\n\n”)]
[`(define-union ,name . ,c*)
(let ((tag* (map car c*))
(field** (map cdr c*)))
(add-union `(,name ,tag* ,field**))
(let ([name (safe name)])
(let ([enum-tags
(join
(map (lambda (tag)
(pc2c-append “_” (safe tag) “_” name)) tag*)
“,\n “)]
[structs
(apply string-append
(map
(lambda (tag field*)
(let ([tag (safe tag)])
(if (null? field*)
(format
” struct { char dummy; } _~a;\n” tag)
(string-append
” struct {”
(apply string-append
(map
(lambda (field)
(format ” void *_~a;” (safe field)))
field*))
(format ” } _~a;\n” tag)))))
tag* field**))]
[structors
(apply string-append
(map
(lambda (tag field*)
(let ([tag (safe tag)])
(string-append
(pc2c-fn-proto (pc2c-append name “r_” tag)
field*)
“;\n”)))
tag* field**))])
(pc2c-append
“struct ” name “;\n”
“typedef struct ” name ” ” name “;\n”
“struct ” name ” {\n”
” enum {\n”
” ” enum-tags “\n”
” } tag;\n”
” union {\n”
structs
” } u;\n”
“};\n\n”
structors “\n”))))]
[`(define-label ,name ,body)
(begin (add-func `(,name ,body))
(string-append (if (equal? (safe name) “main”)
“int ”
“void “) (safe name) “();\n”))])))
(define pc2c-fn-proto
(lambda (fn-name param*)
(let ([declare-params
(lambda (param*)
(join (map (lambda (param)
(format “void *~a” (safe param))) param*) “, “))])
(pc2c-append
“void *” (safe fn-name) “(” (declare-params param*) “)”))))
(define compile/run
(lambda (base-name)
(let ([pc-file (string-append base-name “.pc”)]
[c-file (string-append base-name “.c”)]
[header-file (string-append base-name “.h”)])
(pc2c pc-file c-file header-file)
(let ([compile-command (string-append “gcc -o ” base-name ” ” c-file)]
[indent-command (string-append “indent -bad -bap -br -nbs -ce”
“-cli1 -di1 -i2 -npro -npsl “)])
(let ([compile-val (system compile-command)])
(unless (eqv? compile-val #t)
(error ‘compile/run “Compilation command ‘~s’ returned ~s”
compile-command compile-val))
(system (string-append indent-command c-file))
(system (string-append indent-command header-file))
(system (string-append “./” base-name))
(void))))))
#lang pie
#|
warriors ⇒ software engineers : programs
mages ⇒ mathematicians : proofs
witchers ⇒ PL researchers
|#
#|
Dependent type theory is also called constructive type theory.
|#
#|
For each type, there are four questions:
1, (Formation) how to make such a type
2, (Construction) how to make a member (inhabitant) of this type
3, (Elimination) how to use a member of this type
4, (Equality) how to compare members of this type
|#
#|
Judgments
A is a U
A is the same U as B
|#
#|
the type Nat
1, Nat is a type
2, – zero is a Nat
– if n is a Nat, then (add1 n) is a Nat
3, – (which-Nat n base step)
where step is a function, (λ (n-1) …), this function will be applied
to n-1, if n takes the form (add1 n-1)
– (rec-Nat n base step)
where step is a function, (λ (n-1 almost) …),
almost represents the recursion result, this function will be applied
to n-1 and the recursive result, if n takes the form (add1 n-1)
4, – zero is the same Nat as zero
– m is the same Nat as n, (add1 m) is the same Nat as (add1 n)
|#
#|
the type (→ A B)
1, if A is a type and B is a type, (→ A B) is a type
2, – if assuming x is an A while b is a B,
then (λ (x) b) is a (→ A B),
3, – if f is a (→ A B) and arg is an A, then (f arg) is a B
4, – f is (→ A B) and g is (→ A B),
f and g are the same if f is consistently renamed g, α-conversion
– f is (→ A B), (λ (x) (f x)) is the same (→ A B) as f, η-conversion
|#
#|
the type (Π ([x A]) B)
unfinshed
|#
#|
the type (List A)
unfinished
|#
(claim five Nat)
(define five 5)
(claim zero?
(→ Nat
Atom))
(define zero?
(λ (n)
(which-Nat n
‘yes
(λ (n-1)
‘no))))
#|
(+ 3 5)
almost: (+ 2 5)
|#
(claim +
(→ Nat Nat
Nat))
(define +
(λ (n m)
(rec-Nat n
m
(λ (n-1 almost)
#| almost is the natural recursion, (+ n-1 m) |#
(add1 almost)
))
#|In dependent types, EVERY program has to TERMINATE.|#
#;
(cond
[(zero? n) m]
[else (add1 (+ (sub1 n) m))])))
#|
(gauss 10) -> 55
almost: (gauss 9) -> 45
|#
(claim gauss
(→ Nat
Nat))
(define gauss
(λ (n)
(rec-Nat n
0
(λ (n-1 almost)
(+ almost (add1 n-1))))))
(claim id₁
(→ Nat
Nat))
(define id₁
(λ (n)
n))
(claim id₂
(→ Nat
Nat))
(define id₂
(λ (x)
x))
(claim id₃
(→ Nat
Nat))
(define id₃
(λ (m)
(id₁ m)))
(claim id₄
(→ U
U))
(define id₄
(λ (A)
A))
#;
(claim repeat
(→ A Nat
(List Atom)))
#;
(define repeat
(λ (a n)
(rec-Nat n
(the (List Atom) nil)
(λ (n-1 almost)
(:: a almost)))))
#;
(claim repeat-nat
(→ Nat Nat
(List Nat)))
#;
(define repeat-nat
(λ (a n)
(rec-Nat n
(the (List Nat) nil)
(λ (n-1 almost)
(:: a almost)))))
(claim repeat
(Π ([A U])
(→ A Nat
(List A))))
(define repeat
(λ (A)
(λ (a n)
(rec-Nat n
(the (List A) nil)
(λ (n-1 almost)
(:: a almost))))))
#lang pie
(claim +
(Π ([n Nat]
[m Nat])
Nat)
#;
(→ Nat Nat
Nat))
(define +
(λ (n m)
(rec-Nat n
m
(λ (n-1 almost)
(add1 almost)))))
(claim gauss
(→ Nat
Nat))
(define gauss
(λ (n)
(rec-Nat n
0
(λ (k gauss-of-k)
#|if n is 100,
k = 99, gauss-of-99
k = 98, …|#
(+ gauss-of-k (add1 k))))))
#|
For each type, there are four questions:
1, (Formation) how to make such a type
2, (Construction) how to make a member (inhabitant) of this type
3, (Elimination) how to use a member of this type
4, (Equality) how to compare members of this type
|#
#|
the type Nat
1, Nat is a type
2, – zero is a Nat
– if n is a Nat, then (add1 n) is a Nat
3, – (rec-Nat n base step)
(rec-Nat 0 base step) ≡ base
(rec-Nat (add1 n) base step) ≡ (step n (rec-Nat n base step))
how to type it?
if we have
– n is a Nat
– base is an A
– step is a (→ Nat A A)
then we have
– (rec-Nat n base step) is an A
– (ind-Nat n motive base step)
motive is a (→ Nat U)
base is a (motive 0)
step is (Π ([k Nat] [ih (motive k)]) (motive n))
4, – zero is the same Nat as zero
– m is the same Nat as n, (add1 m) is the same Nat as (add1 n)
|#
#|
the type (→ A B)
1, if A is a type and B is a type, (→ A B) is a type
2, – if assuming x is an A while b is a B,
then (λ (x) b) is a (→ A B),
3, – if f is a (→ A B) and arg is an A, then (f arg) is a B
4, – f is (→ A B) and g is (→ A B),
f and g are the same if f is consistently renamed g, α-conversion
– f is (→ A B), (λ (x) (f x)) is the same (→ A B) as f, η-conversion
|#
#|
the type (Π ([x A]) B)
(→ A B) is a syntax sugar for (Π ([x A]) B), if x is not used in B
1, if A is a type and B is a type by assuming x has type A, (Π ([x A]) B) is a type
2, – if assuming x is an A while b is a B,
then (λ (x) b) is a (→ A B),
3, – if f is a (→ A B) and arg is an A, then (f arg) is a B
4, – f is (→ A B) and g is (→ A B),
f and g are the same if f is consistently renamed g, α-conversion
– f is (→ A B), (λ (x) (f x)) is the same (→ A B) as f, η-conversion
|#
#;
(claim repeat
(Π ([X U])
(Π ([n Nat])
(List X))))
#|
the type (List A)
1, if A is a type, (List A) is a type
2, – nil is a (List A)
– if a is an A and d is a (List A), (:: a d) is a (List A)
3, – (rec-List ls base step)
(rec-List nil base step) ≡ base
(rec-List (:: a d) base step) ≡ (step a d (rec-List n base step))
how to type it?
if we have
– ls is a (List A)
– base is an B
– step is a (→ A (List A) B B)
then we have
– (rec-List n base step) is an B
4,
|#
(claim length
(Π ([X U])
(→ (List X)
Nat)))
(define length
(λ (X xs)
(rec-List xs
0
(λ (a d length-of-d)
(add1 length-of-d)))))
(claim append
(Π ([X U])
(→ (List X) (List X)
(List X))))
(define append
(λ (X xs ys)
(rec-List xs
ys
(λ (a d append-d-ys)
append-d-ys))))
(claim append-vector
(Π ([X U]
[n Nat]
[m Nat])
(→ (Vec X n) (Vec X m)
(Vec X (+ n m)))))
(define append-vector
(λ (X n)
(ind-Nat n
#|motive, why|#
(λ (n) (Π ([m Nat])
(→ (Vec X n) (Vec X m)
(Vec X (+ n m)))))
(λ (m xs ys)
#|
givens:
n : Nat n is 0
m : Nat
xs : (Vec X 0)
ys : (Vec X m)
goal:
(Vec X m)
|#
ys)
(λ (k ih #|induction-hypothesis|#)
(λ (m xs ys)
#|
givens:
k : Nat
ih : (Π ([m Nat])
(→ (Vec X k) (Vec X m)
(Vec X (+ k m))))
m : Nat
(ih m) : (→ (Vec X k) (Vec X m)
(Vec X (+ k m)))
xs : (Vec X (add1 k))
(head xs) : X
(tail xs) : (Vec X k)
(ih m (tail xs) ys) : (Vec X (+ k m))
(vec:: (head xs) (ih m (tail xs) ys)) : (Vec X (+ (add1 k) m))
ys : (Vec X m)
goal:
(Vec X (+ (add1 k) m))
|#
(vec:: (head xs) (ih m (tail xs) ys)))))))
#;
(append-vector Atom 2 3
(vec:: ‘cat (vec:: ‘cat vecnil))
(vec:: ‘dog (vec:: ‘dog (vec:: ‘dog
vecnil))))
(claim vec→list
(Π ([X U]
[ℓ Nat])
#|——- |#
(→ (Vec X ℓ)
(List X))))
(define vec→list
(λ (X ℓ)
(ind-Nat ℓ
(λ (k) (→ (Vec X k)
(List X)))
(λ (vec-of-length-0) nil)
(λ (k ih)
(λ (v-of-add1-k)
(:: (head v-of-add1-k) (ih (tail v-of-add1-k))))
#|
givens:
k : Nat
ih : (→ (Vec X k)
(List X))
v (A.K.A v-of-add1-k) : (Vec X (add1 k))
(tail v) : (Vec X k)
(ih (tail v)) : (List X)
(:: (head v) (ih (tail v))) : (List X)
goal:
(List X)
|#
))))
(vec→list Atom 5
(the (Vec Atom 5)
(vec:: ‘cat
(vec:: ‘cat
(vec:: ‘dog
(vec:: ‘dog
(vec:: ‘dog vecnil)))))))
#lang racket
(provide defrel
conde conda condu
condᵉ
fresh
run run*
== ≡ =/= ≠ absento numbero symbolo numberᵒ symbolᵒ absentᵒ
succeed fail
prt)
#|microKanren, Ch 10|#
(define nothing
(vector))
(define (var sym scp)
(vector sym scp nothing))
(define var? vector?)
(define (var-has-val? x)
(not (equal? nothing (vector-ref x 2))))
(define (var-val x)
(vector-ref x 2))
(define (set-var-val! x v)
(vector-set! x 2 v))
(define (var-scp x)
(vector-ref x 1))
#;
(struct State
(s
scp
t
neqs
abs))
(struct Scope
())
(define State
(λ (s scp t neqs abs)
`(,s ,scp ,t ,neqs ,abs)))
(define init-S
(State (make-immutable-hasheqv) (Scope) (make-immutable-hasheqv) ‘()
(make-immutable-hasheqv)))
(define (walk v s)
(cond
[(var? v)
(cond
[(var-has-val? v)
(walk (var-val v) s)]
[(hash-ref s v #f)
=>
(λ (v) (walk v s))]
[else v])]
[else v]))
(define (ext-s x v s)
(cond
[(occurs? x v s) #f]
[else (hash-set s x v)]))
(define (occurs? x v s)
(let ([v (walk v s)])
(cond
[(var? v) (eqv? v x)]
[(pair? v) (or (occurs? x (car v) s)
(occurs? x (cdr v) s))]
[else #f])))
(define (unify u v s scp new-pairs)
(let ([u (walk u s)]
[v (walk v s)])
(cond
[(eqv? u v) (cons s new-pairs)]
[(var? u) (cond
[(eqv? (var-scp u) scp)
(if (occurs? u v s)
#f
(begin (set-var-val! u v)
(cons s `((,u . ,v) . ,new-pairs))))]
[else
(go-on ([s (ext-s u v s)])
(cons s `((,u . ,v) . ,new-pairs)))])]
[(var? v) (cond
[(eqv? (var-scp v) scp)
(if (occurs? v u s)
#f
(begin (set-var-val! v u)
(cons s `((,v . ,u) . ,new-pairs))))]
[else
(go-on ([s (ext-s v u s)])
(cons s `((,v . ,u) . ,new-pairs)))])]
[(and (pair? u) (pair? v))
(go-on ([`(,s . ,new-pairs) (unify (car u) (car v) s scp new-pairs)]
[`(,s . ,new-pairs) (unify (cdr u) (cdr v) s scp new-pairs)])
(cons s new-pairs))]
[else #f])))
(define (== u v)
(λS (S @ s scp t neqs abs)
(go-on ( [`(,s . ,new-pairs) (unify u v s scp ‘())]
[neqs (validate-neqs neqs s)]
[t (validate-types new-pairs t)]
[`(,neqs . ,abs) (validate-abs new-pairs neqs abs s)])
`(,(State s scp t neqs abs))
‘())))
(define (succeed S) `(,S))
(define (fail S) ‘())
(define ((disj₂ g₁ g₂) S)
($append (g₁ S) (g₂ S)))
(define ($append $₁ $₂)
(cond
[(null? $₁) $₂]
[(pair? $₁) (cons (car $₁) ($append (cdr $₁) $₂))]
[else (λ () ($append $₂ ($₁)))]))
(define ($take n $)
(cond
[(and n (zero? n)) ‘()]
[(null? $) ‘()]
[(pair? $) (cons (car $) ($take (and n (sub1 n)) (cdr $)))]
[else ($take n ($))]))
(define ((conj₂ g₁ g₂) S)
($append-map g₂ (g₁ S)))
(define ($append-map g $)
(cond
[(null? $) ‘()]
[(pair? $) ($append (g (car $)) ($append-map g (cdr $)))]
[else (λ () ($append-map g ($)))]))
(define call/fresh
(λ (name f)
(λS (S @ s scp t neqs abs)
((f (var name scp)) S))))
(define (reify-name n)
(string->symbol (string-append “_” (number->string n))))
(define (walk* v s)
(let ([v (walk v s)])
(cond
[(var? v) v]
[(pair? v) (cons (walk* (car v) s)
(walk* (cdr v) s))]
[else v])))
(define (reify-s v s)
(let ([v (walk v s)])
(cond
[(var? v) (let ([n (hash-count s)])
(let ([rn (reify-name n)])
(hash-set s v rn)))]
[(pair? v) (let ([s (reify-s (car v) s)])
(reify-s (cdr v) s))]
[else s])))
(define (reify v)
(λS (S @ s scp t neqs abs)
(let ([v (walk* v s)])
(let ([names (reify-s v (make-immutable-hasheqv))])
(walk* v names)))))
(define (run-goal n g)
($take n (g init-S)))
(define ((ifte g₁ g₂ g₃) S)
(let loop ([$ (g₁ S)])
(cond
[(null? $) (g₃ S)]
[(pair? $)
($append-map g₂ $)]
[else (λ () (loop ($)))])))
(define ((once g) S)
(let loop ([$ (g S)])
(cond
[(null? $) ‘()]
[(pair? $) (cons (car $) ‘())]
[else (λ () (loop ($)))])))
#|macros, connecting wires|#
(define-syntax disj
(syntax-rules ()
[(disj) fail]
[(disj g) g]
[(disj g₀ g …) (disj₂ g₀ (disj g …))]))
(define-syntax conj
(syntax-rules ()
[(conj) succeed]
[(conj g) g]
[(conj g₀ g …) (conj₂ g₀ (conj g …))]))
(define-syntax defrel
(syntax-rules ()
[(defrel (name x …) g …)
(define (name x …)
(λ (s)
(λ ()
((conj g …) s))))]))
(define-syntax run
(syntax-rules ()
[(run n (x₀ x …) g …)
(run n q (fresh (x₀ x …)
(== `(,x₀ ,x …) q)
g …))]
[(run n q g …)
(let ([q (var ‘q (Scope))])
(map (reify q) (run-goal n (conj g …))))]))
(define-syntax run*
(syntax-rules ()
[(run* q g …) (run #f q g …)]))
(define-syntax fresh
(syntax-rules ()
[(fresh () g …) (conj g …)]
[(fresh (x₀ x …) g …)
(call/fresh ‘x₀
(λ (x₀)
(fresh (x …) g …)))]))
(define-syntax conde
(syntax-rules ()
[(conde (g …) …) ((call/new-scope) (disj (conj g …) …))]))
(define-syntax condᵉ
(syntax-rules ()
[(condᵉ (g …) …) ((call/new-scope) (disj (conj g …) …))]))
(define-syntax conda
(syntax-rules ()
[(conda (g₀ g …)) (conj g₀ g …)]
[(conda (g₀ g …) ln …)
(ifte g₀ (conj g …) (conda ln …))]))
(define-syntax condu
(syntax-rules ()
[(condu (g₀ g …) …)
(conda ((once g₀) g …) …)]))
(define (call/new-scope)
(λ (g)
(λS (S @ s scp t neqs abs)
(g (State s (Scope) t neqs abs)))))
#|other constraints|#
(define ((prt c) S)
(let ([s (State-s S)])
(begin (displayln (walk* c s))
`(,S))))
(define (validate-neqs neqs s)
(cond
[(null? neqs) ‘()]
[else (go-on ([new-car (unify-all (car neqs) s ‘())])
(if (null? new-car)
#f
(go-on ([new-cdr (validate-neqs (cdr neqs) s)])
(cons new-car new-cdr)))
(validate-neqs (cdr neqs) s))]))
(define (unify-all ls s new-pairs)
(cond
[(null? ls) new-pairs]
[else (go-on ([`(,s . ,new-pairs)
(unify (car (car ls)) (cdr (car ls)) s (Scope) new-pairs)])
(unify-all (cdr ls) s new-pairs))]))
(define (validate-types ls types)
(cond
[(null? ls) types]
[else (go-on ([types (propogate-type (car ls) types)]
[types (validate-types (cdr ls) types)])
types)]))
(define (propogate-type pr types)
(let ([u (car pr)]
[v (cdr pr)])
(cond
[(var? v) (let ([u-type (hash-ref types u #f)]
[v-type (hash-ref types v #f)])
(cond
[(and u-type v-type) (and (eqv? u-type v-type) types)]
[u-type (hash-set types v u-type)]
[v-type (hash-set types u v-type)]
[else types]))]
[else (let ([u-type (hash-ref types u #f)])
(cond
[u-type (and (u-type v) types)]
[else types]))])))
(define (unicons x ls)
(if (memv x ls) ls (cons x ls)))
(define (not-appears u v neqs abs s)
(let ([u (walk u s)]
[v (walk v s)])
(cond
[(var? v) (let ([v-abs (hash-ref abs v #f)])
(cons (cons `((,v . ,u)) neqs)
(hash-set abs v (unicons u (or v-abs ‘())))))]
[(pair? v) (go-on ([`(,neqs . ,abs) (not-appears u (car v) neqs abs s)])
(not-appears u (cdr v) neqs abs s))]
[else (and (not (eqv? u v)) (cons neqs abs))])))
(define (validate-abs ls neqs abs s)
(cond
[(null? ls) (cons neqs abs)]
[else (let ([pr (car ls)])
(let ([u (car pr)]
[v (cdr pr)])
(let ([u-abs (hash-ref abs u #f)])
(if u-abs
(go-on ([`(,neqs . ,abs)
(propogate-abs u-abs v neqs abs s)])
(validate-abs (cdr ls) neqs abs s))
(validate-abs (cdr ls) neqs abs s)))))]))
(define (propogate-abs ls t neqs abs s)
(cond
[(null? ls) (cons neqs abs)]
[else (go-on ([`(,neqs . ,abs) (not-appears (car ls) t neqs abs s)])
(propogate-abs (cdr ls) t neqs abs s))]))
(define ≡ ==)
(define (=/= u v)
(λS (S @ s scp t neqs abs)
(go-on ([`(,s^ . ,new-pairs) (unify u v s (Scope) ‘())])
(if (null? new-pairs)
‘()
`(,(State s scp t (cons new-pairs neqs) abs)))
`(,S))))
(define ≠ =/=)
(define (booleano u)
(typeo boolean? u))
(define (numbero u)
(typeo number? u))
(define numberᵒ numbero)
(define (symbolo u)
(typeo symbol? u))
(define symbolᵒ symbolo)
(define (typeo pred u)
(λS (S @ s scp t neqs abs)
(let ([u (walk u s)])
(cond
[(var? u) (let ([u-type (hash-ref t u #f)])
(cond
[u-type (if (eqv? u-type pred) `(,S) ‘())]
[else `(,(State s scp (hash-set t u pred) neqs abs))]))]
[(pred u) `(,S)]
[else ‘()]))))
(define (absento u v)
(λS (S @ s scp t neqs abs)
(go-on ([`(,neqs . ,abs) (not-appears u v neqs abs s)])
`(,(State s scp t neqs abs))
‘())))
(define absentᵒ absento)
#|syntax sugars|#
(define-syntax go-on
(syntax-rules ()
[(_ () then) then]
[(_ () then alter) then]
[(_ ([p₀ e₀] [p e] …) then)
(cond
[e₀ => (λ (v) (match v
[p₀ (go-on ([p e] …) then)]))]
[else #f])]
[(_ ([p₀ e₀] [p e] …) then alter)
(cond
[e₀ => (λ (v) (match v
[p₀ (go-on ([p e] …) then alter)]))]
[else alter])]))
(define (State-s S)
(car S))
(define (State-scp S)
(car (cdr S)))
(define (State-t S)
(car (cdr (cdr S))))
(define (State-neqs S)
(car (cdr (cdr (cdr S)))))
(define (State-abs S)
(car (cdr (cdr (cdr (cdr S))))))
(define-syntax λS
(syntax-rules (@)
[(_ (S @ s scp t neqs abs) b)
(λ (S)
(let ([s (State-s S)]
[scp (State-scp S)]
[t (State-t S)]
[neqs (State-neqs S)]
[abs (State-abs S)])
b))]))
#lang racket
(require “mkr.rkt”)
(define Γ₀
‘((x . ℕ) (x . 𝔹) (z . ℕ)))
(defrel (lookupᵒ Γ x t)
(fresh (x^ t^ Γ^)
(≡ `((,x^ . ,t^) . ,Γ^) Γ)
(conde
[(≡ x^ x) (≡ t^ t)]
[(≠ x^ x)
(lookupᵒ Γ^ x t)])))
#;
(run 2 q
(lookupᵒ Γ₀ ‘x q))
#;
(run 1 τ
(lookupᵒ Γ₀ ‘x τ))
(defrel (⊢ Γ e τ)
(conde
[(symbolo e)
(lookupᵒ Γ e τ)]
[(fresh (x body)
(== `(fix (λ (,x) ,body)) e)
(⊢ `((,x . ,τ) . ,Γ) body τ))]
[(numbero e)
(== τ ‘ℕ)]
[(conde
[(== e #t)]
[(== e #f)])
(== τ ‘𝔹)]
[(fresh (e₁ e₂)
(== `(* ,e₁ ,e₂) e)
(⊢ Γ e₁ ‘ℕ)
(⊢ Γ e₂ ‘ℕ)
(== τ ‘ℕ))]
[(fresh (e₁ e₂ e₃)
(== `(if ,e₁ ,e₂ ,e₃) e)
(⊢ Γ e₁ ‘𝔹)
(⊢ Γ e₂ τ)
(⊢ Γ e₃ τ))]
[(fresh (e₁)
(== `(sub1 ,e₁) e)
(⊢ Γ e₁ ‘ℕ)
(== τ ‘ℕ))]
[(fresh (e₁)
(== `(zero? ,e₁) e)
(⊢ Γ e₁ ‘ℕ)
(== τ ‘𝔹))]
[(fresh (x body)
(== `(λ (,x) ,body) e)
(symbolo x)
(fresh (τin τout)
(== `(→ ,τin ,τout) τ)
(⊢ `((,x . ,τin) . ,Γ) body τout)))]
[(fresh (rator rand)
(== `(,rator ,rand) e)
(fresh (τin)
(⊢ Γ rator `(→ ,τin ,τ))
(⊢ Γ rand τin)))]
))
#;
(run 10 τ
(⊢ ‘()
‘(λ (y) (zero? ((λ (x) (sub1 y)) 4)))
τ))
#;
(run 1 τ
(⊢ ‘() `((fix (λ (fact)
(λ (n)
(if (zero? n)
1
(* n (fact (sub1 n)))))))
5)
τ))
(defrel (lookup2ᵒ vars vals x o)
(fresh (var val vars^ vals^)
(≡ `(,var . ,vars^) vars)
(≡ `(,val . ,vals^) vals)
(conde
[(≡ var x) (≡ val o)]
[(≠ var x)
(lookup2ᵒ vars^ vals^ x o)])))
(defrel (valof*ᵒ vars vals es o)
(conde
[(== ‘() es)
(== ‘() o)]
[(fresh (a d)
(== `(,a . ,d) es)
(fresh (aᵒ dᵒ)
(== `(,aᵒ . ,dᵒ) o)
(valofᵒ vars vals a aᵒ)
(valof*ᵒ vars vals d dᵒ)))]))
(defrel (valofᵒ vars vals e val)
(conde
[(symbolo e)
(lookup2ᵒ vars vals e val)]
[(== `(quote ,val) e)
(absentᵒ ‘clos val)]
[(fresh (es)
(== `(list . ,es) e)
(absentᵒ ‘list vars)
(valof*ᵒ vars vals es val))]
[(fresh (x body)
(== `(λ (,x) ,body) e)
(symbolo x)
(=/= ‘quote x)
(=/= ‘λ x)
(== `(clos ,x ,body ,vars ,vals) val))]
[(fresh (rator rand)
(== `(,rator ,rand) e)
(fresh (x body vars^ vals^ a)
(valofᵒ vars vals rator `(clos ,x ,body ,vars^ ,vals^))
(valofᵒ vars vals rand a)
(valofᵒ `(,x . ,vars^) `(,a . ,vals^) body val)))]))
(defrel (quine e)
(valofᵒ ‘() ‘() e e))
(defrel (twine e₁ e₂)
(=/= e₁ e₂)
(valofᵒ ‘() ‘() e₁ e₂)
(valofᵒ ‘() ‘() e₂ e₁))
(defrel (thrine e₁ e₂ e₃)
(=/= e₁ e₂)
(=/= e₂ e₃)
(valofᵒ ‘() ‘() e₁ e₂)
(valofᵒ ‘() ‘() e₂ e₃)
(valofᵒ ‘() ‘() e₃ e₁))
(run 10 e
(quine e))
#lang pie
(claim +
(→ Nat Nat
Nat))
(define +
(λ (n m)
(rec-Nat n
m
(λ (n-1 almost)
(add1 almost)))))
(claim sub1
(→ Nat
Nat))
(define sub1
(λ (n)
(which-Nat n
0
(λ (n-1)
n-1))))
#|
Identity type
1, (Formation)
if X is a U, a is an X and b is an X, then (= X a b) is a U
2, (Contruction)
(same a) is an element of (= X a a)
3, (Elimination)
– cong
4, (Equality)
|#
#|
Sigma type
1, (Formation)
if X is a U, x is an A, and
assuming x is X gives you Y is a U,
then (Σ ([x X]) Y) is a U
|#
(claim one-is-one
(= Nat 1 1))
(define one-is-one
#|refl|#
(same 1))
(claim one-is-two
(= Nat 1 2))
#;
(define one-is-two
TODO)
#|cannot be proved|#
(claim sub1-add1-same
(Π ([n Nat])
(= Nat (sub1 (add1 n)) n)))
(define sub1-add1-same
(λ (n)
#|This is what pie will do in the backend|#
#|(= Nat (sub1 (add1 n)) n)|#
#|(= Nat (which-Nat (add1 n)
0
(λ (n-1)
n-1))
n)|#
#|(= Nat n n)|#
(same n)))
#|
∀ n,m. (+ (add1 n) m) ≡ (add1 (+ n m))
|#
(claim add1-jumps-out
(Π ([n Nat]
[m Nat])
(= Nat (+ (add1 n) m) (add1 (+ n m)))))
(define add1-jumps-out
(λ (n m)
#|
(= Nat (+ (add1 n) m) (add1 (+ n m)))
1, find out all eliminator in the expression
2, if the target of the eliminator has add1 on the top, then the expression
can be reduced (the eliminator is called a redex)
(rec-Nat (add1 n)
m
(λ (n-1 almost) #|step|#
(add1 almost)))
=>
(step n (rec-Nat n m step))
(step n (+ n m))
(add1 (+ n m))
(= Nat (add1 (+ n m)) (add1 (+ n m)))
|#
(same (add1 (+ n m)))))
#|
∀ n,m. (add1 (+ n m)) ≡ (+ (add1 n) m)
|#
(claim add1-jumps-in
(Π ([n Nat]
[m Nat])
(= Nat (add1 (+ n m)) (+ (add1 n) m))))
(define add1-jumps-in
(λ (n m)
(ind-Nat n
(λ (?) (= Nat
(add1 (+ ? m))
(+ (add1 ?) m)))
#|(= Nat (add1 (+ 0 m)) (+ (add1 0) m))|#
#|(= Nat (add1 m) (+ (add1 0) m))|#
#|(= Nat (add1 m) (add1 (+ 0 m)))|#
#|(= Nat (add1 m) (add1 m))|#
(same (add1 m))
(λ (k ih)
#|
k : Nat
ih : (= Nat (add1 (+ k m)) (add1 (+ k m)))
(add1 (+ k m)) = (add1 (+ k m))
(add1 (add1 (+ k m))) = (add1 (add1 (+ k m)))
goal : (= Nat (add1 (add1 (+ k m))) (add1 (add1 (+ k m))))
|#
#|
congruence : (cong (= X a b) f) ⇒ (= X (f a) (f b))
|#
(cong ih (+ 1)
#;
(the (→ Nat Nat)
(λ (x)
(add1 x)))))
)))
#;
(define add1-jumps-in
(λ (n m)
#|(symm (= X a b)) ⇒ (= X b a)|#
(symm (add1-jumps-out n m))))
(claim +-is-associative
(Π ([m Nat]
[n Nat]
[p Nat])
(= Nat (+ m (+ n p)) (+ (+ m n) p))))
(define +-is-associative
(λ (m n p)
(ind-Nat m
(λ (?) (= Nat (+ ? (+ n p)) (+ (+ ? n) p)))
#|(= Nat (+ n p) (+ n p))|#
(same (+ n p))
(λ (k ih)
#|
k : Nat
ih : (= Nat (+ k (+ n p)) (+ (+ k n) p))
goal : (= Nat (add1 (+ k (+ n p))) (add1 (+ (+ k n) p)))
|#
(cong ih (+ 1))))))
(claim Even
(→ Nat
U))
(define Even
(λ (n)
(Σ ([n/2 Nat])
(= Nat n (+ n/2 n/2)))))
(claim four-is-Even
(Even 4))
(define four-is-Even
(cons 2 (same 4)))
#lang typed/racket
#|
bi-directional type checking
check: Γ ⊢ e ∈ τ, Γ e τ all inputs, boolean output
– constructors are annotated and checked
synth: Γ ⊢ e ↑ τ, Γ e inputs, τ output
– eliminators are synthed
Γ ⊢ e : τ
α
β
|#
#|
Exercises:
1, add the Nat type (Nat, zero, add1, rec-Nat)
2, add the List type ((List A), nil, ::, rec-List)
3, add the Σ type (basically copying the Π type)
|#
(: lookup (All (A D) (→ (Listof (Pairof A D)) A D)))
(define (lookup ρ x)
(match ρ
[‘() (error “unbound ” x)]
[`((,a . ,d) . ,ρ^)
(if (eqv? a x) d (lookup ρ^ x))]))
(: ext (All (A D) (→ (Listof (Pairof A D)) A D (Listof (Pairof A D)))))
(define (ext l a d)
`((,a . ,d) . ,l))
(define-type Exp
(U (List ‘Π (List (List Symbol Exp)) Exp) #|(Π ([x A]) B)|#
(List ‘λ (List Symbol) Exp) #|(λ (x) b)|#
(List Exp Exp) #|(rator rand)|#
‘U
Symbol
))
(: β (→ Exp Symbol Exp
Exp))
(define (β e x t)
(match e
[`,y
#:when (symbol? y)
(if (eqv? y x) t y)]
[‘U ‘U]
[`(λ (,y) ,b)
(cond
#|
There is a third case: y occurs free in t.
Then you need to α-rename y before the recursion on b.
|#
[(eqv? y x)
#|(x (λ (x) x)) x y|#
`(λ (,y) ,b)]
[else
#|(x (λ (z) x)) x y|#
`(λ (,y) ,(β b x t))])]
[`(Π ([,y ,A]) ,B)
(cond
#|
There is a third case: y occurs free in t.
Then you need to α-rename y before the recursion on B.
|#
[(eqv? y x)
`(Π ([,y ,(β A x t)]) ,B)]
[else
`(Π ([,y ,(β A x t)]) ,(β B x t))])]
[`(,rator ,rand)
`(,(β rator x t) ,(β rand x t))]))
(define-type Context #|we use Γ for contexts|#
(Listof (Pairof Symbol Exp)))
(: synth (→ Context Exp
(U Exp False)))
(define (synth Γ e)
(match e
[`,y
#:when (symbol? y)
(lookup Γ y)]
[‘U ‘U]
[`(Π ([,x ,A]) ,B)
(go-on ([_ (check Γ A ‘U)]
[_ (check (ext Γ x A) B ‘U)])
‘U)]
[`(,rator ,rand)
(go-on ([`(Π ([,x ,A]) ,B) (synth Γ rator)]
[_ (check Γ rand A)])
#|
(f 5)
f : (Π ([n Nat]) (Vec Atom n))
5 : Nat
(Vec Atom 5)
|#
(β B x rand))]))
(: check (→ Context Exp Exp
Boolean))
(define (check Γ e τ)
(match `(,e ,τ)
[`((λ (,x) ,b) (Π ([,x^ ,A]) ,B))
#|e.g. (λ (x) x) (Π ([a Nat]) Nat)|#
#|e.g. (λ (x) x) (Π ([n Nat]) (Vec Atom n))|#
(check (ext Γ x A) b (β B x^ x))]
[`(,elim ,τ)
(go-on ([τ^ (synth Γ elim)])
(aeq? τ τ^))]))
(define-type DExp
#|de~Bruijn Exp|#
(U (List ‘Π (List DExp) DExp)
(List ‘λ DExp)
(List DExp DExp)
‘U
Symbol
Number))
(: lex (→ Exp (Listof Symbol)
DExp))
(define (lex e names)
(match e
[`,y
#:when (symbol? y)
(or (index-of names y) y)]
[`(Π ([,x ,A]) ,B)
`(Π (,(lex A names)) ,(lex B (cons x names)))]
[`(λ (,x) ,b)
`(λ ,(lex b (cons x names)))]
[`(,rator ,rand)
`(,(lex rator names) ,(lex rand names))]
[‘U ‘U]))
(: aeq? (→ Exp Exp Boolean))
(define (aeq? e₁ e₂)
(equal? (lex e₁ ‘())
(lex e₂ ‘())))
(define-type UserExp
(U ‘U
(List ‘λ (Listof Symbol) UserExp)
(List ‘Π (Listof (List Symbol UserExp)) UserExp)
(Listof UserExp)
Symbol))
(: pre (→ UserExp Exp))
(define (pre e)
(match e
[`(Π () ,e)
(pre e)]
[`(Π ([,x ,e₁] . ,d) ,e₂)
#:when (symbol? x)
`(Π ([,x ,(pre e₁)])
,(pre `(Π ,d ,e₂)))]
[`(λ () ,e)
(pre e)]
[`(λ (,x . ,d) ,e)
#:when (symbol? x)
`(λ (,x)
,(pre `(λ ,d ,e)))]
[‘U ‘U]
[`,x
#:when (symbol? x)
x]
[`(,f . ,d)
(let ([d (map (λ ([e : UserExp]) (pre e)) d)])
(foldl (λ ([e : Exp]
[r : Exp])
`(,r ,e))
(pre f)
d))]))
(: run (→ UserExp UserExp Boolean))
(define (run e t)
(check ‘() (pre e) (pre t)))
#;
(let ([t ‘(Π ([A U]
[a A])
A)]
[e ‘(λ (A a)
a)])
(run e t))
(let ([t ‘(Π ([ℕ U]
[Vec (Π ([X U]
[n ℕ])
U)]
[+ (Π ([n₁ ℕ]
[n₂ ℕ])
ℕ)]
[append (Π ([X U]
[n₁ ℕ]
[n₂ ℕ]
[v₁ (Vec X n₁)]
[v₂ (Vec X n₂)])
(Vec X (+ n₁ n₂)))]
[X U]
[n₁ ℕ]
[n₂ ℕ]
[v₁ (Vec X n₁)]
[v₂ (Vec X n₂)])
(Vec X (+ n₁ n₂)))]
[e ‘(λ (ℕ Vec + append X n₁ n₂ v₁ v₂)
(append X n₁ n₂ v₁ v₂))])
(run e t))
(define-syntax go-on
(syntax-rules ()
[(go-on () r) r]
[(go-on ([p₀ e₀] [p e] …) r)
(cond
[e₀
=>
(λ (v)
(match v
[p₀ (go-on ([p e] …) r)]))]
[else #f])]))
#lang racket
(define append-map-cps
(λ (f-cps ls k)
(cond
[(null? ls) (k ‘())]
[else (f-cps (car ls)
(λ (ls₁)
(append-map-cps f-cps (cdr ls)
(λ (ls₂)
(k (append ls₁ ls₂))))))])))
(call/cc (λ (k)
(+ (k 1) (k 2) (k 3))))
(define !-
(λ (G e t)
(conde
[(fresh (e₁ e₂ t₁)
(== `(begin2 ,e₁ ,e₂) e)
(!- G e₁ t₁)
(!- G e₂ t))]
[(fresh (ma f b a)
(== `(bind-maybe ,ma ,f) e)
(== `(Maybe ,b) t)
(!- G ma `(Maybe ,a))
(!- G f `(,a -> (Maybe ,b))))])))
#|
Γ,x:τ₁ ⊢ b : τ
Γ ⊢ e : τ₁
—————————–
Γ ⊢ (let ((x e)) b) : τ
|#
b -> ‘fish
c -> `(fish)
a -> `(fish)
‘(((fish) fish (fish)))
#;
(defrel (append-cdrᵒ ls o)
(conde
[(== ‘() ls)
(== ‘() o)]
[(fresh (a d res)
(== `(,a . ,d) ls)
(append-cdrᵒ d res)
(appendᵒ ls res o))]))
(define gcd
(λ (a b)
(cond
[(eqv? a b) (inj-writer a)]
[(> a b)
(go-on ([_ (tell `(swapping ,a ,b))])
(gcd b a))]
[else (gcd a (- b a))])))
(define at-least-two
(λ (n)
(which-Nat n
‘nil
(λ (n-1)
(which-Nat n
‘nil
(λ (n-1)
‘t))))))
#lang racket
(require “monads.rkt”)
(define store ‘())
(define fib/effects
(λ (n)
(cond
[(assv n store)
=>
(λ (assv-result) (cdr assv-result))]
[(zero? n) 1]
[(zero? (sub1 n)) 1]
[else (let ([fib-sub1 (fib/effects (sub1 n))]
[fib-sub2 (fib/effects (sub1 (sub1 n)))])
(begin (set! store `((,n . ,(+ fib-sub1 fib-sub2)) . ,store))
(+ fib-sub1 fib-sub2)))])))
(define fib/sps
(λ (n store)
(cond
[(assv n store)
=>
(λ (assv-result) `(,(cdr assv-result) . ,store))]
[(zero? n) `(1 . ,store)]
[(zero? (sub1 n)) `(1 . ,store)]
[else (match-let* ([`(,fib-sub1 . ,store) (fib/sps (sub1 n) store)]
[`(,fib-sub2 . ,store) (fib/sps (sub1 (sub1 n)) store)])
`(,(+ fib-sub1 fib-sub2) . ((,n . ,(+ fib-sub1 fib-sub2)) . ,store)))])))
#|
A programming language is low level when its programs require attention to the irrelevant.
— Alan Perlis
|#
#;
(fib/sps 100 ‘())
#|State monad|#
#|
state monad : is a pair of a pure and a store
inj-state : puts something at the pure part (→ A (State S A))
put : puts something at the store part (→ S (State S A))
bind-state : (→ (State S A) (→ A (State S B)) (State S B))
get : takes the store part from a state monad (→ (State S A) S)
(get `(,store . ,pure)) => `(,store . ,store)
|#
#;
((run-state (inj-state 5)) ‘init-state)
#;
((run-state (put ‘new-state)) ‘init-state)
#;
((run-state
(bind-state (inj-state 5)
(λ (pure)
(inj-state (zero? pure)))))
‘dc)
#;
((run-state
(bind-state (put 5)
(λ (pure)
(get))))
‘dc)
; (→ Number (State (Listof (Pairof Number Number)) Number))
#;
(define fib
(λ (n)
(bind-state (get)
(λ (store)
(cond
[(assv n store)
=>
(λ (assv-result)
(inj-state (cdr assv-result)))]
[(zero? n) (inj-state 1)]
[(zero? (sub1 n)) (inj-state 1)]
[else (bind-state (fib (sub1 n))
(λ (fib-sub1)
(bind-state (fib (sub1 (sub1 n)))
(λ (fib-sub2)
(bind-state (get)
(λ (store)
(bind-state (put `((,n . ,(+ fib-sub1 fib-sub2)) . ,store))
(λ (_)
(inj-state (+ fib-sub1 fib-sub2))))))))))])))))
#;
(cdr ((run-state (fib 1000)) ‘()))
#;
((run-state
(bind-state (inj-state 5)
(λ (pure)
(bind-state (inj-state (zero? pure))
(λ (bool)
(inj-state (eqv? #t bool)))))))
‘dc)
#;
((run-state
(go-on ([pure (inj-state 5)]
[bool (inj-state (zero? pure))])
(inj-state (eqv? #t bool))))
‘dc)
(define fib
(λ (n)
(bind-state (get)
(λ (store)
(cond
[(assv n store)
=>
(λ (assv-result)
(inj-state (cdr assv-result)))]
[(zero? n) (inj-state 1)]
[(zero? (sub1 n)) (inj-state 1)]
[else
(go-on ([fib-sub1 (fib (sub1 n))]
[fib-sub2 (fib (sub1 (sub1 n)))]
[store (get)]
[_ (put `((,n . ,(+ fib-sub1 fib-sub2)) . ,store))])
(inj-state (+ fib-sub1 fib-sub2)))])))))
#;
(cdr ((run-state (fib 1000)) ‘()))
#|
maybe monad : is a pair of a pure and a store
Just : puts something at the pure part (→ A (Maybe A))
Nothing : puts something at the store part (→ (Maybe A))
bind-maybe: (→ (Maybe A) (→ A (Maybe B)) (Maybe B))
|#
; (: lookup (→ Symbol (Listof (Pairof Symbol A)) (Maybe A)))
(define lookup
(λ (x ls)
(match ls
[‘() (Nothing)]
[`((,x^ . ,v) . ,ls^)
(if (eqv? x^ x)
(Just v)
(lookup x ls^))])))
#;
(lookup ‘x ‘((x . (Nothing)) (y . 10)))
#lang typed/racket/no-check
;#lang typed/racket
(provide (all-defined-out))
(struct (A) Just
([a : A])
#:transparent)
(struct Nothing
()
#:transparent)
(define-type (Maybe A)
(U (Just A)
Nothing))
(: bind-maybe (All (A B) (-> (Maybe A) (-> A (Maybe B)) (Maybe B))))
(define (bind-maybe ma f)
(match ma
[(Just a) (f a)]
[(Nothing) (Nothing)]))
(struct Unit
())
(struct (W A) Writer
([log : (Listof W)]
[a : A]))
(: run-writer (All (W A) (-> (Writer W A) (Pair (Listof W) A))))
(define (run-writer ma)
(match ma
[(Writer log a) (cons log a)]))
(: inj-writer (All (W A) (-> A (Writer W A))))
(define (inj-writer a)
(Writer ‘() a))
(: tell (All (W) (-> W (Writer W Unit))))
(define (tell msg)
(Writer (list msg) (Unit)))
(: bind-writer (All (W A B) (-> (Writer W A) (-> A (Writer W B)) (Writer W B))))
(define (bind-writer ma f)
(match ma
[(Writer la a) (match (run-writer (f a))
[(cons lb b) (Writer (append la lb) b)])]))
(: pass (All (W A) (-> (Writer W A) (-> (Listof W) (Listof W)) (Writer W A))))
(define (pass ma f)
(match ma
[(Writer la a) (Writer (f la) a)]))
(: listen (All (W A) (-> (Writer W A) (Writer W (Pair (Listof W) A)))))
(define (listen ma)
(match ma
[(Writer la a) (Writer la (cons la a))]))
(struct (Store A) State
([run-state : (-> Store (Pair Store A))]))
(: inj-state (All (S A) (-> A (State S A))))
(define (inj-state a)
(State (λ ([s : S]) (cons s a))))
(: run-state (All (S A) (-> (State S A) (-> S (Pair S A)))))
(define run-state State-run-state)
(: bind-state (All (S A B) (-> (State S A) (-> A (State S B)) (State S B))))
(define (bind-state ma f)
(State (λ ([s : S])
(match ((run-state ma) s)
[`(,s . ,a) ((run-state (f a)) s)]))))
(: get (All (S) (-> (State S S))))
(define (get)
(State (λ ([s : S])
(cons s s))))
(: put (All (S) (-> S (State S Unit))))
(define (put s)
(State (λ (_) (cons s (Unit)))))
(struct (R A) Cont
([run-cont : (-> (-> A R) R)]))
(: run-cont (All (R A) (-> (Cont R A) (-> (-> A R) R))))
(define run-cont Cont-run-cont)
(: inj-cont (All (R A) (-> A (Cont R A))))
(define (inj-cont a)
(Cont (λ ([k : (-> A R)]) (k a))))
(: bind-cont (All (A B R) (-> (Cont R A) (-> A (Cont R B)) (Cont R B))))
(define (bind-cont ma f)
(Cont (λ ([k : (-> B R)])
((run-cont ma) (λ ([a : A]) ((run-cont (f a)) k))))))
(: callcc (All (R A B) (-> (-> (-> A (Cont R B)) (Cont R A)) (Cont R A))))
(define (callcc f)
(Cont (λ ([k : (-> A R)])
((run-cont (f (λ (a) (Cont (λ (_) (k a))))))
k))))
(: inj-list (All (A) (Listof A)))
(define (inj-list a)
`(,a))
(: empty-list (All (A) (Listof A)))
(define (empty-list)
‘())
(: bind-list (All (A B) (→ (Listof A) (→ A (Listof B))
(Listof B))))
(define (bind-list ls f)
(append-map f ls))
(define bind
(λ (m f)
(cond
[(or (Just? m) (Nothing? m)) (bind-maybe m f)]
[(Writer? m) (bind-writer m f)]
[(State? m) (bind-state m f)]
[(Cont? m) (bind-cont m f)]
[(list? m) (bind-list m f)]
[else (error “bind: ~a is not a monad” m)])))
#;
(define-syntax go-on
(syntax-rules (<-)
[(_ e) e]
[(_ (v₀ <- e₀) e ...)
(bind e₀ (λ (v₀) (go-on e ...)))]
[(_ e₀ e ...)
(bind e₀ (λ (_) (go-on e ...)))]))
(define-syntax go-on
(syntax-rules ()
[(_ () b) b]
[(_ ([v₀ e₀] pr ...) b)
(bind e₀ (λ (v₀) (go-on (pr ...) b)))]))
#lang racket
(require "monads.rkt")
#|
| inject-pure | inject-effect | bind
state | inj-state (→ A (State S A)) | put (-> S (State S A)) | bind-state (→ (State S A) (→ A (State S B)) (State S B))
maybe | Just (→ A (Maybe A)) | Nothing (→ (Maybe A)) | bind-maybe (→ (Maybe A) (→ A (Maybe B)) (Maybe B))
writer | inj-writer | tell | bind-writer
cont | inj-k | callcc | bind-k
list | (→ A (Listof A)) | (→ (Listof A)) | (→ (Listof A) (→ A (Listof B)) (Listof B)))
|#
#|
For list, inject-pure is (λ (a) (cons a ‘()))
inject-effect is (λ (_) ‘())
bind is append-map
to prove law1, we have to show that
(append-map `(,a) f) ≡ (f a)
lhs: (append (f a) (append-map ‘() f))
lhs: (append (f a) ‘())
lhs: (f a)
to prove law2, we have to show that
(append-map ls (λ (a) (cons a ‘()))) ≡ ls
– (append-map ‘() (λ (a) (cons a ‘()))) ≡ ‘()
‘()
– (append-map `(,a . ,d) (λ (a) (cons a ‘()))) ≡ `(,a . ,d)
(append `(,a) (append-map d f)) ≡ `(,a . ,d)
by induction hypothesis, (append-map d f) ≡ d
lhs: (append `(,a) d)
lhs: `(,a . ,d)
|#
(define product
(λ (xs ys)
(bind-list xs
(λ (x)
(bind-list ys
(λ (y)
(inj-list `(,x . ,y))))))
#;
(go-on ([x xs]
[y ys])
(inj-list `(,x . ,y)))))
#;
(product ‘(1 2) ‘(3 4 5))
(define append-map
(λ (ls f)
(cond
[(null? ls) ‘()]
[else (append (f (car ls))
(append-map (car ls) f))])))
#|
To claim something T is a monad
find inject-pure, inject-effect, and bind
law1: left-id (bind (inj-pure a) f) ≡ (f a)
law2: right-id (bind ma inj-pure) ≡ ma
law3: assoc (bind (bind ma f) g) ≡ (bind ma (λ (x) (bind (f x) g)))
|#
#;
(run-writer
(bind-writer (tell ‘something-else)
(λ (_)
(bind-writer (tell ‘something)
(λ (_)
(inj-writer 5))))))
#;
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(env y)]
[`,n
#:when (number? n)
n]
[`(+ ,e₁ ,e₂)
(+ (valof e₁ env) (valof e₂ env))]
[`(λ (,x) ,body)
(λ (a) (valof body (λ (y) (if (eqv? y x) a (env y)))))]
[`(,rator ,rand)
((valof rator env) (valof rand env))])))
#;
(define valof
(λ (exp env)
(bind-writer (tell `(valof ,exp ,env))
(λ (_)
(match exp
[`,y
#:when (symbol? y)
(inj-writer (env y))]
[`,n
#:when (number? n)
(inj-writer n)]
[`(+ ,e₁ ,e₂)
(go-on ([n₁ (valof e₁ env)]
[n₂ (valof e₂ env)])
(inj-writer (+ n₁ n₂)))]
[`(λ (,x) ,body)
(inj-writer (λ (arg) (valof body (λ (y) (if (eqv? y x) arg (env y))))))]
[`(,rator ,rand)
(go-on ([clos (valof rator env)]
[arg (valof rand env)])
(clos arg))])))))
#;
(run-writer
(valof ‘(((λ (x) (λ (y) (+ x y))) 5) 42)
(λ (y) (error “unbound ” y))))
(define valof
(λ (exp env)
(match exp
[`,y
#:when (symbol? y)
(inj-k (env y))]
[`,n
#:when (number? n)
(inj-k n)]
[`(+ ,e₁ ,e₂)
(go-on ([n₁ (valof e₁ env)]
[n₂ (valof e₂ env)])
(inj-k (+ n₁ n₂)))]
[`(let/cc ,kvar ,body)
#|callcc is call-with-current-continuation|#
#|this is not Racket’s call/cc|#
#|this is the function in line 101 in monads.rkt|#
(callcc (λ (k) (valof body (λ (y) (if (eqv? y kvar) k (env y))))))]
[`(λ (,x) ,body)
(inj-k (λ (a) (valof body (λ (y) (if (eqv? y x) a (env y))))))]
[`(,rator ,rand)
(go-on ([clos (valof rator env)]
[arg (valof rand env)])
(clos arg))])))
#;
((run-k
(valof ‘(let/cc k (((λ (x) (λ (y) (+ (k x) y))) 5) 42))
(λ (y) (error “unbound ” y))))
(λ (v) v))
#lang typed/racket/no-check
;#lang typed/racket
(provide (all-defined-out))
(struct (A) Just
([a : A])
#:transparent)
(struct Nothing
()
#:transparent)
(define-type (Maybe A)
(U (Just A)
Nothing))
(: bind-maybe (All (A B) (-> (Maybe A) (-> A (Maybe B)) (Maybe B))))
(define (bind-maybe ma f)
(match ma
[(Just a) (f a)]
[(Nothing) (Nothing)]))
(struct Unit
())
(struct (W A) Writer
([log : (Listof W)]
[a : A]))
(: run-writer (All (W A) (-> (Writer W A) (Pair (Listof W) A))))
(define (run-writer ma)
(match ma
[(Writer log a) (cons log a)]))
(: inj-writer (All (W A) (-> A (Writer W A))))
(define (inj-writer a)
(Writer ‘() a))
(: tell (All (W) (-> W (Writer W Unit))))
(define (tell msg)
(Writer (list msg) (Unit)))
(: bind-writer (All (W A B) (-> (Writer W A) (-> A (Writer W B)) (Writer W B))))
(define (bind-writer ma f)
(match ma
[(Writer la a) (match (run-writer (f a))
[(cons lb b) (Writer (append la lb) b)])]))
(: pass (All (W A) (-> (Writer W A) (-> (Listof W) (Listof W)) (Writer W A))))
(define (pass ma f)
(match ma
[(Writer la a) (Writer (f la) a)]))
(: listen (All (W A) (-> (Writer W A) (Writer W (Pair (Listof W) A)))))
(define (listen ma)
(match ma
[(Writer la a) (Writer la (cons la a))]))
(struct (Store A) State
([run-state : (-> Store (Pair Store A))]))
(: inj-state (All (S A) (-> A (State S A))))
(define (inj-state a)
(State (λ ([s : S]) (cons s a))))
(: run-state (All (S A) (-> (State S A) (-> S (Pair S A)))))
(define run-state State-run-state)
(: bind-state (All (S A B) (-> (State S A) (-> A (State S B)) (State S B))))
(define (bind-state ma f)
(State (λ ([s : S])
(match ((run-state ma) s)
[`(,s . ,a) ((run-state (f a)) s)]))))
(: get (All (S) (-> (State S S))))
(define (get)
(State (λ ([s : S])
(cons s s))))
(: put (All (S) (-> S (State S Unit))))
(define (put s)
(State (λ (_) (cons s (Unit)))))
(struct (R A) Cont
([run-k : (-> (-> A R) R)]))
(: run-k (All (R A) (-> (Cont R A) (-> (-> A R) R))))
(define run-k Cont-run-k)
(: inj-k (All (R A) (-> A (Cont R A))))
(define (inj-k a)
(Cont (λ ([k : (-> A R)]) (k a))))
(: bind-k (All (A B R) (-> (Cont R A) (-> A (Cont R B)) (Cont R B))))
(define (bind-k ma f)
(Cont (λ ([k : (-> B R)])
((run-k ma) (λ ([a : A]) ((run-k (f a)) k))))))
(: callcc (All (R A B) (-> (-> (-> A (Cont R B)) (Cont R A)) (Cont R A))))
(define (callcc f)
(Cont (λ ([k : (-> A R)])
((run-k (f (λ (a) (Cont (λ (_) (k a))))))
k))))
(: inj-list (All (A) (Listof A)))
(define (inj-list a)
`(,a))
(: empty-list (All (A) (Listof A)))
(define (empty-list)
‘())
(: bind-list (All (A B) (→ (Listof A) (→ A (Listof B))
(Listof B))))
(define (bind-list ls f)
(append-map f ls))
(define bind
(λ (m f)
(cond
[(or (Just? m) (Nothing? m)) (bind-maybe m f)]
[(Writer? m) (bind-writer m f)]
[(State? m) (bind-state m f)]
[(Cont? m) (bind-k m f)]
[(list? m) (bind-list m f)]
[else (error “bind: ~a is not a monad” m)])))
#;
(define-syntax go-on
(syntax-rules (<-)
[(_ e) e]
[(_ (v₀ <- e₀) e ...)
(bind e₀ (λ (v₀) (go-on e ...)))]
[(_ e₀ e ...)
(bind e₀ (λ (_) (go-on e ...)))]))
(define-syntax go-on
(syntax-rules ()
[(_ () b) b]
[(_ ([v₀ e₀] pr ...) b)
(bind e₀ (λ (v₀) (go-on (pr ...) b)))]))