diff --git a/racket/typed/core-expressions.rkt b/racket/typed/core-expressions.rkt
index 9039f00..1d317ba 100644
--- a/racket/typed/core-expressions.rkt
+++ b/racket/typed/core-expressions.rkt
@@ -17,6 +17,8 @@
          error
          define-tuple
          match-define
+         mk-tuple
+         tuple-select
          (for-syntax (all-defined-out)))
 
 (require "core-types.rkt")
@@ -164,12 +166,15 @@
      (⇒ ν-s #,(make-Branch #'((ss ...) ...)))])
 
 
+;; (Listof Value) -> Value
+(define- (mk-tuple es)
+  (#%app- cons- 'tuple es))
 
 (define-typed-syntax (tuple e:expr ...) ≫
   [⊢ e ≫ e- (⇒ : τ)] ...
   #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
   -----------------------
-  [⊢ (#%app- list- 'tuple e- ...) (⇒ : (Tuple τ ...))])
+  [⊢ (#%app- mk-tuple (#%app- list- e- ...)) (⇒ : (Tuple τ ...))])
 
 (define unit : Unit (tuple))
 
diff --git a/racket/typed/either.rkt b/racket/typed/either.rkt
index 669c7a7..cf16456 100644
--- a/racket/typed/either.rkt
+++ b/racket/typed/either.rkt
@@ -25,15 +25,16 @@
 
 (define (∀ (X Y Z) (partition/either [xs : (List X)]
                                      [pred : (→fn X (U (Left Y)
-                                                       (Right Z)) #;(Either Y Z))]
+                                                       (Right Z)))]
                                      -> (Tuple (List Y) (List Z))))
-  (for/fold ([acc (Tuple (List Y) (List Z)) (tuple (list) (list))])
+  (for/fold ([lefts (List Y) (list)]
+             [rights (List Z) (list)])
             ([x xs])
     (define y-or-z (pred x))
     (match y-or-z
       [(left (bind y Y))
-       (tuple (cons y (select 0 acc))
-              (select 1 acc))]
+       (tuple (cons y lefts)
+              rights)]
       [(right (bind z Z))
-       (tuple (select 0 acc)
-              (cons z (select 1 acc)))])))
+       (tuple lefts
+              (cons z rights))])))
diff --git a/racket/typed/for-loops.rkt b/racket/typed/for-loops.rkt
index 3d2b537..3950f85 100644
--- a/racket/typed/for-loops.rkt
+++ b/racket/typed/for-loops.rkt
@@ -15,7 +15,7 @@
 (require (only-in "set.rkt" Set ~Set))
 (require (only-in "hash.rkt" Hash ~Hash))
 (require (only-in "prim.rkt" Bool + #%datum))
-(require (only-in "core-expressions.rkt" let unit))
+(require (only-in "core-expressions.rkt" let unit tuple-select mk-tuple))
 (require "maybe.rkt")
 
 (require (postfix-in - (only-in racket/set
@@ -127,36 +127,68 @@
              #,body))]))
 
 (define-typed-syntax for/fold
-  [(for/fold ([acc:id (~optional (~datum :)) τ-acc init])
+  [(for/fold ([acc:id (~optional (~datum :)) τ-acc init] ...+)
              (clause:iter-clause
               ...)
      e-body ...+) ≫
-  [⊢ init ≫ init- (⇐ : τ-acc)]
-  #:fail-unless (pure? #'init-) "expression must be pure"
+  [⊢ init ≫ init- (⇐ : τ-acc)] ...
+  #:fail-unless (all-pure? #'(init- ...)) "expression must be pure"
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
-  [[x ≫ x-- : τ] ...
-   [acc ≫ acc- : τ-acc] ⊢ (block e-body ...) ≫ e-body-
-                           (⇐ : τ-acc)
-                           (⇒ ν-ep (~effs τ-ep ...))
-                           (⇒ ν-s (~effs τ-s ...))
-                           (⇒ ν-f (~effs τ-f ...))]
+  #:do [(define num-accs (length (syntax->list #'(τ-acc ...))))]
+  #:with body-ty (if (= 1 num-accs)
+                     (first (syntax->list #'(τ-acc ...)))
+                     (type-eval #'(Tuple (~@ τ-acc ...))))
+  [[[x ≫ x-- : τ] ...]
+   [[acc ≫ acc- : τ-acc] ...] ⊢ (block e-body ...) ≫ e-body-
+                               (⇐ : body-ty)
+                               (⇒ ν-ep (~effs τ-ep ...))
+                               (⇒ ν-s (~effs τ-s ...))
+                               (⇒ ν-f (~effs τ-f ...))]
   -------------------------------------------------------
-  [⊢ (for/fold- ([acc- init-])
-                clauses-
-                #,(bind-renames #'([x-- x-] ...) #'e-body-))
-     (⇒ : τ-acc)
+  [⊢ (values->tuple #,num-accs
+       (for/fold- ([acc- init-] ...)
+         clauses-
+         #,(bind-renames #'([x-- x-] ...) #`(tuple->values #,num-accs e-body-))))
+     (⇒ : body-ty)
      (⇒ ν-ep (τ-ep ...))
      (⇒ ν-s (τ-s ...))
      (⇒ ν-f (τ-f ...))]]
-  [(for/fold ([acc:id init])
+  [(for/fold (accs ... [acc:id init] more-accs ...)
              clauses
      e-body ...+) ≫
    [⊢ init ≫ _ (⇒ : τ-acc)]
    ---------------------------------------------------
-   [≻ (for/fold ([acc τ-acc init])
+   [≻ (for/fold (accs ... [acc τ-acc init] more-accs ...)
                 clauses
         e-body ...)]])
 
+(define-syntax-parser tuple->values
+  [(_ n:nat e:expr)
+   (define arity (syntax-e #'n))
+   (cond
+     [(= 1 arity)
+      #'e]
+     [else
+      (define/with-syntax tmp (generate-temporary 'tup))
+      (define projections
+        (for/list ([i (in-range arity)])
+          #`(#%app- tuple-select #,i tmp)))
+      #`(let- ([tmp e])
+          (#%app- values- #,@projections))])])
+
+#;(tuple->values 1 (tuple 0))
+
+(define-syntax-parser values->tuple
+  [(_ n:nat e:expr)
+   (define arity (syntax-e #'n))
+   (cond
+     [(= 1 arity)
+      #'e]
+     [else
+      (define/with-syntax (tmp ...) (generate-temporaries (make-list arity 'values->tuple)))
+      #`(let-values- ([(tmp ...) e])
+          (#%app- mk-tuple (#%app- list- tmp ...)))])])
+
 (define-typed-syntax (for/list (clause:iter-clause ...)
                        e-body ...+) ≫
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 27b3fbe..9889192 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -43,7 +43,7 @@
          ;; primitives
          (all-from-out "prim.rkt")
          ;; expressions
-         (all-from-out "core-expressions.rkt")
+         (except-out (all-from-out "core-expressions.rkt") mk-tuple tuple-select)
          ;; lists
          (all-from-out "list.rkt")
          ;; sets