From a71ee3e46a55bb98c2ea76c88e2617ee38d1dfc6 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Mon, 20 Jun 2016 15:17:26 -0400 Subject: [PATCH] implement rec-iso and exist with typed-lang-builder --- tapl/tests/exist-tests.rkt | 79 ++++++++++++------------ tapl/tests/stlc+rec-iso-tests.rkt | 4 +- tapl/typed-lang-builder/exist.rkt | 75 ++++++++++++++++++++++ tapl/typed-lang-builder/stlc+rec-iso.rkt | 51 +++++++++++++++ 4 files changed, 169 insertions(+), 40 deletions(-) create mode 100644 tapl/typed-lang-builder/exist.rkt create mode 100644 tapl/typed-lang-builder/stlc+rec-iso.rkt diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt index 3913a7b..a0782c0 100644 --- a/tapl/tests/exist-tests.rkt +++ b/tapl/tests/exist-tests.rkt @@ -1,4 +1,4 @@ -#lang s-exp "../exist.rkt" +#lang s-exp "../typed-lang-builder/exist.rkt" (require "rackunit-typechecking.rkt") (check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X)) @@ -18,12 +18,12 @@ : (∃ (X) (∃ (X) (→ X X Int)))) ; cant typecheck bc X has local scope, and no X elimination form -;(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) x) : X) +;(check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] x) : X) (check-type 0 : Int) (check-type (+ 0 1) : Int ⇒ 1) (check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1) -(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) (+ x 1))) ; can't use as Int +(typecheck-fail (open [x <= (pack (Int 0) as (∃ (X) X)) with] (+ x 1))) ; can't use as Int (check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y))) (check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z))) @@ -32,7 +32,7 @@ : (∃ (X) X) ⇒ #t) ;; example where the two binding X's are conflated, see exist.rkt for explanation -(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) ((λ ([y : X]) 1) x)) +(check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] ((λ ([y : X]) 1) x)) : Int ⇒ 1) (check-type @@ -45,15 +45,15 @@ as (∃ (X) (× [a : X] [f : (→ X Int)])))) (check-type p4 : (∃ (X) (× [a : X] [f : (→ X Int)]))) -(check-not-type (open ([(X x) <= p4]) (proj x a)) : Int) ; type is X, not Int +(check-not-type (open [x <= p4 with X] (proj x a)) : Int) ; type is X, not Int ; type is (→ X X), not (→ Int Int) -(check-not-type (open ([(X x) <= p4]) (proj x f)) : (→ Int Int)) -(typecheck-fail (open ([(X x) <= p4]) (+ 1 (proj x a)))) -(check-type (open ([(X x) <= p4]) ((proj x f) (proj x a))) : Int ⇒ 6) -(check-type (open ([(X x) <= p4]) ((λ ([y : X]) ((proj x f) y)) (proj x a))) : Int ⇒ 6) +(check-not-type (open [x <= p4 with X] (proj x f)) : (→ Int Int)) +(typecheck-fail (open [x <= p4 with X] (+ 1 (proj x a)))) +(check-type (open [x <= p4 with X] ((proj x f) (proj x a))) : Int ⇒ 6) +(check-type (open [x <= p4 with X] ((λ ([y : X]) ((proj x f) y)) (proj x a))) : Int ⇒ 6) (check-type - (open ([(X x) <= (pack (Int 0) as (∃ (Y) Y))]) + (open [x <= (pack (Int 0) as (∃ (Y) Y)) with X] ((λ ([y : X]) 1) x)) : Int ⇒ 1) @@ -87,20 +87,20 @@ [get : (→ Counter Int)] [inc : (→ Counter Counter)]))) (typecheck-fail - (open ([(Counter counter) <= counterADT]) + (open [counter <= counterADT with Counter] (+ (proj counter new) 1)) - #:with-msg (expected "Int, Int" #:given "Counter, Int")) + #:with-msg "expected: +Int, Int\n *given: +Counter, Int\n *expressions: +\\(proj counter new\\), 1") (typecheck-fail - (open ([(Counter counter) <= counterADT]) + (open [counter <= counterADT with Counter] ((λ ([x : Int]) x) (proj counter new))) - #:with-msg (expected "Int" #:given "Counter")) + #:with-msg "expected: +Int\n *given: +Counter\n *expressions: +\\(proj counter new\\)") (check-type - (open ([(Counter counter) <= counterADT]) + (open [counter <= counterADT with Counter] ((proj counter get) ((proj counter inc) (proj counter new)))) : Int ⇒ 2) (check-type - (open ([(Counter counter) <= counterADT]) + (open [counter <= counterADT with Counter] (let ([inc (proj counter inc)] [get (proj counter get)]) (let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))]) @@ -108,7 +108,7 @@ : Int ⇒ 4) (check-type - (open ([(Counter counter) <= counterADT]) + (open [counter <= counterADT with Counter] (let ([get (proj counter get)] [inc (proj counter inc)] [new (λ () (proj counter new))]) @@ -120,15 +120,16 @@ (λ ([n : Int]) (and (not (zero? n)) (is-even? (sub1 n))))]) - (open ([(FlipFlop flipflop) <= - (pack (Counter (tup [new = (new)] - [read = (λ ([c : Counter]) (is-even? (get c)))] - [toggle = (λ ([c : Counter]) (inc c))] - [reset = (λ ([c : Counter]) (new))])) - as (∃ (FlipFlop) (× [new : FlipFlop] - [read : (→ FlipFlop Bool)] - [toggle : (→ FlipFlop FlipFlop)] - [reset : (→ FlipFlop FlipFlop)])))]) + (open [flipflop <= + (pack (Counter (tup [new = (new)] + [read = (λ ([c : Counter]) (is-even? (get c)))] + [toggle = (λ ([c : Counter]) (inc c))] + [reset = (λ ([c : Counter]) (new))])) + as (∃ (FlipFlop) (× [new : FlipFlop] + [read : (→ FlipFlop Bool)] + [toggle : (→ FlipFlop FlipFlop)] + [reset : (→ FlipFlop FlipFlop)]))) + with FlipFlop] (let ([read (proj flipflop read)] [togg (proj flipflop toggle)]) (read (togg (togg (togg (togg (proj flipflop new))))))))))) @@ -149,7 +150,7 @@ ;; same as above, but with different internal counter representation (check-type - (open ([(Counter counter) <= counterADT2]) + (open [counter <= counterADT2 with Counter] (let ([get (proj counter get)] [inc (proj counter inc)] [new (λ () (proj counter new))]) @@ -161,15 +162,17 @@ (λ ([n : Int]) (and (not (zero? n)) (is-even? (sub1 n))))]) - (open ([(FlipFlop flipflop) <= - (pack (Counter (tup [new = (new)] - [read = (λ ([c : Counter]) (is-even? (get c)))] - [toggle = (λ ([c : Counter]) (inc c))] - [reset = (λ ([c : Counter]) (new))])) - as (∃ (FlipFlop) (× [new : FlipFlop] - [read : (→ FlipFlop Bool)] - [toggle : (→ FlipFlop FlipFlop)] - [reset : (→ FlipFlop FlipFlop)])))]) + (open [flipflop <= + (pack (Counter (tup [new = (new)] + [read = (λ ([c : Counter]) (is-even? (get c)))] + [toggle = (λ ([c : Counter]) (inc c))] + [reset = (λ ([c : Counter]) (new))])) + as (∃ (FlipFlop) (× [new : FlipFlop] + [read : (→ FlipFlop Bool)] + [toggle : (→ FlipFlop FlipFlop)] + [reset : (→ FlipFlop FlipFlop)]))) + with + FlipFlop] (let ([read (proj flipflop read)] [togg (proj flipflop toggle)]) (read (togg (togg (togg (togg (proj flipflop new))))))))))) @@ -181,9 +184,9 @@ #:with-msg "Expected ∃ type, got: Int") (typecheck-fail - (open ([(X x) <= 2]) 3) + (open [x <= 2 with X] 3) #:with-msg - "Expected expression 2 to have ∃ type, got: Int") + "Expected ∃ type, got: Int") ;; previous tets from stlc+reco+var-tests.rkt --------------------------------- ;; define-type-alias diff --git a/tapl/tests/stlc+rec-iso-tests.rkt b/tapl/tests/stlc+rec-iso-tests.rkt index 905607e..5f654d2 100644 --- a/tapl/tests/stlc+rec-iso-tests.rkt +++ b/tapl/tests/stlc+rec-iso-tests.rkt @@ -1,4 +1,4 @@ -#lang s-exp "../stlc+rec-iso.rkt" +#lang s-exp "../typed-lang-builder/stlc+rec-iso.rkt" (require "rackunit-typechecking.rkt") (define-type-alias IntList (μ (X) (∨ [nil : Unit] [cons : (× Int X)]))) @@ -157,7 +157,7 @@ (typecheck-fail (proj 1 2) #:with-msg - "Expected expression 1 to have × type, got: Int") + "Expected × type, got: Int") ;; ext-stlc.rkt tests --------------------------------------------------------- ;; should still pass diff --git a/tapl/typed-lang-builder/exist.rkt b/tapl/typed-lang-builder/exist.rkt new file mode 100644 index 0000000..ee48c9a --- /dev/null +++ b/tapl/typed-lang-builder/exist.rkt @@ -0,0 +1,75 @@ +#lang macrotypes/tapl/typed-lang-builder +(extends "stlc+reco+var.rkt") +(reuse #:from "stlc+rec-iso.rkt") ; want type=?, but only need to load current-type=? + +;; existential types +;; Types: +;; - types from stlc+reco+var.rkt +;; - ∃ +;; Terms: +;; - terms from stlc+reco+var.rkt +;; - pack and open +;; Other: type=? from stlc+rec-iso.rkt + + +(define-type-constructor ∃ #:bvs = 1) + +(define-typed-syntax pack + [(pack (τ:type e) as ∃τ:type) ▶ + [#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm] + [⊢ [[e ≫ e-] ⇒ (: τ_e)]] + [#:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))] + -------- + [⊢ [[_ ≫ e-] ⇒ (: ∃τ.norm)]]]) + +(define-typed-syntax open #:datum-literals (<= with) + [(open [x:id <= e_packed with X:id] e) + ▶ + ;; The subst below appears to be a hack, but it's not really. + ;; It's the (TaPL) type rule itself that is fast and loose. + ;; Leveraging the macro system's management of binding reveals this. + ;; + ;; Specifically, here is the TaPL Unpack type rule, fig24-1, p366: + ;; Γ ⊢ e_packed : {∃X,τ_body} + ;; Γ,X,x:τ_body ⊢ e : τ_e + ;; ------------------------------ + ;; Γ ⊢ (open [x <= e_packed with X] e) : τ_e + ;; + ;; There's *two* separate binders, the ∃ and the let, + ;; which the rule conflates. + ;; + ;; Here's the rule rewritten to distinguish the two binding positions: + ;; Γ ⊢ e_packed : {∃X_1,τ_body} + ;; Γ,X_???,x:τ_body ⊢ e : τ_e + ;; ------------------------------ + ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e + ;; + ;; The X_1 binds references to X in T_12. + ;; The X_2 binds references to X in t_2. + ;; What should the X_??? be? + ;; + ;; A first guess might be to replace X_??? with both X_1 and X_2, + ;; so all the potentially referenced type vars are bound. + ;; Γ ⊢ e_packed : {∃X_1,τ_body} + ;; Γ,X_1,X_2,x:τ_body ⊢ e : τ_e + ;; ------------------------------ + ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e + ;; + ;; But this example demonstrates that the rule above doesnt work: + ;; (open [x <= (pack (Int 0) as (∃ (X_1) X_1)) with X_2] + ;; ((λ ([y : X_2]) y) x) + ;; Here, x has type X_1, y has type X_2, but they should be the same thing, + ;; so we need to replace all X_1's with X_2 + ;; + ;; Here's the fixed rule, which is implemented here + ;; + ;; Γ ⊢ e_packed : {∃X_1,τ_body} + ;; Γ,X_2:#%type,x:[X_2/X_1]τ_body ⊢ e : τ_e + ;; ------------------------------ + ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e + ;; + [⊢ [[e_packed ≫ e_packed-] ⇒ (: (~∃ (Y) τ_body))]] + [#:with τ_x (subst #'X #'Y #'τ_body)] + [([X : #%type ≫ X-]) ([x : τ_x ≫ x-]) ⊢ [[e ≫ e-] ⇒ (: τ_e)]] + -------- + [⊢ [[_ ≫ (let- ([x- e_packed-]) e-)] ⇒ (: τ_e)]]]) diff --git a/tapl/typed-lang-builder/stlc+rec-iso.rkt b/tapl/typed-lang-builder/stlc+rec-iso.rkt new file mode 100644 index 0000000..e887097 --- /dev/null +++ b/tapl/typed-lang-builder/stlc+rec-iso.rkt @@ -0,0 +1,51 @@ +#lang macrotypes/tapl/typed-lang-builder +(extends "stlc+tup.rkt") +(reuse ∨ var case define-type-alias define #:from "stlc+reco+var.rkt") + +;; stlc + (iso) recursive types +;; Types: +;; - types from stlc+tup.rkt +;; - also ∨ from stlc+reco+var +;; - μ +;; Terms: +;; - terms from stlc+tup.rkt +;; - also var and case from stlc+reco+var +;; - fld, unfld +;; Other: +;; - extend type=? to handle lambdas + +(define-type-constructor μ #:bvs = 1) + +(begin-for-syntax + (define stlc:type=? (current-type=?)) + ;; extend to handle μ, ie lambdas + (define (type=? τ1 τ2) +; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1)) +; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2)) + (syntax-parse (list τ1 τ2) + ;; alternative #4: use old type=? for everything except lambda + [(((~literal #%plain-lambda) (x:id ...) t1 ...) + ((~literal #%plain-lambda) (y:id ...) t2 ...)) + (and (stx-length=? #'(x ...) #'(y ...)) + (stx-length=? #'(t1 ...) #'(t2 ...)) + (stx-andmap + (λ (t1 t2) + ((current-type=?) (substs #'(y ...) #'(x ...) t1) t2)) + #'(t1 ...) #'(t2 ...)))] + [_ (stlc:type=? τ1 τ2)])) + (current-type=? type=?) + (current-typecheck-relation type=?)) + +(define-typed-syntax unfld + [(unfld τ:type-ann e) ▶ + [#:with (~μ* (tv) τ_body) #'τ.norm] + [⊢ [[e ≫ e-] ⇐ (: τ.norm)]] + -------- + [⊢ [[_ ≫ e-] ⇒ (: #,(subst #'τ.norm #'tv #'τ_body))]]]) +(define-typed-syntax fld + [(fld τ:type-ann e) ▶ + [#:with (~μ* (tv) τ_body) #'τ.norm] + [#:with τ_e (subst #'τ.norm #'tv #'τ_body)] + [⊢ [[e ≫ e-] ⇐ (: τ_e)]] + -------- + [⊢ [[_ ≫ e-] ⇒ (: τ.norm)]]])