finish exist.rkt
This commit is contained in:
Stephen Chang
parent
e678912c2c
commit
b0a8d192ef
|
|
@ -1,12 +1,95 @@
|
|||
#lang racket/base
|
||||
(require "typecheck.rkt")
|
||||
(require (except-in "stlc+reco+var.rkt" #%app λ)
|
||||
(prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ)))
|
||||
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
|
||||
(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ))
|
||||
|
||||
(require (except-in "stlc+reco+var.rkt" #%app λ let type=?)
|
||||
(prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let type=?))
|
||||
(prefix-in sysf: (only-in "sysf.rkt" type=?)))
|
||||
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])
|
||||
(for-syntax type=?))
|
||||
(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let
|
||||
(for-syntax stlc:type=?)))
|
||||
(provide ∃ pack open)
|
||||
|
||||
;; existential types
|
||||
;; combine type=? from sysf (for lam, ie ∃) and stlc+reco+var (for strings)
|
||||
;; Types:
|
||||
;; - types from stlc+reco+var.rkt
|
||||
;; - ∃
|
||||
;; Terms:
|
||||
;; - terms from stlc+reco+var.rkt
|
||||
;; - pack and open
|
||||
|
||||
(begin-for-syntax
|
||||
(define (type=? t1 t2)
|
||||
(or (stlc:type=? t1 t2)
|
||||
(sysf:type=? t1 t2)))
|
||||
(current-type=? type=?)
|
||||
(current-typecheck-relation type=?))
|
||||
|
||||
;; TODO: disambiguate expanded representation of ∃, ok to use lambda in this calculus
|
||||
(provide ∃)
|
||||
(define-syntax (∃ stx)
|
||||
(syntax-parse stx
|
||||
[(_ (tv:id) body)
|
||||
(syntax/loc stx (#%plain-lambda (tv) body))]))
|
||||
|
||||
(define-syntax (pack stx)
|
||||
(syntax-parse stx
|
||||
[(_ (τ:type e) as ∃τ:type)
|
||||
#:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
|
||||
#:with [e- τ_e] (infer+erase #'e)
|
||||
#:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
|
||||
(⊢ #'e- #'∃τ)]))
|
||||
|
||||
; TODO: the colon syntax might be misleading, since tv is not the type of x
|
||||
(define-syntax (open stx)
|
||||
(syntax-parse stx #:datum-literals (<=)
|
||||
[(_ ([(tv:id x:id) <= e_packed]) e)
|
||||
#:with [e_packed- τ_packed] (infer+erase #'e_packed)
|
||||
#:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
|
||||
;; 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:
|
||||
;; Γ ⊢ t_1 : {∃X,T_12}
|
||||
;; Γ,X,x:T_12 ⊢ t_2 : T_2
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X,x}=t_1 in t_2 : T_2
|
||||
;;
|
||||
;; There's *two* separate binders, the ∃ and the let,
|
||||
;; which the rule conflates.
|
||||
;;
|
||||
;; Here's the rule rewritten to distinguish the two binding positions:
|
||||
;; Γ ⊢ t_1 : {∃X_1,T_12}
|
||||
;; Γ,X_???,x:T_12 ⊢ t_2 : T_2
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
|
||||
;;
|
||||
;; 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.
|
||||
;; Γ ⊢ t_1 : {∃X_1,T_12}
|
||||
;; Γ,X_1,X_2,x:T_12 ⊢ t_2 : T_2
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
|
||||
;;
|
||||
;; But this example demonstrates that the rule above doesnt work:
|
||||
;; (open ([x : X_2 (pack (Int 0) as (∃ (X_1) X_1))])
|
||||
;; ((λ ([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
|
||||
;;
|
||||
;; Γ ⊢ t_1 : {∃X_1,T_12}
|
||||
;; Γ,X_2,x:[X_2/X_1]T_12 ⊢ t_2 : T_2
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
|
||||
;;
|
||||
#:with [tvs- (x-) (e-) (τ_e)]
|
||||
(infer #'(e) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)])
|
||||
#:tvs #'(tv))
|
||||
(⊢ #'(let ([x- e_packed-]) e-) #'τ_e)]))
|
||||
|
|
@ -1,6 +1,163 @@
|
|||
#lang s-exp "../exist.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X))
|
||||
(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y))
|
||||
(typecheck-fail (pack (Int 0) as (∃ (X) Y)))
|
||||
(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
|
||||
(typecheck-fail (pack (Int #t) as (∃ (X) X)))
|
||||
|
||||
; 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 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
|
||||
|
||||
(check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y)))
|
||||
(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z)))
|
||||
: (∃ (X) X) ⇒ 0)
|
||||
(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z)))
|
||||
: (∃ (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))
|
||||
: Int ⇒ 1)
|
||||
|
||||
(check-type
|
||||
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [: "a" X] [: "f" (→ X X)])))
|
||||
: (∃ (X) (× [: "a" X] [: "f" (→ X X)])))
|
||||
|
||||
(define p4
|
||||
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
|
||||
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
|
||||
; 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-type
|
||||
(open ([(X x) <= (pack (Int 0) as (∃ (Y) Y))])
|
||||
((λ ([y : X]) 1) x))
|
||||
: Int ⇒ 1)
|
||||
|
||||
(check-type
|
||||
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [: "a" Int] [: "f" (→ Int Int)])))
|
||||
: (∃ (X) (× [: "a" Int] [: "f" (→ Int Int)])))
|
||||
|
||||
(typecheck-fail
|
||||
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [: "a" Int] [: "f" (→ Bool Int)]))))
|
||||
|
||||
(typecheck-fail
|
||||
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [: "a" X] [: "f" (→ X Bool)]))))
|
||||
|
||||
(check-type
|
||||
(pack (Bool (tup ["a" = #t] ["f" = (λ ([x : Bool]) (if x 1 2))]))
|
||||
as (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
|
||||
: (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
|
||||
|
||||
(define counterADT
|
||||
(pack (Int (tup ["new" = 1]
|
||||
["get" = (λ ([i : Int]) i)]
|
||||
["inc" = (λ ([i : Int]) (+ i 1))]))
|
||||
as (∃ (Counter) (× [: "new" Counter]
|
||||
[: "get" (→ Counter Int)]
|
||||
[: "inc" (→ Counter Counter)]))))
|
||||
(check-type counterADT :
|
||||
(∃ (Counter) (× [: "new" Counter]
|
||||
[: "get" (→ Counter Int)]
|
||||
[: "inc" (→ Counter Counter)])))
|
||||
(check-type
|
||||
(open ([(Counter counter) <= counterADT])
|
||||
((proj counter "get") ((proj counter "inc") (proj counter "new"))))
|
||||
: Int ⇒ 2)
|
||||
|
||||
(check-type
|
||||
(open ([(Counter counter) <= counterADT])
|
||||
(let ([inc (proj counter "inc")]
|
||||
[get (proj counter "get")])
|
||||
(let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))])
|
||||
(get (add3 (proj counter "new"))))))
|
||||
: Int ⇒ 4)
|
||||
|
||||
(check-type
|
||||
(open ([(Counter counter) <= counterADT])
|
||||
(let ([get (proj counter "get")]
|
||||
[inc (proj counter "inc")]
|
||||
[new (λ () (proj counter "new"))])
|
||||
(letrec ([(is-even? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(or (zero? n)
|
||||
(is-odd? (sub1 n))))]
|
||||
[(is-odd? : (→ Int Bool))
|
||||
(λ ([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)])))])
|
||||
(let ([read (proj flipflop "read")]
|
||||
[togg (proj flipflop "toggle")])
|
||||
(read (togg (togg (togg (togg (proj flipflop "new")))))))))))
|
||||
: Bool ⇒ #f)
|
||||
|
||||
(define counterADT2
|
||||
(pack ((× [: "x" Int])
|
||||
(tup ["new" = (tup ["x" = 1])]
|
||||
["get" = (λ ([i : (× [: "x" Int])]) (proj i "x"))]
|
||||
["inc" = (λ ([i : (× [: "x" Int])]) (tup ["x" = (+ 1 (proj i "x"))]))]))
|
||||
as (∃ (Counter) (× [: "new" Counter]
|
||||
[: "get" (→ Counter Int)]
|
||||
[: "inc" (→ Counter Counter)]))))
|
||||
(check-type counterADT2 :
|
||||
(∃ (Counter) (× [: "new" Counter]
|
||||
[: "get" (→ Counter Int)]
|
||||
[: "inc" (→ Counter Counter)])))
|
||||
|
||||
;; same as above, but with different internal counter representation
|
||||
(check-type
|
||||
(open ([(Counter counter) <= counterADT2])
|
||||
(let ([get (proj counter "get")]
|
||||
[inc (proj counter "inc")]
|
||||
[new (λ () (proj counter "new"))])
|
||||
(letrec ([(is-even? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(or (zero? n)
|
||||
(is-odd? (sub1 n))))]
|
||||
[(is-odd? : (→ Int Bool))
|
||||
(λ ([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)])))])
|
||||
(let ([read (proj flipflop "read")]
|
||||
[togg (proj flipflop "toggle")])
|
||||
(read (togg (togg (togg (togg (proj flipflop "new")))))))))))
|
||||
: Bool ⇒ #f)
|
||||
|
||||
;; previous tets from stlc+reco+var-tests.rkt ---------------------------------
|
||||
;; define-type-alias
|
||||
(define-type-alias Integer Int)
|
||||
(define-type-alias ArithBinOp (→ Int Int Int))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,6 @@
|
|||
#lang racket
|
||||
|
||||
;; stlc and extensions
|
||||
(require "stlc-tests.rkt")
|
||||
(require "stlc+lit-tests.rkt")
|
||||
(require "ext-stlc-tests.rkt")
|
||||
|
|
@ -9,10 +11,15 @@
|
|||
|
||||
(require "stlc+rec-iso-tests.rkt")
|
||||
|
||||
(require "exist-tests.rkt")
|
||||
|
||||
;; subtyping
|
||||
(require "stlc+sub-tests.rkt")
|
||||
(require "stlc+reco+sub-tests.rkt")
|
||||
|
||||
;; system F
|
||||
(require "sysf-tests.rkt")
|
||||
(require "exist-tests.rkt")
|
||||
|
||||
;; F_omega
|
||||
(require "fomega-tests.rkt")
|
||||
(require "fomega2-tests.rkt")
|
||||
|
|
@ -167,11 +167,32 @@
|
|||
(define (infers+erase es)
|
||||
(stx-map infer+erase es))
|
||||
;; infers and erases types in an expression, in the context of given type vars
|
||||
(define (infer/tvs+erase e [tvs #'()])
|
||||
(define (infer/tvs+erase e tvs)
|
||||
(syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
|
||||
[(lam tvs+ (#%expression e+))
|
||||
(list #'tvs+ #'e+ (syntax-local-introduce (typeof #'e+)))]))
|
||||
|
||||
(define (infer es #:ctx [ctx null] #:tvs [tvs null])
|
||||
(syntax-parse ctx #:datum-literals (:)
|
||||
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
|
||||
; #:with (x ...) #'(b.x ...)
|
||||
; #:with (τ ...) #'(b.τ ...)
|
||||
#:with (e ...) es
|
||||
#:with
|
||||
((~literal #%plain-lambda) tvs+
|
||||
((~literal #%expression)
|
||||
((~literal #%plain-lambda) xs+
|
||||
((~literal letrec-syntaxes+values) stxs1 ()
|
||||
((~literal letrec-syntaxes+values) stxs2 ()
|
||||
((~literal #%expression) e+) ...)))))
|
||||
(expand/df
|
||||
#`(λ #,tvs
|
||||
(λ (x ...)
|
||||
(let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
|
||||
(#%expression e) ...))))
|
||||
(list #'tvs+ #'xs+ #'(e+ ...) (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
|
||||
[([x τ] ...) (infer+erase es #:ctx #'([x : τ] ...) #:tvs tvs)]))
|
||||
|
||||
(define current-typecheck-relation (make-parameter #f))
|
||||
(define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
|
||||
(define (typechecks? τs1 τs2)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user