[occurrence] filters for lists

tapl/stlc+occurrence.rkt

@@ -1,6 +1,7 @@
 #lang s-exp "typecheck.rkt"
 (extends "stlc+sub.rkt" #:except #%datum)
-(extends "stlc+tup.rkt" #:except + #%datum and)
+;(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
@@ -251,6 +252,8 @@
            ((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+)
@@ -314,3 +317,38 @@
          (Π τ)]))))
  (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-Π))

tapl/tests/stlc+occurrence-tests.rkt

@@ -493,6 +493,60 @@
   (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))
+
 ;; -----------------------------------------------------------------------------
 ;; --- TODO CPS filters