commit a71ee3e46a55bb98c2ea76c88e2617ee38d1dfc6
parent c8ff0afa0255c9fd620861a4aa66c0d0a43b36e5
Author: AlexKnauth <alexander@knauth.org>
Date: Mon, 20 Jun 2016 15:17:26 -0400
implement rec-iso and exist with typed-lang-builder
Diffstat:
4 files changed, 169 insertions(+), 40 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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)]]])
