make list operations polymorphic functions

racket/typed/for-loops.rkt

@@ -7,6 +7,7 @@
 (require (only-in "list.rkt" List ~List))
 (require (only-in "set.rkt" Set ~Set))
 (require (only-in "hash.rkt" Hash ~Hash))
+(require (only-in "prim.rkt" Bool))
 
 (begin-for-syntax
   (define-splicing-syntax-class iter-clause
@@ -89,7 +90,7 @@
      (values #`(in-set- #,e) #'t)]
     [_
      (type-error #:src e
-                 #:msg "not an iterable type: " τ)]))
+                 #:msg "not an iterable type: ~a" τ)]))
 
 
 (define-typed-syntax for/fold

racket/typed/list.rkt

@@ -3,12 +3,12 @@
 (provide List
          (for-syntax ~List)
          list
-         cons
+         (typed-out [[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
-         first
+                    [[first- : (∀ (X) (→fn (List X) X))] first]
-         rest
+                    [[rest- : (∀ (X) (→fn (List X) (List X)))] rest]
-         member?
+                    [[member?- (∀ (X) (→fn X (List X) Bool))] member?]
-         empty?
+                    [[empty?- (∀ (X) (→fn (List X) Bool))] empty?]
-         reverse)
+                    [[reverse- (∀ (X) (→fn (List X) (List X)))] reverse]))
 
 (require "core-types.rkt")
 (require (only-in "prim.rkt" Bool))
@@ -26,44 +26,5 @@
   -------------------
   [⊢ (list- e- ...) ⇒ (List (U τ ...))])
 
-(define-typed-syntax (cons e1 e2) ≫
-  [⊢ e1 ≫ e1- ⇒ τ1]
-  #:fail-unless (pure? #'e1-) "expression must be pure"
-  [⊢ e2 ≫ e2- ⇒ (~List τ2)]
-  #:fail-unless (pure? #'e2-) "expression must be pure"
-  #:with τ-l (type-eval #'(List (U τ1 τ2)))
-  ----------------------------------------
-  [⊢ (cons- e1- e2-) ⇒ τ-l])
-
-(define-typed-syntax (empty? e) ≫
-  [⊢ e ≫ e- ⇒ (~List _)]
-  #:fail-unless (pure? #'e-) "expression must be pure"
-  -----------------------
-  [⊢ (empty?- e-) ⇒ Bool])
-
-(define-typed-syntax (first e) ≫
-  [⊢ e ≫ e- ⇒ (~List τ)]
-  #:fail-unless (pure? #'e-) "expression must be pure"
-  -----------------------
-  [⊢ (first- e-) ⇒ τ])
-
-(define-typed-syntax (rest e) ≫
-  [⊢ e ≫ e- ⇒ (~List τ)]
-  #:fail-unless (pure? #'e-) "expression must be pure"
-  -----------------------
-  [⊢ (rest- e-) ⇒ (List τ)])
-
-(define-typed-syntax (member? e l) ≫
-  [⊢ e ≫ e- ⇒ τe]
-  #:fail-unless (pure? #'e-) "expression must be pure"
-  [⊢ l ≫ l- ⇒ (~List τl)]
-  #:fail-unless (pure? #'l-) "expression must be pure"
-  #:fail-unless (<: #'τe #'τl) "incompatible list"
-  ----------------------------------------
-  [⊢ (member?- e- l-) ⇒ Bool])
-
 (define- (member?- v l)
   (and- (member- v l) #t))
-
-(require/typed racket/base
-  [reverse : (∀ (X) (→fn (List X) (List X)))])

racket/typed/tests/for-loops.rkt

@@ -57,7 +57,8 @@
             : (List (Tuple Int Int))
             ⇒ (list (tuple 1 4) (tuple 2 5) (tuple 3 6)))
 
-(define (zip-even [xs : (List Int)]
+;; binding in #:when isn't handled
+#;(define (zip-even [xs : (List Int)]
                   [ys : (List Int)])
   ((inst reverse (Tuple Int Int))
    (for/fold ([acc : (List (Tuple Int Int))