(module section-4-typed-lump-embedding mzscheme (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2)) (planet "gui.ss" ("robby" "redex.plt" 2)) (planet "subst.ss" ("robby" "redex.plt" 2)) (lib "plt-match.ss")) ;; ============================================================ ;; THE Scheme<->ML embedding example calculus ;; (really embedding untyped cbv LC and simply-typed cbv LC) ;; ------------------------------------------------------------ ;; LANGUAGE GRAMMARS (define mm (language (m:e (m:e m:e) x (lambda (x : m:ty) m:e) (op m:e m:e) number (ifzero m:e m:e m:e) (M1M2 m:ty m2:ty m2:e)) (m:v (lambda (x : m:ty) m:e) number (side-condition (M1M2 L1 m2:ty m2:v_1) (not (match (term m2:v_1) [`(M2M1 ,_ L1 ,v) #t] [_ #f])))) (op + -) (m:ty num (m:ty -> m:ty) L1) (mc (hole m) (mc m:e) (m:v mc) (op mc m:e) (op m:v mc) (ifzero mc m:e m:e) (M1M2 m:ty m2:ty m2c)) ;; ml (m2:e (m2:e m2:e) x (lambda (x : m2:ty) m2:e) (op m2:e m2:e) number (ifzero m2:e m2:e m2:e) (M2M1 m2:ty m:ty m:e)) (m2:v (lambda (x : m2:ty) m2:e) number (side-condition (M2M1 L2 m:ty m:v_1) (not (match (term m:v_1) [`(M1M2 ,_ L2 ,v) #t] [_ #f])))) (m2:ty num (m2:ty -> m2:ty) L2) (m2c (hole m2) (m2c m2:e) (m2:v m2c) (op m2c m2:e) (op m2:v m2c) (ifzero m2c m2:e m2:e) (M2M1 m2:ty m:ty mc)) (x (variable-except lambda M1M2 M2M1 -> num L1 L2 ifzero + -)))) ;; ------------------------------------------------------------ ;; DYNAMIC SEMANTICS (define m1-reductions (list ;; beta (reduction mm (in-named-hole m mc_1 ((lambda (x_a : m:ty) m:e_b) m:v_a)) (term (in-hole mc_1 ,(substitute (term x_a) (term m:v_a) (term m:e_b))))) ;; sum (reduction mm (in-named-hole m mc_1 (+ number_1 number_2)) (term (in-hole mc_1 ,(+ (term number_1) (term number_2))))) (reduction mm (in-named-hole m mc_1 (- number_1 number_2)) (term (in-hole mc_1 ,(max (- (term number_1) (term number_2)) 0)))) ;; ifzero (reduction mm (in-named-hole m mc_1 (ifzero number_1 m:e_1 m:e_2)) (cond [(eqv? (term number_1) 0) (term (in-hole mc_1 m:e_1))] [else (term (in-hole mc_1 m:e_2))])) ;; mapping (reduction mm (side-condition (in-named-hole m mc_1 (M1M2 m:ty_1 L2 (M2M1 L2 m:ty_1 m:v_1))) (not (equal? (term m:ty_1) 'L1))) (term (in-hole mc_1 m:v_1))) (reduction mm (side-condition (in-named-hole m mc_1 (M1M2 m:ty_1 L2 (M2M1 L2 m:ty_2 m:v_2))) (and (not (equal? (term m:ty_1) 'L1)) (not (equal? (term m:ty_1) (term m:ty_2))))) (format "Bad conversion (M1M2): can't convert ~s to ~s" (term (M2M1 L2 m:ty_2 m:v_2)) (term m:ty_1))))) (define m2-reductions (list ;; beta (reduction mm (in-named-hole m2 mc_1 ((lambda (x_a : m2:ty) m2:e_b) m2:v_a)) (term (in-hole mc_1 ,(substitute (term x_a) (term m2:v_a) (term m2:e_b))))) ;; sum (reduction mm (in-named-hole m2 mc_1 (+ number_1 number_2)) (term (in-hole mc_1 ,(+ (term number_1) (term number_2))))) (reduction mm (in-named-hole m2 mc_1 (- number_1 number_2)) (term (in-hole mc_1 ,(max (- (term number_1) (term number_2)) 0)))) ;; ifzero (reduction mm (in-named-hole m2 mc_1 (ifzero number_1 m2:e_1 m2:e_2)) (cond [(eqv? (term number_1) 0) (term (in-hole mc_1 m2:e_1))] [else (term (in-hole mc_1 m2:e_2))])) ;; mapping (reduction mm (side-condition (in-named-hole m2 mc_1 (M2M1 m2:ty_1 L1 (M1M2 L1 m2:ty_1 m2:v_1))) (not (equal? (term m2:ty_1) 'L2))) (term (in-hole mc_1 m2:v_1))) (reduction mm (side-condition (in-named-hole m2 mc_1 (M2M1 m2:ty_1 L1 (M1M2 L1 m2:ty_2 m2:v_1))) (and (not (equal? (term m2:ty_1) 'L2)) (not (equal? (term m2:ty_1) (term m2:ty_2))))) (term "Bad conversion (M2M1)")))) (define reductions (append m1-reductions m2-reductions)) ;; ------------------------------------------------------------ ;; TYPE SYSTEM (define op? (language->predicate mm 'op)) ;; m:typeof : m:e env -> m:ty | #f ;; determines the type of an ML program. (define (m:typeof p Γ) (match p [(? string?) 'error] [(? symbol?) (lookup p Γ)] [(? number?) 'num] [`(,e_1 ,e_2) (match (list (m:typeof e_1 Γ) (m:typeof e_2 Γ)) [`((,ty_dom -> ,ty_rng) ,ty_arg) (if (equal? ty_dom ty_arg) ty_rng #f)] [_ #f])] [`(lambda (,x : ,dom_ty) ,e) (let ((rng_ty (m:typeof e (extend Γ x dom_ty)))) (if rng_ty `(,dom_ty -> ,rng_ty) #f))] [`(,(? op?) ,e_1 ,e_2) (match (list (m:typeof e_1 Γ) (m:typeof e_2 Γ)) [`(num num) 'num] [_ #f])] [`(ifzero ,e1 ,e2 ,e3) (let ((t1 (m:typeof e1 Γ)) (t2 (m:typeof e2 Γ)) (t3 (m:typeof e2 Γ))) (if (and (equal? t1 'num) (equal? t2 t3)) t2 #f))] [`(M1M2 ,mty ,m2ty ,m2e) (let ((subty (m2:typeof m2e Γ))) (if (and subty (equal? subty m2ty)) mty #f))])) (define (m2:typeof p Γ) (match p [(? symbol?) (lookup p Γ)] [(? number?) 'num] [`(,e_1 ,e_2) (match (list (m2:typeof e_1 Γ) (m2:typeof e_2 Γ)) [`((,ty_dom -> ,ty_rng) ,ty_arg) (if (equal? ty_dom ty_arg) ty_rng #f)] [_ #f])] [`(lambda (,x : ,dom_ty) ,e) (let ((rng_ty (m2:typeof e (extend Γ x dom_ty)))) (if rng_ty `(,dom_ty -> ,rng_ty) #f))] [`(,(? op?) ,e_1 ,e_2) (match (list (m2:typeof e_1 Γ) (m2:typeof e_2 Γ)) [`(num num) 'num] [_ #f])] [`(ifzero ,e1 ,e2 ,e3) (let ((t1 (m2:typeof e1 Γ)) (t2 (m2:typeof e2 Γ)) (t3 (m2:typeof e2 Γ))) (if (and (equal? t1 'num) (equal? t2 t3)) t2 #f))] [`(M2M1 ,m2ty ,mty ,me) (let ((subty (m:typeof me Γ))) (if (and subty (equal? mty subty)) m2ty #f))])) ;; ------------------------------------------------------------ ;; ENVIRONMENT MANAGEMENT (define empty-set '()) (define (lookup x Γ) (let ((ans (assq x Γ))) (unless ans (error 'lookup "Variable not in environment: ~a" x)) (cadr ans))) (define (extend Γ x v) (cons (list x v) Γ)) ;; ------------------------------------------------------------ ;; MISC. HELPERS (define (truish v) (if v #t #f)) (define (newname x) (string->symbol (symbol->string (gensym x)))) (define substitute (subst [(? symbol?) (variable)] [(? number?) (constant)] [`(lambda (,x : ,ty) ,b) (all-vars (list x)) (build (lambda (vars body) `(lambda (,(car vars) : ,ty) ,body))) (subterm (list x) b)] [`(M1M2 ,ty1 ,ty2 ,e) (all-vars '()) (build (lambda (vars eb) `(M1M2 ,ty1 ,ty2 ,eb))) (subterm '() e)] [`(M2M1 ,ty2 ,ty1 ,e) (all-vars '()) (build (lambda (vars eb) `(M2M1 ,ty2 ,ty1 ,eb))) (subterm '() e)] [`(,(? op? o) ,e1 ,e2) (all-vars '()) (build (lambda (vars e1 e2) `(,o ,e1 ,e2))) (subterm '() e1) (subterm '() e2)] [`(ifzero ,e1 ,e2 ,e3) (all-vars '()) (build (lambda (vars e1 e2 e3) `(ifzero ,e1 ,e2 ,e3))) (subterm '() e1) (subterm '() e2) (subterm '() e3)] [`(,f ,x) (all-vars '()) (build (lambda (vars f x) `(,f ,x))) (subterm '() f) (subterm '() x)])) ;; ------------------------------------------------------------ ;; TEST CODE (define (run p) (let* ([thetype (m:typeof p empty-set)] [initial-term (if thetype p "Type error")]) (traces/pred mm reductions (list initial-term) (λ (x) (let ((newtype (m:typeof x empty-set))) (or (equal? newtype thetype) (eq? newtype 'error))))))) (define (evaluate p) (if (m:typeof p empty-set) (normalize p) "Type error")) (define m:value? (language->predicate mm 'm:v)) (define normalize (λ (p) (normalize* p void))) (define normalize/tell (λ (p) (normalize* p (λ (x) (write x) (newline))))) (define (normalize* p observer) (let loop ((p p)) (observer p) (cond [(m:value? p) p] [else (let ((nexts (reduce reductions p))) (cond [(null? nexts) p] [(null? (cdr nexts)) (loop (car nexts))] [else (error 'normalize "Term ~s reduces multiple ways" p)]))]))) (require-for-syntax (lib "etc.ss")) (define-syntax (tests stx) (syntax-case stx (test) [(_ (test term expected) ...) (with-syntax ([(num ...) (build-list (length (syntax-e #'(term ...))) add1)]) #`(let ((numcases #,(length (syntax-e #'(term ...)))) (numfailed 0)) (let ((fail (lambda (exp result) (set! numfailed (add1 numfailed)) (printf "TEST ~a FAILED :\nTest:\t\t~s\nExpected:\t~s\nReceived:\t~s\n\n" num 'term exp result)))) (with-handlers ([exn:fail? (lambda (exn) (fail 'expected (format "[exception: ~a]" (exn-message exn))))]) (let ((ans (evaluate `term)) (e `expected)) (unless (α-equivalent? ans e) (fail e ans))))) ... (if (= numfailed 0) (printf "Passed all ~a tests.\n" numcases) (printf "Passed ~a out of ~a tests.\n" (- numcases numfailed) numcases))))])) (define (α-equivalent? p1 p2) (define free (gensym)) (define (mt var) free) (define (extend env var depth) (lambda (v) (if (eq? v var) depth (env v)))) (define (m:α-equivalent? p1 p2 depth m1 m2) (match (list p1 p2) [`(,(? symbol?) ,(? symbol?)) (eq? (m1 p1) (m2 p2))] [`(,(? number?) ,(? number?)) (= p1 p2)] [`(,(? string?) ,(? string?)) (string=? p1 p2)] [`((lambda (,x1 : ,ty1) ,b1) (lambda (,x2 : ,ty2) ,b2)) (m:α-equivalent? b1 b2 (add1 depth) (extend m1 x1 depth) (extend m2 x2 depth))] [`((,p1f ,p1a) (,p2f ,p2a)) (and (m:α-equivalent? p1f p2f depth m1 m2) (m:α-equivalent? p1a p2a depth m1 m2))] [`((,(? op? o1) ,p1f ,p1a) (,(? op? o2) ,p2f ,p2a)) (and (eqv? o1 o2) (m:α-equivalent? p1f p2f depth m1 m2) (m:α-equivalent? p1a p2a depth m1 m2))] [`((ifzero ,e11 ,e12 ,e13) (ifzero ,e21 ,e22 ,e23)) (and (m:α-equivalent? e11 e21 depth m1 m2) (m:α-equivalent? e12 e22 depth m1 m2) (m:α-equivalent? e13 e23 depth m1 m2))] [`((M1M2 ,ty11 ,ty12 ,st1) (M1M2 ,ty21 ,ty22 ,st2)) (and (equal? ty11 ty21) (equal? ty12 ty22) (m2:α-equivalent? st1 st2 depth m1 m2))] [_ #f])) (define (m2:α-equivalent? p1 p2 depth m1 m2) (match (list p1 p2) [`(,(? symbol?) ,(? symbol?)) (eq? (m1 p1) (m2 p2))] [`(,(? number?) ,(? number?)) (= p1 p2)] [`(,(? string?) ,(? string?)) (string=? p1 p2)] [`((lambda (,x1 : ,ty1) ,b1) (lambda (,x2 : ,ty2) ,b2)) (m2:α-equivalent? b1 b2 (add1 depth) (extend m1 x1 depth) (extend m2 x2 depth))] [`((,p1f ,p1a) (,p2f ,p2a)) (and (m2:α-equivalent? p1f p2f depth m1 m2) (m2:α-equivalent? p1a p2a depth m1 m2))] [`((,(? op? o1) ,p1f ,p1a) (,(? op? o2) ,p2f ,p2a)) (and (eqv? o1 o2) (m2:α-equivalent? p1f p2f depth m1 m2) (m2:α-equivalent? p1a p2a depth m1 m2))] [`((ifzero ,e11 ,e12 ,e13) (ifzero ,e21 ,e22 ,e23)) (and (m2:α-equivalent? e11 e21 depth m1 m2) (m2:α-equivalent? e12 e22 depth m1 m2) (m2:α-equivalent? e13 e23 depth m1 m2))] [`((M2M1 ,ty12 ,ty11 ,m1t1) (M2M1 ,ty22 ,ty21 ,m1t2)) (and (equal? ty11 ty21) (equal? ty12 ty22) (m:α-equivalent? m1t1 m1t2 depth m1 m2))] [_ #f])) (m:α-equivalent? p1 p2 0 mt mt)) #;(tests (test ((lambda (x : num) x) 4) 4) (test ((lambda (x : (num -> num)) x) (lambda (y : num) y)) (lambda (y : num) y)) (test (+ 5 12) 17) (test (- 12 5) 7) (test (- 5 12) 0) (test (ifzero 0 2 3) 2) (test (ifzero 1 2 3) 3) (test (M1M2 L1 num (+ 5 12)) (M1M2 L1 num 17)) (test (M1M2 L1 num (- 5 12)) (M1M2 L1 num 0)) (test (M1M2 L1 num (ifzero 0 2 3)) (M1M2 L1 num 2)) (test (M1M2 L1 num (ifzero 1 2 3)) (M1M2 L1 num 3)) (test (M1M2 L1 (num -> num) ((lambda (x : (num -> num)) x) 4)) "Type error") (test ((lambda (x : (num -> num)) x) 4) "Type error") (test (M1M2 num L2 (M2M1 L2 num 3)) 3) (test (M1M2 L1 num (M2M1 num L1 (M1M2 L1 num 3))) (M1M2 L1 num 3)) (test (M1M2 (num -> num) L2 (M2M1 L2 num 3)) "Bad conversion") (test (M1M2 L1 (num -> num) (M2M1 (num -> num) L1 (M1M2 L1 num 3))) "Bad conversion")) (define (nontermination-example) ;; P : (L1 -> L1) -> L1 (define P `(lambda (x : (L1 -> L1)) (M1M2 L1 (num -> L2) (lambda (z : num) (M2M1 L2 (L1 -> L1) x))))) ;; U : L1 -> (L1 -> L1) (define U `(lambda (x : L1) (M1M2 (L1 -> L1) L2 ((M2M1 (num -> L2) L1 x) 0)))) (run `((lambda (x : L1) ((,U x) x)) (,P (lambda (x : L1) ((,U x) x)))))) ;; display a GUI with the example reduction sequence (nontermination-example))