Skip to content

Instantly share code, notes, and snippets.

@nyuichi
Last active February 13, 2018 03:23
Show Gist options
  • Save nyuichi/4ab710f0373dee6b32a7f333c20648f8 to your computer and use it in GitHub Desktop.
Save nyuichi/4ab710f0373dee6b32a7f333c20648f8 to your computer and use it in GitHub Desktop.
untyped normalization by evaluation
(use r7rs)
(define uniq
(let ((n 0))
(lambda ()
(set! n (+ n 1))
(string->symbol (string-append "$" (number->string n))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; - Operational aspects of untyped normalization by evaluation, K. Aehlig et al, MSCS 2003.
;;; - Normalization by evaluation, Sam Lindley, http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; object language
;; e ::= x
;; | c
;; | (lambda (x) e)
;; | (e e)
;; meta language
;; E ::= (NE . e)
;; | (ABS . f)
; e -> E
(define (reflect e)
`(NE . ,e))
; E -> e
(define (reify e)
(let ((tag (car e)) (e (cdr e)))
(case tag
((ABS) (let ((x (uniq)))
`(lambda (,x) ,(reify (e (reflect x))))))
((NE) e))))
; E * E -> E
(define (app f x)
(let ((tag (car f)) (f (cdr f)))
(case tag
((ABS) (f x))
((NE) (reflect `(,f ,(reify x)))))))
; (E -> E) -> E
(define (lam f)
`(ABS . ,f))
; e -> E
(define (interpret e env)
(cond
((symbol? e)
(let ((v (assq e env)))
(if v (cdr v) (reflect e))))
((not (pair? e))
(reflect e))
((eq? 'lambda (car e))
(let ((v (caadr e)) (e (caddr e)))
(lam (lambda (x) (interpret e `((,v . ,x) . ,env))))))
(else
(let ((f (interpret (car e) env))
(x (interpret (cadr e) env)))
(app f x)))))
(define (nbe e env)
(reify (interpret e env)))
(nbe '((lambda (y) y) x) '()) ; => x
(nbe '(lambda (x) ((lambda (z) z) x)) '()) ; => (lambda ($2) $2)
(nbe '(lambda (x) (lambda (y) (x y))) '()) ; => (lambda ($3) (lambda ($4) ($3 $4)))
(nbe '((lambda (x) ((lambda (z) z) x)) y) `((y . ,(reflect 1)))) ; => 1
(nbe '((+ 1) 2)
`((+ . ,(lam (lambda (x)
(lam (lambda (y)
(reflect (+ (reify x) (reify y)))))))))) ; => 3
; w/ side effects
(nbe '(lambda (x) (print 42))
`((print . ,(lam (lambda (x)
(display (reify x))
(newline)
(reflect #f)))))) ; => (lambda ($5) #f) console: 42
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; One-pass CPS transformation is just a normalization-by-evaluation interpreter.
;;; - Ordinary and one-pass CPS transformation, Oleg Kiselyov, http://okmij.org/ftp/tagless-final/cookbook.html#CPS
;;; - Representing control: a study of the CPS transformation, O. Danvy, A. Filinski, MSCS'92.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; [x] --> \k.k@x
;; [\x.M] --> \k.k@\x.[M]
;; [M@N] --> \k.[M]@\m.[N]@\n.(m@n)@k
; E -> E
(define (cps-var x)
(lam (lambda (k) (app k x))))
; (E -> E) -> E
(define (cps-lam f)
(lam (lambda (k)
(app k (lam f)))))
; E * E -> E
(define (cps-app f x)
(lam (lambda (k)
(app f (lam (lambda (m)
(app x (lam (lambda (n)
(app (app m n) k))))))))))
; e -> E
(define (cps-interpret e env)
(cond
((symbol? e)
(cps-var (cdr (assq e env))))
((eq? 'lambda (car e))
(let ((v (caadr e)) (e (caddr e)))
(cps-lam (lambda (x) (cps-interpret e `((,v . ,x) . ,env))))))
(else
(let ((f (cps-interpret (car e) env))
(x (cps-interpret (cadr e) env)))
(cps-app f x)))))
(define (cps-nbe e env)
(reify (cps-interpret e env)))
(cps-nbe '(lambda (x) x) '())
(cps-nbe '(lambda (f)
(lambda (x)
(lambda (y)
((f y) x))))
'())
;; =>
;; (lambda ($15)
;; ($15 (lambda ($16)
;; (lambda ($17)
;; ($17 (lambda ($18)
;; (lambda ($19)
;; ($19 (lambda ($20)
;; (lambda ($21)
;; (($16 $20) (lambda ($22)
;; (($22 $18) $21)))))))))))))
(cps-nbe '(call/cc (lambda (f)
((f x) y)))
`((call/cc . ,(lam (lambda (f)
(lam (lambda (k)
(app (app f (lam (lambda (x)
(lam (lambda (m)
(app k x))))))
k))))))
(x . ,(reflect 'x))
(y . ,(reflect 'y))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment