commit d7913f775356cd442b686f9548405033fc920e26
parent c5d6bfbf9e1d771040b49134087aaa615cc9be4d
Author: Ben Greenman <types@ccs.neu.edu>
Date: Tue, 13 Oct 2015 12:51:24 -0400
[occurrence] subtyping, normal form, and VERY BASIC filters. Having trouble propogating variables.
Diffstat:
2 files changed, 337 insertions(+), 23 deletions(-)
diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
@@ -21,21 +21,69 @@
[(_ . x) #'(stlc+sub:#%datum . x)])
(define-type-constructor ∪ #:arity >= 1)
-;; TODO disallow recursive ∪
+
+;; -----------------------------------------------------------------------------
+;; --- Union operations
+
+;; Occurrence type operations
+;; These assume that τ is a type in 'normal form'
+(begin-for-syntax
+ ;; True if τ is a union type, otherwise #f
+
+ (define (∪->list τ)
+ ;; Ignore type constructor & the kind
+ ;; (because there are no bound identifiers)
+ (syntax-parse τ
+ [(~∪ τ* ...)
+ (syntax->list #'(τ* ...))]
+ [_
+ (error '∪->list (format "Given non-ambiguous type '~a'" τ))]))
+
+ (define (list->∪ τ*)
+ (τ-eval #`(∪ #,@τ*)))
+
+ (define (type->filter τ)
+ ;; Going to have the same problem here, matching on types
+ ;; (Γ is stored insisde τ)
+ ;; (define Π (get-context τ 'filter))
+ ;; (Π τ))
+ ;; TODO filter properly
+ #'boolean?)
+
+ (define (∖ τ1 τ2)
+ (cond
+ [(∪? τ1)
+ (printf "SETMINUS got an ∪ ~a\n" τ1)
+ (define (not-τ2? τ)
+ (not (typecheck? τ τ2)))
+ (list->∪ (filter not-τ2? (∪->list τ1)))]
+ [else ; do nothing
+ τ1]))
+)
+
+;; -----------------------------------------------------------------------------
+;; --- Normal Form
(begin-for-syntax
(define τ-eval (current-type-eval))
+ (define (τ->symbol τ)
+ (cadr (syntax->datum τ)))
(define (∪-eval τ-stx)
- (syntax-parse τ-stx #:datum-literals (∪)
- [(∪ τ-stx* ...)
- ;; TODO Assumes that each τ is non-∪
- ;; TODO just make a set?
- ;; will that work if we have ∪ inside the ∪ ?
- ;(printf "Syntax prop type is ~a\n" (syntax-property (τ-eval τ) 'type))
+ (syntax-parse (τ-eval τ-stx)
+ [(~∪ τ-stx* ...)
+ ;; Recursively evaluate members
+ (define τ**
+ (for/list ([τ (in-list (syntax->list #'(τ-stx* ...)))])
+ (let ([τ+ (∪-eval τ)])
+ (if (∪? τ+)
+ (∪->list τ+)
+ (list τ+)))))
+ ;; Remove duplicates from the union, sort members
(define τ*
(sort
- (remove-duplicates (syntax->list #'(τ-stx* ...)) (current-type=?))
+ (remove-duplicates (apply append τ**) (current-type=?))
symbol<?
- #:key syntax->datum))
+ #:key τ->symbol)) ;; TODO handle functions & other constructors
+ ;; Check for empty & singleton lists
(define τ
(cond
[(null? τ*)
@@ -51,15 +99,107 @@
(τ-eval τ-stx)]))
(current-type-eval ∪-eval))
+;; -----------------------------------------------------------------------------
+;; --- Subtyping
+;; Problem: matching on normal forms is tricky
+;; (use stlc+reco+sub as an example)
+
;; - subtype U with simple, U with contained
+;; - AMB : t <: (U ... t ...)
+;; - SUB : a<:b => (U a t' ...) <: (U b t' ...)
+;; - EXT : (U t' ...) <: (U t t' ...)
+(begin-for-syntax
+ ;; True if one ordered list (of types) is a subset of another
+ (define (subset? x* y* #:leq [cmp (current-typecheck-relation)])
+ (let loop ([x* x*] [y* y*])
+ (cond
+ [(null? x*) #t]
+ [(null? y*) #f]
+ [(cmp (car x*) (car y*))
+ (loop (cdr x*) (cdr y*))]
+ [else
+ (loop x* (cdr y*))])))
+
+ (define sub? (current-sub?))
+ (define (∪-sub? τ1-stx τ2-stx)
+ (define τ1 ((current-type-eval) τ1-stx))
+ (define τ2 ((current-type-eval) τ2-stx))
+ (match `(,(∪? τ1) ,(∪? τ2))
+ ['(#f #t)
+ ;; AMB : a<:b => a <: (U ... b ...)
+ (for/or ([τ (in-list (∪->list τ2))])
+ (sub? τ1 τ))]
+ ['(#t #t)
+ (define τ1* (∪->list τ1))
+ (define τ2* (∪->list τ2))
+ (match `(,(length τ1*) ,(length τ2*))
+ [`(,L1 ,L2) #:when (< L1 L2)
+ ;; - EXT : (U t' ...) <: (U t t' ...)
+ (subset? τ1* τ2* #:leq sub?)]
+ [`(,L1 ,L2) #:when (= L1 L2)
+ ;; - SUB : a<:b => (U a t' ...) <: (U b t' ...)
+ ;; `∪->list` guarantees same order on type members
+ ;; `sub?` is reflexive
+ (andmap sub? τ1* τ2*)]
+ [_ #f])]
+ [_
+ ;; Could be (U ...) <: T
+ (sub? τ1 τ2)]))
+
+ (current-sub? ∪-sub?)
+ (current-typecheck-relation (current-sub?))
+)
+
;; - TEST subtyping, with 'values' and with 'functions'
-;; - add filters
+
+;; -----------------------------------------------------------------------------
+;; --- Filters
+(begin-for-syntax
+ (define (simple-Π τ)
+ (syntax-parse (τ-eval τ)
+ [~Boolean
+ #'boolean?]
+ [~Int
+ #'integer?]
+ [~Str
+ #'string?]
+ ['Number
+ #'number?]
+ ['Natural
+ #'(lambda (n) (and (integer? n) (not (negative? n))))]
+ [_
+ (error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))]))
+ (define current-Π (make-parameter simple-Π)))
+
+;; - "simple", (Int ? e)
+;; - "correct", where the function is effectful and independent of cond
+
+;; - check if τ0 is a union type
+;; - check if τ-filter is a subtype of τ0
+;; - drop absurd branches?
+;; - allow x not identifier
+(define-typed-syntax test #:datum-literals (?)
+ [(_ [τ-filter:type ? x-stx:id] e1 e2)
+ ;; Get the filter type, evaluate to a runtime predicate
+ #:with f ((current-Π) #'τ-filter)
+ #:fail-unless (syntax-e #'f)
+ (format "Could not express type '~a' as a filter." #'τ-filter-stx)
+ ;; TypeCheck e0:normally, e1:positive, e2:negative
+ #:with (x τ0) (infer+erase #'x-stx)
+ ;; #:when (printf "Check'd e0, type is ~a\n" (syntax->datum #'τ0))
+ #:with [_ e1+ τ1] (infer/tyctx+erase #'([x-stx : τ-filter]) #'e1)
+ ;; #:when (printf "Check'd e1\n")
+ #:with [_ e2+ τ2] (infer/tyctx+erase #`([x-stx : #,(∖ #'τ0 #'τ-filter)]) #'e2)
+ ;; #:when (printf "Checked e2\n")
+ ;; Expand to a conditional, using the runtime predicate
+ (⊢ (if (f x) e1+ e2+)
+ : (∪ τ1 τ2))])
+
+;; - add filters (install filters, at start of file)
;; - TEST basic filters
;; - TEST function filters (delayed filters?)
;; - disallow (U (-> ...) (-> ...))
;; - TEST latent filters -- listof BLAH
+
;; - integrate with sysf
-;; (begin-for-syntax
-;; (define stlc:sub? (current-sub?))
-;; )
diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt
@@ -16,7 +16,7 @@
#:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
(typecheck-fail
(λ ([x : (∪)]) x)
- #:with-msg "empty union type")
+ #:with-msg "Improper usage of type constructor ∪")
(typecheck-fail
(λ ([x : (∪ ∪)]) x)
#:with-msg "Improper usage of type constructor ∪")
@@ -45,14 +45,188 @@
: (→ (∪ Boolean Int) Int))
(check-type (λ ([x : (∪ Int Boolean Boolean Int)]) x)
: (→ (∪ Boolean Int) (∪ Boolean Int)))
+(check-type (λ ([x : (∪ (∪ Int Boolean))]) 42)
+ : (→ (∪ Int Boolean) Int))
+(check-type (λ ([x : (∪ Int Boolean)]) 42)
+ : (→ (∪ (∪ Int Boolean)) Int))
+(check-type (λ ([x : (∪ Int Boolean)]) 42)
+ : (→ (∪ (∪ Int Boolean) (∪ Int Boolean)) Int))
+
;; -----------------------------------------------------------------------------
-;; --- basic subtyping
-;; (check-type 1 : (∪ Int))
-;; (check-type 1 : (∪ Int Boolean))
-;; (check-type 1 : (∪ Boolean Int))
-;; (check-type 1 : (∪ Boolean Int (→ Boolean Boolean)))
-;; (check-type 1 : (∪ (∪ Int)))
-
-;; (check-not-type 1 : (∪ Boolean))
-;; (check-not-type 1 : (∪ Boolean (→ Int Int)))
+;; --- subtyping
+
+;; ---- basics
+(check-type 1 : (∪ Int))
+(check-type 1 : (∪ (∪ Int)))
+
+(check-not-type 1 : (∪ Boolean))
+
+;; - AMB : t <: t' => t <: (U ... t' ...)
+(check-type 1 : (∪ Boolean Int))
+(check-type -1 : (∪ Int Boolean))
+(check-type 1 : (∪ Boolean Int (→ Boolean Boolean)))
+(check-type 1 : (∪ (∪ Int Boolean) (∪ Int Boolean)))
+
+(check-not-type 1 : (∪ Boolean (→ Int Int)))
+
+;; --- EXT : (U t' ...) <: (U t t' ...)
+(check-type (λ ([x : (∪ Int Boolean)]) x)
+ : (→ (∪ Int Boolean) (∪ Int Boolean Str)))
+(check-type (λ ([x : (∪ Int Boolean)]) x)
+ : (→ (∪ Boolean) (∪ Int Boolean Str)))
+
+(check-not-type (λ ([x : (∪ Int Boolean)]) x)
+ : (→ (∪ Int Boolean) (∪ Int)))
+(check-not-type (λ ([x : (∪ Int Boolean)]) x)
+ : (→ (∪ Boolean Int Str) (∪ Int Boolean)))
+
+;; --- SUB : a<:b => (U a t' ...) <: (U b t' ...)
+(check-type (λ ([x : (∪ Int Str)]) x)
+ : (→ (∪ Int Str) (∪ Num Str)))
+(check-type (λ ([x : (∪ Int Str)]) x)
+ : (→ (∪ Nat Str) (∪ Num Str)))
+
+(check-type (λ ([x : (∪ Int Str)]) x)
+ : (→ (∪ Int Str) Top))
+
+(check-not-type (λ ([x : (∪ Int Str)]) x)
+ : (→ Top (∪ Num Str)))
+
+;; -----------------------------------------------------------------------------
+;; --- Basic Filters (applying functions)
+
+;; --- is-boolean?
+(check-type
+ (λ ([x : (∪ Boolean Int)])
+ (test [Boolean ? x]
+ #t
+ #f))
+ : (→ (∪ Boolean Int) Boolean))
+(check-type-and-result
+ ((λ ([x : (∪ Boolean Int)])
+ (test (Boolean ? x)
+ #t
+ #f)) #t)
+ : Boolean ⇒ #t)
+(check-type-and-result
+ ((λ ([x : (∪ Boolean Int)])
+ (test (Boolean ? x)
+ #t
+ #f)) 902)
+ : Boolean ⇒ #f)
+
+;; --- successor
+;; (check-type
+;; (λ ([x : (∪ Int Boolean)])
+;; (test (Int ? x)
+;; (+ 1 x)
+;; (if x 1 0)))
+;; : Int)
+;; (check-type-and-result
+;; ((λ ([x : (∪ Int Boolean)])
+;; (test (Int ? x)
+;; (+ 1 x)
+;; (if x 1 0))) #f)
+;; : Int ⇒ 0)
+;; (check-type-and-result
+;; ((λ ([x : (∪ Int Boolean)])
+;; (test (Int ? x)
+;; (+ 1 x)
+;; (if x 1 0))) #t)
+;; : Int ⇒ 1)
+;; (check-type-and-result
+;; ((λ ([x : (∪ Int Boolean)])
+;; (test (Int ? x)
+;; (+ 1 x)
+;; (if x 1 0))) 9000)
+;; : Int ⇒ 9001)
+
+;; ;; --- Do-nothing filter
+(check-type
+ (λ ([x : Int])
+ (test (Int ? x) #t #f))
+ : (→ Int Boolean))
+(check-type
+ (λ ([x : Int])
+ (test (Boolean ? x) 1 0))
+ : (→ Int Int))
+
+;; --- Filter a subtype
+;; (check-type
+;; (λ ([x : (∪ Nat Boolean)])
+;; (test (Int ? x)
+;; x
+;; x))
+;; : (→ (∪ Nat Bool) (∪ Int (∪ Nat Bool))))
+
+;; (check-type
+;; (λ ([x : (∪ Int Bool)])
+;; (test (Nat ? x)
+;; (+ 2 x)
+;; x))
+;; : (→ (∪ Bool Int) (∪ Int Bool)))
+
+;; (check-type-and-result
+;; ((λ ([x : (∪ Int Bool)])
+;; (test (Num ? x)
+;; #f
+;; x)) #t)
+;; : (→ (∪ Int Bool) Bool)
+;; ⇒ #t)
+
+;; ;; Should filter all the impossible types
+;; (check-type-and-result
+;; ((λ ([x : (∪ Nat Int Num Bool)])
+;; (test (Num ? x)
+;; #f
+;; x)) #t)
+;; : (→ (∪ Nat Int Num Bool) Bool)
+;; ⇒ #t)
+
+;; -----------------------------------------------------------------------------
+;; --- misc subtyping + filters (regression tests)
+(check-type
+ (λ ([x : (∪ Int Boolean)])
+ (test (Int ? x)
+ 0
+ 1))
+ : (→ (∪ Int Boolean) Nat))
+(check-type
+ (λ ([x : (∪ Int Boolean)])
+ (test (Int ? x)
+ 0
+ 1))
+ : (→ (∪ Int Boolean) Int))
+
+;; -----------------------------------------------------------------------------
+;; --- Invalid filters
+
+(typecheck-fail
+ (λ ([x : (∪ Int Boolean)])
+ (test (1 ? x) #t #f))
+ #:with-msg "not a valid type")
+(typecheck-fail
+ (test (1 ? 1) #t #f)
+ #:with-msg "not a valid type")
+(typecheck-fail
+ (test (1 ? 1) #t #f)
+ #:with-msg "not a valid type")
+(typecheck-fail
+ (test (#f ? #t) #t #f)
+ #:with-msg "not a valid type")
+
+;; -----------------------------------------------------------------------------
+;; --- TODO Subtypes should not be collapsed
+;; (Not sure how to test this, because type=? is subtyping and these ARE subtypes)
+;; (check-not-type (λ ([x : (∪ Int Nat)]) #t)
+;; : (→ Nat Boolean))
+;; (check-not-type (λ ([x : (∪ Int Nat)]) #t)
+;; : (→ Int Boolean))
+
+;; ;; -----------------------------------------------------------------------------
+;; ;; --- Filter values (should do nothing)
+
+;; (check-type
+;; (test (Int ? 1) #t #f)
+;; : Boolean)
