commit 1887d99abb12210aa6a7602d0b9c373d86c97626
parent 36bec40650c073048d0c4a63d38ebc8c87ec73ca
Author: Ben Greenman <types@ccs.neu.edu>
Date: Fri, 16 Oct 2015 18:56:54 -0400
[occurrence] filters for products
Diffstat:
2 files changed, 263 insertions(+), 66 deletions(-)
diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
@@ -1,5 +1,6 @@
#lang s-exp "typecheck.rkt"
(extends "stlc+sub.rkt" #:except #%datum)
+(extends "stlc+tup.rkt" #:except + #%datum and)
;; Calculus for occurrence typing.
;; - Types can be simple, or sets of simple types
@@ -147,35 +148,36 @@
[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?))
@@ -187,49 +189,128 @@
;; Makes it easy to add a new filter & avoids duplicating this map
(begin-for-syntax
- (define current-Π (make-parameter (lambda (x) (error 'Π))))
- (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* (for/list ([τ (in-syntax #'(τ* ...))])
- ((current-Π) τ)))
- #`(lambda (v) (for/or ([f (in-list (list #,@filter*))]) (f v)))]
- [_
- (error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))]))
- (current-Π 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))]
+ ;; -- 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))])
+;; =============================================================================
+;; === 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)))
+
+;; 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-Π π-Π))
+
diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt
@@ -375,6 +375,125 @@
: (∪ 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")
+
+;; -----------------------------------------------------------------------------
;; --- TODO CPS filters
;; -----------------------------------------------------------------------------
@@ -387,6 +506,3 @@
;; -----------------------------------------------------------------------------
;; --- TODO Values as filters (check equality)
-;; -----------------------------------------------------------------------------
-;; --- TODO Latent filters (on data structures)
-
