From 050c43b3a2eea7fc53f17219970b633799059b8d Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Tue, 6 Oct 2015 16:32:26 -0400 Subject: [PATCH 1/5] [occurrence] constructor + basic tests --- tapl/stlc+occurrence.rkt | 38 +++++++++++++++++++++ tapl/tests/stlc+occurrence-tests.rkt | 50 ++++++++++++++++++++++++++++ 2 files changed, 88 insertions(+) create mode 100644 tapl/stlc+occurrence.rkt create mode 100644 tapl/tests/stlc+occurrence-tests.rkt diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt new file mode 100644 index 0000000..4384c55 --- /dev/null +++ b/tapl/stlc+occurrence.rkt @@ -0,0 +1,38 @@ +#lang s-exp "typecheck.rkt" +(extends "stlc+sub.rkt" #:except #%datum) +;; TODO import if- form? + +;; Calculus for occurrence typing. +;; - Types can be simple, or sets of simple types +;; (aka "ambiguous types". +;; The type is one of a few ambiguous possibilities at compile-time) +;; - The U constructor makes ambiguous types +;; - `(if-τ? [x : τ] e1 e2)` form will insert a run-time check to discriminate amb. types +;; - For non-top types, τ is a subtype of (∪ τ1 ... τ τ2 ...) + +;; ============================================================================= + +(define-base-type Boolean) +(define-base-type Str) + +(define-typed-syntax #%datum + [(_ . n:boolean) (⊢ (#%datum . n) : Boolean)] + [(_ . n:str) (⊢ (#%datum . n) : Str)] + [(_ . x) #'(stlc+sub:#%datum . x)]) + +(define-type-constructor ∪ #:arity >= 1) + +;; - define normal form for U, sorted +;; - TEST create U types +;; - subtype U with simple, U with contained +;; - TEST subtyping, with 'values' and with 'functions' +;; - add filters +;; - 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 new file mode 100644 index 0000000..50ec6fb --- /dev/null +++ b/tapl/tests/stlc+occurrence-tests.rkt @@ -0,0 +1,50 @@ +#lang s-exp "../stlc+occurrence.rkt" +(require "rackunit-typechecking.rkt") + +;; ----------------------------------------------------------------------------- +;; basic types & syntax + +(check-type 1 : Int) +(check-type #f : Boolean) +(check-type "hello" : Str) +(check-type 1 : Top) +(check-type (λ ([x : (∪ Boolean Int)]) x) + : (→ (∪ Boolean Int) (∪ Boolean Int))) +(check-type (λ ([x : (∪ Int Int Int Int)]) x) + : (→ (∪ Int Int Int Int) (∪ Int Int Int Int))) + +(typecheck-fail + (λ ([x : ∪]) x) + #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") +(typecheck-fail + (λ ([x : (∪)]) x) + #:with-msg "Improper usage of type constructor ∪") +(typecheck-fail + (λ ([x : (∪ ∪)]) x) + #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") +(typecheck-fail + (λ ([x : (1 ∪)]) x) + ;; TODO Weird message for this one. + #:with-msg "Expected expression 1 to have → type") +(typecheck-fail + (λ ([x : (Int ∪)]) x) + ;; TODO a little weird of a message + #:with-msg "expected identifier") +(typecheck-fail + (λ ([x : (→ ∪ ∪)]) x) + #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") +(typecheck-fail + (λ ([x : (→ Int ∪)]) x) + #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") +(typecheck-fail + (λ ([x : (∪ Int →)]) x) + #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments") + +;; (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))) From 5497b347df8749fb1efea41da13fb11534c97508 Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Fri, 9 Oct 2015 02:24:09 -0400 Subject: [PATCH 2/5] [occurrence] simple type evaluator, assumes no recursive unions --- tapl/stlc+occurrence.rkt | 18 ++++++++++++++++-- tapl/tests/stlc+occurrence-tests.rkt | 8 +++----- 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt index 4384c55..23655e8 100644 --- a/tapl/stlc+occurrence.rkt +++ b/tapl/stlc+occurrence.rkt @@ -21,9 +21,23 @@ [(_ . x) #'(stlc+sub:#%datum . x)]) (define-type-constructor ∪ #:arity >= 1) +;; TODO disallow recursive ∪ +(begin-for-syntax + (define τ-eval (current-type-eval)) + (define (∪-eval τ) + (syntax-parse τ #:datum-literals (∪) + [(_ ∪ τ* ...) + ;; Assumes that each τ is non-∪ + (define τ*+ (for/list ([τ (in-syntax #'(τ* ...))]) (τ-eval τ))) + ;; TODO just make a set + #`#,(cons '∪ + (remove-duplicates + (sort τ*+ symboldatum) + (current-type=?)))] + [_ + (τ-eval τ)])) + (current-type-eval ∪-eval)) -;; - define normal form for U, sorted -;; - TEST create U types ;; - subtype U with simple, U with contained ;; - TEST subtyping, with 'values' and with 'functions' ;; - add filters diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt index 50ec6fb..9b22aa0 100644 --- a/tapl/tests/stlc+occurrence-tests.rkt +++ b/tapl/tests/stlc+occurrence-tests.rkt @@ -21,15 +21,13 @@ #:with-msg "Improper usage of type constructor ∪") (typecheck-fail (λ ([x : (∪ ∪)]) x) - #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") + #:with-msg "not a valid type") (typecheck-fail (λ ([x : (1 ∪)]) x) - ;; TODO Weird message for this one. - #:with-msg "Expected expression 1 to have → type") + #:with-msg "not a valid type") (typecheck-fail (λ ([x : (Int ∪)]) x) - ;; TODO a little weird of a message - #:with-msg "expected identifier") + #:with-msg "not a valid type") (typecheck-fail (λ ([x : (→ ∪ ∪)]) x) #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") From c5d6bfbf9e1d771040b49134087aaa615cc9be4d Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Sun, 11 Oct 2015 00:22:16 -0400 Subject: [PATCH 3/5] [occurrence] type eval --- tapl/stlc+occurrence.rkt | 35 +++++++++++++++++++--------- tapl/tests/stlc+occurrence-tests.rkt | 24 +++++++++++++------ 2 files changed, 41 insertions(+), 18 deletions(-) diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt index 23655e8..ab19beb 100644 --- a/tapl/stlc+occurrence.rkt +++ b/tapl/stlc+occurrence.rkt @@ -24,18 +24,31 @@ ;; TODO disallow recursive ∪ (begin-for-syntax (define τ-eval (current-type-eval)) - (define (∪-eval τ) - (syntax-parse τ #:datum-literals (∪) - [(_ ∪ τ* ...) - ;; Assumes that each τ is non-∪ - (define τ*+ (for/list ([τ (in-syntax #'(τ* ...))]) (τ-eval τ))) - ;; TODO just make a set - #`#,(cons '∪ - (remove-duplicates - (sort τ*+ symboldatum) - (current-type=?)))] + (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)) + (define τ* + (sort + (remove-duplicates (syntax->list #'(τ-stx* ...)) (current-type=?)) + symboldatum)) + (define τ + (cond + [(null? τ*) + (raise-user-error 'τ-eval "~a (~a:~a) empty union type ~a\n" + (syntax-source τ-stx) (syntax-line τ-stx) (syntax-column τ-stx) + (syntax->datum τ-stx))] + [(null? (cdr τ*)) + #`#,(car τ*)] + [else + #`#,(cons #'∪ τ*)])) + (τ-eval τ)] [_ - (τ-eval τ)])) + (τ-eval τ-stx)])) (current-type-eval ∪-eval)) ;; - subtype U with simple, U with contained diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt index 9b22aa0..61d5dba 100644 --- a/tapl/tests/stlc+occurrence-tests.rkt +++ b/tapl/tests/stlc+occurrence-tests.rkt @@ -10,27 +10,25 @@ (check-type 1 : Top) (check-type (λ ([x : (∪ Boolean Int)]) x) : (→ (∪ Boolean Int) (∪ Boolean Int))) -(check-type (λ ([x : (∪ Int Int Int Int)]) x) - : (→ (∪ Int Int Int Int) (∪ Int Int Int Int))) (typecheck-fail (λ ([x : ∪]) x) #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") (typecheck-fail (λ ([x : (∪)]) x) - #:with-msg "Improper usage of type constructor ∪") + #:with-msg "empty union type") (typecheck-fail (λ ([x : (∪ ∪)]) x) - #:with-msg "not a valid type") + #:with-msg "Improper usage of type constructor ∪") (typecheck-fail (λ ([x : (1 ∪)]) x) - #:with-msg "not a valid type") + #:with-msg "") (typecheck-fail (λ ([x : (Int ∪)]) x) - #:with-msg "not a valid type") + #:with-msg "expected identifier") (typecheck-fail (λ ([x : (→ ∪ ∪)]) x) - #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") + #:with-msg "Improper usage of type constructor ∪") (typecheck-fail (λ ([x : (→ Int ∪)]) x) #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments") @@ -38,6 +36,18 @@ (λ ([x : (∪ Int →)]) x) #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments") +;; ----------------------------------------------------------------------------- +;; --- type evaluation + +(check-type (λ ([x : (∪ Int Int Int Int)]) x) + : (→ Int Int)) +(check-type (λ ([x : (∪ Int Boolean)]) 42) + : (→ (∪ Boolean Int) Int)) +(check-type (λ ([x : (∪ Int Boolean Boolean Int)]) x) + : (→ (∪ Boolean Int) (∪ Boolean Int))) + +;; ----------------------------------------------------------------------------- +;; --- basic subtyping ;; (check-type 1 : (∪ Int)) ;; (check-type 1 : (∪ Int Boolean)) ;; (check-type 1 : (∪ Boolean Int)) From d7913f775356cd442b686f9548405033fc920e26 Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Tue, 13 Oct 2015 12:51:24 -0400 Subject: [PATCH 4/5] [occurrence] subtyping, normal form, and VERY BASIC filters. Having trouble propogating variables. --- tapl/stlc+occurrence.rkt | 166 +++++++++++++++++++++-- tapl/tests/stlc+occurrence-tests.rkt | 192 +++++++++++++++++++++++++-- 2 files changed, 336 insertions(+), 22 deletions(-) diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt index ab19beb..32cb7f8 100644 --- 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=?)) symboldatum)) + #: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 index 61d5dba..a4f7d77 100644 --- 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))) +;; --- subtyping -;; (check-not-type 1 : (∪ Boolean)) -;; (check-not-type 1 : (∪ Boolean (→ Int Int))) +;; ---- 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) From bc2e83c44975776800aa90fa6fe261321780d271 Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Tue, 13 Oct 2015 15:16:24 -0400 Subject: [PATCH 5/5] [occurence] simple filters complete --- tapl/stlc+occurrence.rkt | 127 +++++++++---------- tapl/tests/stlc+occurrence-tests.rkt | 174 +++++++++++++++++---------- 2 files changed, 177 insertions(+), 124 deletions(-) diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt index 32cb7f8..763c525 100644 --- a/tapl/stlc+occurrence.rkt +++ b/tapl/stlc+occurrence.rkt @@ -1,17 +1,24 @@ #lang s-exp "typecheck.rkt" (extends "stlc+sub.rkt" #:except #%datum) -;; TODO import if- form? ;; Calculus for occurrence typing. ;; - Types can be simple, or sets of simple types -;; (aka "ambiguous types". -;; The type is one of a few ambiguous possibilities at compile-time) -;; - The U constructor makes ambiguous types -;; - `(if-τ? [x : τ] e1 e2)` form will insert a run-time check to discriminate amb. types -;; - For non-top types, τ is a subtype of (∪ τ1 ... τ τ2 ...) +;; (aka "ambiguous types"; +;; the run-time value will have one of a few ambiguous possible types.) +;; - The ∪ constructor makes ambiguous types +;; - `(test [τ ? x] e1 e2)` form will insert a run-time check to discriminate ∪ +;; -- If the value at identifier x has type τ, then we continue to e1 with [x : τ] +;; -- Otherwise, we move to e2 with [x : (- (typeof x) τ)]. +;; i.e., [x : τ] is not possible +;; - Subtyping rules: +;; -- ALL : t ... <: t' => (U t ...) <: t' +;; -- AMB : t <: (U ... t ...) +;; -- EXT : (U t' ...) <: (U t t' ...) +;; -- ONE : a<:b => (U a t' ...) <: (U b t' ...) ;; ============================================================================= +(define-base-type Bot) ;; For empty unions (define-base-type Boolean) (define-base-type Str) @@ -28,8 +35,6 @@ ;; 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) @@ -40,33 +45,34 @@ (error '∪->list (format "Given non-ambiguous type '~a'" τ))])) (define (list->∪ τ*) - (τ-eval #`(∪ #,@τ*))) + (if (null? τ*) + #'Bot + (τ-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 + [else ; do nothing not non-union types τ1])) ) ;; ----------------------------------------------------------------------------- ;; --- Normal Form +;; Evaluate each type in the union, +;; remove duplicates +;; determinize the ordering of members +;; flatten nested unions + (begin-for-syntax (define τ-eval (current-type-eval)) + (define (τ->symbol τ) + ;; TODO recurse for function types (cadr (syntax->datum τ))) + (define (∪-eval τ-stx) (syntax-parse (τ-eval τ-stx) [(~∪ τ-stx* ...) @@ -82,7 +88,7 @@ (sort (remove-duplicates (apply append τ**) (current-type=?)) symbolsymbol)) ;; TODO handle functions & other constructors + #:key τ->symbol)) ;; Check for empty & singleton lists (define τ (cond @@ -101,13 +107,7 @@ ;; ----------------------------------------------------------------------------- ;; --- 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)]) @@ -121,39 +121,44 @@ (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)])) + (or (Bot? τ1) (Top? τ2) + (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])] + ['(#t #f) + ;; - ALL : t... <: t' => (U t ...) <: t' + (andmap (lambda (τ) (sub? τ τ2)) (∪->list τ1))] + ['(#f #f) + (sub? τ1 τ2)]))) (current-sub? ∪-sub?) (current-typecheck-relation (current-sub?)) ) -;; - TEST subtyping, with 'values' and with 'functions' - ;; ----------------------------------------------------------------------------- ;; --- Filters +;; These are stored imperatively, in a function. +;; Makes it easy to add a new filter & avoids duplicating this map + (begin-for-syntax (define (simple-Π τ) (syntax-parse (τ-eval τ) @@ -163,21 +168,20 @@ #'integer?] [~Str #'string?] - ['Number + [~Num #'number?] - ['Natural + [~Nat #'(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 - +;; (test (τ ? x) e1 e2) +;; TODO: ;; - check if τ0 is a union type ;; - check if τ-filter is a subtype of τ0 ;; - drop absurd branches? -;; - allow x not identifier +;; - allow x not identifier (1. does nothing 2. latent filters) (define-typed-syntax test #:datum-literals (?) [(_ [τ-filter:type ? x-stx:id] e1 e2) ;; Get the filter type, evaluate to a runtime predicate @@ -186,17 +190,14 @@ (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") + #:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ-filter]) #'e1) + #:with [x2 e2+ τ2] (infer/ctx+erase #`([x-stx : #,(∖ #'τ0 #'τ-filter)]) #'e2) ;; Expand to a conditional, using the runtime predicate - (⊢ (if (f x) e1+ e2+) + (⊢ (if (f x-stx) + ((lambda x1 e1+) x-stx) + ((lambda x2 e2+) x-stx)) : (∪ τ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 diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt index a4f7d77..fa9f1c4 100644 --- a/tapl/tests/stlc+occurrence-tests.rkt +++ b/tapl/tests/stlc+occurrence-tests.rkt @@ -59,6 +59,8 @@ ;; ---- basics (check-type 1 : (∪ Int)) (check-type 1 : (∪ (∪ Int))) +(check-type (λ ([x : Int]) x) + : (→ Bot Top)) (check-not-type 1 : (∪ Boolean)) @@ -93,6 +95,19 @@ (check-not-type (λ ([x : (∪ Int Str)]) x) : (→ Top (∪ Num Str))) +;; --- ALL +(check-type (λ ([x : (∪ Boolean Int Str)]) x) + : (→ (∪ Boolean Int Str) Top)) +(check-type (λ ([x : (∪ Nat Int Num)]) x) + : (→ (∪ Nat Int Num) Num)) +(check-type (λ ([x : (∪ Nat Int Num)]) x) + : (→ Nat Num)) + +;; --- misc +;; Because Int<:(U Int ...) +(check-type (λ ([x : (∪ Int Nat)]) #t) + : (→ Int Boolean)) + ;; ----------------------------------------------------------------------------- ;; --- Basic Filters (applying functions) @@ -117,30 +132,30 @@ : 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) +(check-type + (λ ([x : (∪ Int Boolean)]) + (test (Int ? x) + (+ 1 x) + 0)) + : (→ (∪ Int Boolean) (∪ Num Nat))) +(check-type-and-result + ((λ ([x : (∪ Int Boolean)]) + (test (Int ? x) + (+ 1 x) + 0)) #f) + : Num ⇒ 0) +(check-type-and-result + ((λ ([x : (∪ Int Boolean)]) + (test (Int ? x) + (+ 1 x) + 1)) #t) + : Num ⇒ 1) +(check-type-and-result + ((λ ([x : (∪ Int Boolean)]) + (test (Int ? x) + (+ 1 x) + 0)) 9000) + : Num ⇒ 9001) ;; ;; --- Do-nothing filter (check-type @@ -149,40 +164,48 @@ : (→ Int Boolean)) (check-type (λ ([x : Int]) - (test (Boolean ? x) 1 0)) - : (→ Int Int)) + (test (Boolean ? x) 0 x)) + : (→ Int (∪ Nat Int))) ;; --- Filter a subtype -;; (check-type -;; (λ ([x : (∪ Nat Boolean)]) -;; (test (Int ? x) -;; x -;; x)) -;; : (→ (∪ Nat Bool) (∪ Int (∪ Nat Bool)))) +(check-type + (λ ([x : (∪ Nat Boolean)]) + (test (Int ? x) + x + x)) + : (→ (∪ Nat Boolean) (∪ Int (∪ Nat Boolean)))) -;; (check-type -;; (λ ([x : (∪ Int Bool)]) -;; (test (Nat ? x) -;; (+ 2 x) -;; x)) -;; : (→ (∪ Bool Int) (∪ Int Bool))) +(check-type + (λ ([x : (∪ Int Boolean)]) + (test (Nat ? x) + x + x)) + : (→ (∪ Boolean Int) (∪ Int Nat Boolean))) -;; (check-type-and-result -;; ((λ ([x : (∪ Int Bool)]) -;; (test (Num ? x) -;; #f -;; x)) #t) -;; : (→ (∪ Int Bool) Bool) -;; ⇒ #t) +;; --- Filter a supertype +(check-type + (λ ([x : (∪ Int Boolean)]) + (test (Num ? x) + 1 + x)) + : (→ (∪ Boolean Int) (∪ Nat Boolean))) -;; ;; 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) +(check-type-and-result + ((λ ([x : (∪ Int Boolean)]) + (test (Num ? x) + #f + x)) #t) + : Boolean + ⇒ #t) + +;; Should filter all the impossible types +(check-type-and-result + ((λ ([x : (∪ Nat Int Num Boolean)]) + (test (Num ? x) + #f + x)) #t) + : Boolean + ⇒ #t) ;; ----------------------------------------------------------------------------- ;; --- misc subtyping + filters (regression tests) @@ -217,16 +240,45 @@ #: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)) +;; --- Subtypes should not be collapsed + +(check-not-type (λ ([x : (∪ Int Nat)]) #t) + : (→ Num Boolean)) +(check-type ((λ ([x : (∪ Int Nat Boolean)]) + (test (Int ? x) + 2 + (test (Nat ? x) + 1 + 0))) + #t) + : Nat ⇒ 0) +(check-type ((λ ([x : (∪ Int Nat)]) + (test (Nat ? x) + 1 + (test (Int ? x) + 2 + 0))) + 1) + : Nat ⇒ 1) +(check-type ((λ ([x : (∪ Int Nat)]) + (test (Int ? x) + 2 + (test (Nat ? x) + 1 + 0))) + -10) + : Nat ⇒ 2) -;; ;; ----------------------------------------------------------------------------- -;; ;; --- Filter values (should do nothing) +;; ----------------------------------------------------------------------------- +;; --- TODO Filter values (should do nothing) ;; (check-type ;; (test (Int ? 1) #t #f) ;; : Boolean) + +;; ----------------------------------------------------------------------------- +;; --- TODO Filter functions + +;; ----------------------------------------------------------------------------- +;; --- TODO Latent filters (on data structures) +