commit 67d28645f93d602954524c63ff6d1e9f2538cd3d
parent f7635af9b59d846e10f58102059acf41a328e58b
Author: stchang <stchang@ccs.neu.edu>
Date: Thu, 22 Oct 2015 17:05:05 -0400
Merged in o+ (pull request #4)
Occurence types, improved
Diffstat:
4 files changed, 587 insertions(+), 99 deletions(-)
diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
@@ -1,5 +1,7 @@
#lang s-exp "typecheck.rkt"
(extends "stlc+sub.rkt" #:except #%datum)
+;(extends "stlc+tup.rkt" #:except + #%datum and)
+(extends "stlc+cons.rkt" #:except + #%datum and)
;; Calculus for occurrence typing.
;; - Types can be simple, or sets of simple types
@@ -48,7 +50,7 @@
(if (null? τ*)
#'Bot
(τ-eval #`(∪ #,@τ*))))
-
+
(define (∖ τ1 τ2)
(cond
[(∪? τ1)
@@ -67,42 +69,69 @@
;; 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* ...)
- ;; 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 (apply append τ**) (current-type=?))
- symbol<?
- #:key τ->symbol))
- ;; Check for empty & singleton lists
- (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 τ)]
+ (syntax-parse τ
+ [(_ κ)
+ (syntax->datum #'κ)]
+ [(_ κ (_ () _ τ* ...))
+ (define κ-str (symbol->string (syntax->datum #'κ)))
+ (define τ-str*
+ (map (compose1 symbol->string τ->symbol) (syntax->list #'(τ* ...))))
+ (string->symbol
+ (string-append
+ (apply string-append "(" κ-str τ-str*)
+ ")"))]
[_
- (τ-eval τ-stx)]))
+ (error 'τ->symbol (~a (syntax->datum τ)))]))
+
+ (define ∪-eval
+ ;; Private helper: check that all functions have unique arities
+ ;; It's private because it assumes all τ* have been evaluated
+ (let ([assert-unique-arity-arrows
+ (lambda (τ*)
+ (for/fold ([seen '()])
+ ([τ (in-list τ*)])
+ (syntax-parse τ
+ [(~→ τ-dom* ... τ-cod)
+ (define arity (stx-length #'(τ-dom* ...)))
+ (when (memv arity seen)
+ (error '∪ (format "Cannot discriminate types in the union ~a. Multiple functions have arity ~a." (cons '∪ (map syntax->datum τ*)) arity)))
+ (cons arity seen)]
+ [_ seen])))])
+ (lambda (τ-stx)
+ (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 (apply append τ**) (current-type=?))
+ symbol<?
+ #:key τ->symbol))
+ ;; Check for empty & singleton lists
+ (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
+ (assert-unique-arity-arrows τ*)
+ #`#,(cons #'∪ τ*)]))
+ (τ-eval τ)]
+ [_
+ (τ-eval τ-stx)]))))
(current-type-eval ∪-eval))
;; -----------------------------------------------------------------------------
@@ -120,36 +149,37 @@
[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))
- (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)])))
-
+ (define ∪-sub?
+ (let ([sub? (current-sub?)])
+ (lambda (τ1-stx τ2-stx)
+ (define τ1 ((current-type-eval) τ1-stx))
+ (define τ2 ((current-type-eval) τ2-stx))
+ (or (Bot? τ1) (Top? τ2)
+ (match `(,(∪? τ1) ,(∪? τ2))
+ ['(#f #t)
+ ;; AMB : a<:b => a <: (U ... b ...)
+ (for/or ([τ (in-list (∪->list τ2))])
+ ((current-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 (current-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 (current-sub?) τ1* τ2*)]
+ [_ #f])]
+ ['(#t #f)
+ ;; - ALL : t... <: t' => (U t ...) <: t'
+ (andmap (lambda (τ) ((current-sub?) τ τ2)) (∪->list τ1))]
+ ['(#f #f)
+ ;; Fall back to OLD sub
+ (sub? τ1 τ2)])))))
+
(current-sub? ∪-sub?)
(current-typecheck-relation (current-sub?))
)
@@ -160,47 +190,165 @@
;; Makes it easy to add a new filter & avoids duplicating this map
(begin-for-syntax
- (define (simple-Π τ)
- (syntax-parse (τ-eval τ)
- [~Boolean
- #'boolean?]
- [~Int
- #'integer?]
- [~Str
- #'string?]
- [~Num
- #'number?]
- [~Nat
- #'(lambda (n) (and (integer? n) (not (negative? n))))]
- [_
- (error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))]))
- (define current-Π (make-parameter simple-Π)))
+ (define current-Π (make-parameter (lambda (x) (error 'Π))))
+
+ (define (type->filter τ)
+ (define f ((current-Π) τ))
+ (unless f
+ (error 'τ->filter (format "Could not express type '~a' as a filter." (syntax->datum τ))))
+ f)
+
+ (define (type*->filter* τ*)
+ (map (current-Π) τ*))
+
+ (define (simple-Π τ)
+ (syntax-parse (τ-eval τ)
+ [~Boolean
+ #'boolean?]
+ [~Int
+ #'integer?]
+ [~Str
+ #'string?]
+ [~Num
+ #'number?]
+ [~Nat
+ #'(lambda (n) (and (integer? n) (not (negative? n))))]
+ [(~→ τ* ... τ)
+ (define k (stx-length #'(τ* ...)))
+ #`(lambda (f) (and (procedure? f) (procedure-arity-includes? f #,k #f)))]
+ [(~∪ τ* ...)
+ (define filter* (type*->filter* (syntax->list #'(τ* ...))))
+ #`(lambda (v) (for/or ([f (in-list (list #,@filter*))]) (f v)))]
+ [_
+ (error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))]))
+ (current-Π simple-Π)
+
+)
;; (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 (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
- #: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
+ ;; -- THIS CASE BELONGS IN A NEW FILE
+ [(_ [τ0+:type ? (unop x-stx:id n-stx:nat)] e1 e2)
+ ;; 1. Check that we're using a known eliminator
+ #:when (free-identifier=? #'proj #'unop)
+ ;; 2. Make sure we're filtering with a valid type
+ #:with f (type->filter #'τ0+)
+ ;; 3. Typecheck the eliminator call. Remember the type & apply the filter.
+ ;; (This type is PROBABLY a union -- else why bother testing!)
+ #:with (e0+ τ0) (infer+erase #'(unop x-stx n-stx))
+ #:with τ0- (∖ #'τ0 #'τ0+)
+ ;; 4. Build the +/- types for our identifier; the thing we apply the elim. + test to
+ ;; We know that x has a pair type because (proj x n) typechecked
+ #:with (x (~× τi* ...)) (infer+erase #'x-stx)
+ #:with τ+ #`(× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0+))
+ #:with τ- #`(× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0-))
+ ;; 5. Check the branches with the refined types
+ #:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ+]) #'e1)
+ #:with [x2 e2+ τ2] (infer/ctx+erase #'([x-stx : τ-]) #'e2)
+ ;; 6. Desugar, replacing the filtered identifier
+ (⊢ (if (f e0+)
+ ((lambda x1 e1+) x-stx)
+ ((lambda x2 e2+) x-stx))
+ : (∪ τ1 τ2))]
+ ;; TODO lists
+ ;; For now, we can't express the type (List* A (U A B)), so our filters are too strong
+ ;; -- THE ORIGINAL
+ [(_ [τ0+:type ? x-stx:id] e1 e2)
+ #:with f (type->filter #'τ0+)
#:with (x τ0) (infer+erase #'x-stx)
- #:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ-filter]) #'e1)
- #:with [x2 e2+ τ2] (infer/ctx+erase #`([x-stx : #,(∖ #'τ0 #'τ-filter)]) #'e2)
+ #:with τ0- (∖ #'τ0 #'τ0+)
+ #:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ0+]) #'e1)
+ #:with [x2 e2+ τ2] (infer/ctx+erase #'([x-stx : τ0-]) #'e2)
;; Expand to a conditional, using the runtime predicate
(⊢ (if (f x-stx)
((lambda x1 e1+) x-stx)
((lambda x2 e2+) x-stx))
: (∪ τ1 τ2))])
-;; - TEST function filters (delayed filters?)
-;; - disallow (U (-> ...) (-> ...))
-;; - TEST latent filters -- listof BLAH
+;; =============================================================================
+;; === BELONGS IN A NEW FILE
+
+;; (extends "stlc+occurrence.rkt"); #:rename [test ot:test])
+;; (extends "stlc+tup.rkt" #:except + #%datum)
+
+(define-for-syntax (replace-at τ* n τ-new)
+ (for/list ([τ-old (in-list τ*)]
+ [i (in-naturals)])
+ (if (= i n)
+ τ-new
+ τ-old)))
-;; - integrate with sysf
+;; Add subtyping for tuples
+(begin-for-syntax
+ (define ×-sub?
+ (let ([sub? (current-sub?)])
+ (lambda (τ1-stx τ2-stx)
+ (define τ1 ((current-type-eval) τ1-stx))
+ (define τ2 ((current-type-eval) τ2-stx))
+ (or (Bot? τ1) (Top? τ2)
+ (syntax-parse `(,τ1 ,τ2)
+ [((~× τi1* ...)
+ (~× τi2* ...))
+ (and (stx-length=? #'(τi1* ...)
+ #'(τi2* ...))
+ ;; Gotta use (current-sub?), because products may be recursive
+ (stx-andmap (current-sub?) #'(τi1* ...) #'(τi2* ...)))]
+ [_
+ (sub? τ1 τ2)])))))
+ (current-sub? ×-sub?)
+ (current-typecheck-relation (current-sub?)))
+
+;; --- Update Π for products
+(begin-for-syntax
+ (define π-Π
+ (let ([Π (current-Π)])
+ (lambda (τ)
+ (syntax-parse (τ-eval τ)
+ [(~× τ* ...)
+ (define filter* (type*->filter* (syntax->list #'(τ* ...))))
+ #`(lambda (v*)
+ (and (list? v*)
+ (for/and ([v (in-list v*)]
+ [f (in-list (list #,@filter*))])
+ (f v))))]
+ [_ ;; Fall back
+ (Π τ)]))))
+ (current-Π π-Π))
+;; =============================================================================
+;; === Lists
+
+;; Subtyping for lists
+(begin-for-syntax
+ (define list-sub?
+ (let ([sub? (current-sub?)])
+ (lambda (τ1-stx τ2-stx)
+ (define τ1 ((current-type-eval) τ1-stx))
+ (define τ2 ((current-type-eval) τ2-stx))
+ (or (Bot? τ1) (Top? τ2)
+ (syntax-parse `(,τ1 ,τ2)
+ [((~List τi1)
+ (~List τi2))
+ ((current-sub?) #'τi1 #'τi2)]
+ [_
+ (sub? τ1 τ2)])))))
+ (current-sub? list-sub?)
+ (current-typecheck-relation (current-sub?)))
+
+;; --- Update Π for lists
+(begin-for-syntax
+ (define list-Π
+ (let ([Π (current-Π)])
+ (lambda (τ)
+ (syntax-parse (τ-eval τ)
+ [(~List τi)
+ (define f ((current-Π) #'τi))
+ #`(lambda (v*)
+ (and (list? v*)
+ (for/and ([v (in-list v*)])
+ (#,f v))))]
+ [_ ;; Fall back
+ (Π τ)]))))
+ (current-Π list-Π))
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -42,7 +42,9 @@
(Top? τ2)))
(define current-sub? (make-parameter sub?))
(current-typecheck-relation sub?)
- (define (subs? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2))
+ (define (subs? τs1 τs2)
+ (and (stx-length=? τs1 τs2)
+ (stx-andmap (current-sub?) τs1 τs2)))
(define-syntax (define-sub-relation stx)
(syntax-parse stx #:datum-literals (<: =>)
diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt
@@ -207,6 +207,15 @@
: Boolean
⇒ #t)
+;; Can refine non-union types
+(check-type-and-result
+ ((λ ([x : Top])
+ (test (Str ? x)
+ x
+ "nope"))
+ "yes")
+ : Str ⇒ "yes")
+
;; -----------------------------------------------------------------------------
;; --- misc subtyping + filters (regression tests)
(check-type
@@ -270,15 +279,340 @@
: Nat ⇒ 2)
;; -----------------------------------------------------------------------------
-;; --- TODO Filter values (should do nothing)
+;; --- Functions in union
+
+(check-type (λ ([x : (∪ Int (∪ Nat) (∪ (→ Int Str Int)) (→ (→ (→ Int Int)) Int))]) #t)
+ : (→ (∪ Int Nat (→ Int Str Int) (→ (→ (→ Int Int)) Int)) Boolean))
+
+(check-type (λ ([x : (∪ Int (→ Int Int))]) #t)
+ : (→ Int Boolean))
+
+;; --- filter functions
+(check-type
+ (λ ([x : (∪ Int (→ Int Int))])
+ (test ((→ Int Int) ? x)
+ (x 0)
+ x))
+ : (→ (∪ Int (→ Int Int)) Int))
+
+(check-type
+ (λ ([x : (∪ (→ Int Int Int) (→ Int Int))])
+ (test ((→ Int Int) ? x)
+ (x 0)
+ (test (Int ? x)
+ x
+ (x 1 0))))
+ : (→ (∪ (→ Int Int Int) (→ Int Int)) Int))
+
+(check-type-and-result
+ ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
+ (test ((→ Int Int) ? x)
+ (x 0)
+ (test (Int ? x)
+ x
+ (x 1 0)))) 1)
+ : Int ⇒ 1)
+
+(check-type-and-result
+ ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
+ (test ((→ Int Int) ? x)
+ (x 0)
+ (test (Int ? x)
+ x
+ (x 1 0)))) (λ ([y : Int]) 5))
+ : Int ⇒ 5)
+
+(check-type-and-result
+ ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
+ (test ((→ Int Int) ? x)
+ (x 0)
+ (test (Int ? x)
+ x
+ (x 1 0)))) (λ ([y : Int] [z : Int]) z))
+ : Int ⇒ 0)
+
+;; --- disallow same-arity functions
+(typecheck-fail
+ (λ ([x : (∪ (→ Int Int) (→ Str Str))]) 1)
+ #:with-msg "Cannot discriminate")
+
+;; -----------------------------------------------------------------------------
+;; --- Filter with unions
+
+(check-type
+ (λ ([x : (∪ Int Str)])
+ (test ((∪ Int Str) ? x)
+ x
+ "nope"))
+ : (→ (∪ Int Str) (∪ Int Str)))
+
+(check-type
+ (λ ([x : (∪ Int Str Boolean)])
+ (test ((∪ Int Str) ? x)
+ x
+ "Nope"))
+ : (→ (∪ Int Str Boolean) (∪ Int Str)))
+
+(check-type
+ (λ ([x : (∪ Int Str Boolean)])
+ (test ((∪ Int Str) ? x)
+ (test (Str ? x)
+ "yes"
+ "int")
+ "bool"))
+ : (→ (∪ Int Str Boolean) Str))
+
+(check-type-and-result
+ ((λ ([x : (∪ Str Boolean)])
+ (test ((∪ Int Nat Num) ? x)
+ x
+ (+ 1 2))) "hi")
+ : Num ⇒ 3)
+
+(check-type-and-result
+ ((λ ([x : (∪ Str Int Boolean)])
+ (test ((∪ Int Str) ? x)
+ x
+ "error")) 1)
+ : (∪ Str Int) ⇒ 1)
+
+(check-type-and-result
+ ((λ ([x : (∪ Str Int Boolean)])
+ (test ((∪ Int Str) ? x)
+ x
+ "error")) "hi")
+ : (∪ Int Str) ⇒ "hi")
+
+;; -----------------------------------------------------------------------------
+;; --- Subtyping products
+
+(check-type (tup 1) : (× Nat))
+(check-type (tup 1) : (× Int))
+(check-type (tup 1) : (× Num))
+(check-type (tup 1) : (× Top))
+(check-type (tup 1) : Top)
+
+(check-not-type (tup 1) : Boolean)
+(check-not-type (tup 1) : Str)
+(check-not-type (tup 1) : (× Str))
+(check-not-type (tup 1) : (× Int Str))
+(check-not-type (tup 1) : Bot)
+
+(check-type (tup 1 2 3) : (× Int Nat Num))
+(check-type (tup 1 2 3) : (× Num Nat Num))
+(check-type (tup 1 2 3) : (× Top Top Num))
+(check-type (tup 1 "2" 3) : (× Int Top Int))
+
+(check-not-type (tup 1 2 3) : (× Nat Nat Str))
+
+;; -----------------------------------------------------------------------------
+;; --- Latent filters (on products)
+
+(check-type
+ (λ ([v : (× (∪ Int Str) Int)])
+ (test (Int ? (proj v 0))
+ (+ (proj v 0) (proj v 1))
+ 0))
+ : (→ (× (∪ Int Str) Int) Num))
+
+(check-type-and-result
+ ((λ ([v : (× (∪ Int Str) Int)])
+ (test (Int ? (proj v 0))
+ (+ (proj v 0) (proj v 1))
+ 0))
+ (tup ((λ ([x : (∪ Int Str)]) x) -2) -3))
+ : Num ⇒ -5)
+(check-type-and-result
+ ((λ ([v : (× (∪ Int Str) Int)])
+ (test (Int ? (proj v 0))
+ (+ (proj v 0) (proj v 1))
+ 0))
+ (tup "hi" -3))
+ : Num ⇒ 0)
+
+;; --- Use a product as filter
+
+(check-type
+ (λ ([x : (∪ Int (× Int Int Int))])
+ (test (Int ? x)
+ (+ 1 x)
+ (+ (proj x 0) (+ (proj x 1) (proj x 2)))))
+ : (→ (∪ (× Int Int Int) Int) Num))
+
+(check-type-and-result
+ ((λ ([x : (∪ Int (× Int Int Int))])
+ (test (Int ? x)
+ (+ 1 x)
+ (+ (proj x 0) (+ (proj x 1) (proj x 2)))))
+ 0)
+ : Num ⇒ 1)
+
+(check-type-and-result
+ ((λ ([x : (∪ Int (× Int Int Int))])
+ (test (Int ? x)
+ (+ 1 x)
+ (+ (proj x 0) (+ (proj x 1) (proj x 2)))))
+ (tup 2 2 2))
+ : Num ⇒ 6)
+
+(check-type-and-result
+ ((λ ([x : (∪ Int (× Str Nat) (× Int Int Int))])
+ (test (Int ? x)
+ (+ 1 x)
+ (test ((× Int Int Int) ? x)
+ (+ (proj x 0) (+ (proj x 1) (proj x 2)))
+ (proj x 1))))
+ (tup 2 2 2))
+ : Num ⇒ 6)
+
+(check-type-and-result
+ ((λ ([x : (∪ Int (× Str Nat) (× Int Int Int))])
+ (test (Int ? x)
+ (+ 1 x)
+ (test ((× Int Int Int) ? x)
+ (+ (proj x 0) (+ (proj x 1) (proj x 2)))
+ (proj x 1))))
+ (tup "yolo" 33))
+ : Num ⇒ 33)
+
+;; -- All together now
+
+(check-type-and-result
+ ((λ ([x : (∪ Int (× Boolean Boolean) (× Int (∪ Str Int)))])
+ (test (Int ? x)
+ "just an int"
+ (test ((× Boolean Boolean) ? x)
+ "pair of bools"
+ (test (Str ? (proj x 1))
+ (proj x 1)
+ "pair of ints"))))
+ (tup 33 "success"))
+ : Str ⇒ "success")
+
+(check-type-and-result
+ ((λ ([x : (∪ Int (× Int Int) (× Int (∪ Str Int)))])
+ (test (Int ? x)
+ "just an int"
+ (test ((× Int Int) ? x)
+ "pair of ints"
+ (test (Str ? (proj x 1))
+ (proj x 1)
+ "another pair of ints"))))
+ (tup 33 "success"))
+ : Str ⇒ "success")
+
+;; -----------------------------------------------------------------------------
+;; --- Filter lists
+
+(check-type
+ (λ ([x : (List (∪ Int Str))])
+ (test ((List Str) ? x)
+ x
+ #f))
+ : (→ (List (∪ Int Str)) (∪ Boolean (List Str))))
+
+;; -- -subtyping lists
+(check-type
+ (cons 1 (nil {Nat}))
+ : (List Int))
+
+(check-type
+ ((λ ([filter/3 : (→ (List (∪ Int Str)) (List Int))]
+ [add*/3 : (→ Num (List Num) (List Num))]
+ [xs : (× (∪ Int Str) (∪ Int Str) (∪ Int Str))])
+ (add*/3 5 (filter/3 (cons (proj xs 0)
+ (cons (proj xs 1)
+ (cons (proj xs 2)
+ (nil {(∪ Str Int)})))))))
+ ;; filter (okay this is a little tricky for recursion)
+ (λ ([xs : (List (∪ Int Str))])
+ ((λ ([v1 : (∪ Int Str)]
+ [v2 : (∪ Int Str)]
+ [v3 : (∪ Int Str)])
+ (test (Int ? v1)
+ (cons v1 (test (Int ? v2)
+ (cons v2 (test (Int ? v3)
+ (cons v3 (nil {Int}))
+ (nil {Int})))
+ (test (Int ? v3)
+ (cons v3 (nil {Int}))
+ (nil {Int}))))
+ (test (Int ? v2)
+ (cons v2 (test (Int ? v3)
+ (cons v3 (nil {Int}))
+ (nil {Int})))
+ (test (Int ? v3)
+ (cons v3 (nil {Int}))
+ (nil {Int})))))
+ (head xs) (head (tail xs)) (head (tail (tail xs)))))
+ ;; add3
+ (λ ([n : Num] [xs : (List Num)])
+ (cons (+ n (head xs))
+ (cons (+ n (head (tail xs)))
+ (cons (+ n (head (tail (tail xs))))
+ (nil {Num})))))
+ ;; xs (3-tuple)
+ (tup 1 "foo" 3))
+ : (List Num))
+
+;; -----------------------------------------------------------------------------
+;; --- ICFP'10 examples
+
+;; -- Exaple 1 (x can have any type)
+(check-type
+ (λ ([x : Top])
+ (test (Num ? x)
+ (+ 1 x)
+ 0))
+ : (→ Top Num))
+
+;; -- Example 2
+(check-type
+ (λ ([x : (∪ Str Num)]
+ [str-length : (→ Str Num)])
+ (test (Num ? x)
+ (+ 1 x)
+ (str-length x)))
+ : (→ (∪ Str Num) (→ Str Num) Num))
+
+;; -- TODO Example 3 (requires IF)
;; (check-type
-;; (test (Int ? 1) #t #f)
-;; : Boolean)
+;; (λ ([member : (→ Num (List Num) Boolean)])
+;; (λ ([x : Num] [l : (List Num)])
+;; (if (member x l)
+;; <compute with x>
+;; <fail>)))
+;; : <compute-result>
+
+;; -- Example 4
+(check-type
+ (λ ([x : (∪ Num Str Top)] [f : (→ (∪ Num Str) Num)])
+ (test ((∪ Num Str) ? x)
+ (f x)
+ 0))
+ : (→ (∪ Num Str Top) (→ (∪ Num Str) Num) Num))
+
+;; Exmample 10 (we don't allow non-homogenous lists, so need to select head before filtering)
+(check-type
+ (λ ([p : (List (∪ Nat Str))])
+ ((λ ([x : (∪ Nat Str)])
+ (test (Num ? x)
+ (+ 1 x)
+ 7))
+ (head p)))
+ : (→ (List (∪ Nat Str)) Num))
;; -----------------------------------------------------------------------------
-;; --- TODO Filter functions
+;; --- TODO CPS filters
+
+;; -----------------------------------------------------------------------------
+;; --- TODO Filter on values (should do nothing)
+
+;; (check-type
+;; (test (Int ? 1) #t #f)
+;; : Boolean)
;; -----------------------------------------------------------------------------
-;; --- TODO Latent filters (on data structures)
+;; --- TODO Values as filters (check equality)
diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt
@@ -57,3 +57,7 @@
(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
(check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20)
+
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int))
+(check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))
