Skip to content

Instantly share code, notes, and snippets.

@zeptometer
Last active February 11, 2018 08:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save zeptometer/921cf519197abe147ba23197f3d251da to your computer and use it in GitHub Desktop.
Save zeptometer/921cf519197abe147ba23197f3d251da to your computer and use it in GitHub Desktop.
;; Intentional normalization by evaluation for untyped lambda caluclus
;; Based on Sam Lindley's talk at metaprog2016
;; http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
;; object lang
;; M ::= x
;; | (fn x M)
;; | (M N)
(defun econs (key val env)
(acons key val env))
(defun lookup (key env)
(let ((result (assoc key env)))
(if result
(cdr result)
key)))
(defparameter idenv nil)
;; main
(defun make-app (term1 term2)
(cond ((functionp term1) (funcall term1 term2))
(t `(,term1 ,term2))))
(defun evaluate (term env)
(cond ((symbolp term) (lookup term env))
((eq (car term) 'fn)
(lambda (x)
(evaluate (caddr term) (econs (cadr term) x env))))
(t (make-app (evaluate (car term) env)
(evaluate (cadr term) env)))))
(defun reify (obj)
(cond ((functionp obj) (let ((sym (gensym)))
`(fn ,sym ,(reify (make-app obj sym)))))
(t obj)))
(defun norm (term)
(reify (evaluate term idenv)))
;; example
(defparameter sixteen (let ((two '(fn f (fn x (f (f x))))))
`(,two (,two ,two))))
(norm sixteen) ; => (fn %x (fn %y (%x (%x .... (%x y)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment