diff --git a/racket/typed/scribblings/typed-syndicate.scrbl b/racket/typed/scribblings/typed-syndicate.scrbl
index 0de1f93..03aa9b8 100644
--- a/racket/typed/scribblings/typed-syndicate.scrbl
+++ b/racket/typed/scribblings/typed-syndicate.scrbl
@@ -172,6 +172,13 @@ See @racket[→].
 
 @section{User Defined Types}
 
+@defform*[[(define-type-alias id type)
+           (define-type-alias (ty-cons-id arg-id ...) type)]]{
+Define @racket[id] to be the same as @racket[type], or create a type constructor
+@racket[(ty-cons-id ty ...)] whose meaning is @racket[type] with references to
+@racket[arg-id ...] replaced by @racket[ty ...].
+}
+
 @defform[(define-constructor (ctor-id slot-id ...)
                maybe-type-ctor
                maybe-alias ...)
@@ -456,7 +463,8 @@ Instantiates the type variables @racket[X ...] with @racket[type ...], where
            (opt-res-ty (code:line)
                        (code:line arr res-type))
            (arr (code:line →) (code:line ->))]]{
-Define a constant or a (potentially polymorphic) function.
+Define a constant or a (potentially polymorphic) function. Note that the
+function name @racket[id] is @emph{not} bound in the body.
 }
 
 @defform[(define-tuple (id ...) expr)]{
@@ -489,13 +497,13 @@ Constructs a tuple of arbitrary arity.
 Extract the @racket[i]th element of a @racket[tuple].
 }
 
+@defthing[unit Unit #:value (tuple)]
+
 @defform[(error format-expr arg-expr ...)]{
 Raises an exception using @racket[format-expr] as a format string together with
 @racket[arg-expr ...].
 }
 
-@defthing[unit Unit #:value (tuple)]
-
 @deftogether[(
 @defthing[+ (→fn Int Int Int)]
 @defthing[- (→fn Int Int Int)]
@@ -533,6 +541,43 @@ Raises an exception using @racket[format-expr] as a format string together with
 Primitive operations imported from Racket.
 }
 
+@defform[#:literals (:)
+         (for/fold ([acc-id maybe-:ty acc-expr] ...+)
+                   (for-clause ...)
+           body-expr ...+)
+         #:grammar
+         [(maybe-:ty (code:line)
+                     (code:line : acc-type))
+          (for-clause (code:line [id seq-expr])
+                      (code:line [id : type seq-expr])
+                      (code:line [(k-id v-id) hash-expr])
+                      (code:line #:when test-expr)
+                      (code:line #:unless test-expr)
+                      (code:line #:break test-expr))]]{
+Similar to Racket's @racket[racket:for/fold].
+
+When more than one @racket[acc-id] is used, the body of the loop must evaluate
+to a @racket[tuple] with one value for each accumulator, with the final tuple
+also being the result of the entire expression.
+
+Each @racket[seq-expr] should be of type @racket[Sequence], though expressions
+of type @racket[List] and @racket[Set] are automatically converted.
+}
+
+@deftogether[(
+@defform[(for/list (for-clause ...) body ...+)]
+@defform[(for/set (for-clause ...) body ...+)]
+@defform[(for/sum (for-clause ...) body ...+)]
+@defform[(for (for-clause ...) body ...+)]
+@defform[(for/first (for-clause ...) body ...+)]
+)]{
+Like their Racket counterparts. See @racket[for/fold] for the description of
+@racket[for-clause].
+
+Unlike @racket[racket:for/first], @racket[for/first] returns a @racket[Maybe]
+value to indicate success/failure.
+}
+
 @section{Require & Provide}
 
 @defform[(struct-out ctor-id)]{
@@ -550,6 +595,9 @@ Primitive operations imported from Racket.
           (opaque (code:line =) (code:line >) (code:line >=))]]{
 Import and assign types to bindings from outside Typed Syndicate.
 
+Note that @emph{unlike} Typed Racket, Typed Syndicate does not attach contracts
+to imported bindings.
+
 An @racket[#:opaque] declaration defines a type @racket[type-name] (or, in the
 @racket[#:arity] case, a type constructor) that may be used to describe imports
 but otherwise has no other operations.
@@ -591,8 +639,138 @@ Constructor for a broadcast message.
 
 @subsection{Lists}
 
+@defform[(List type)]{
+The type for @racket[cons] lists whose elements are of type @racket[type].
+}
+
+@deftogether[(
+@defthing[empty (List ⊥)]
+@defthing[empty? (∀ (X) (→fn (List X) Bool))]
+@defthing[cons (∀ (X) (→fn X (List X) (List X)))]
+@defthing[cons? (∀ (X) (→fn X (List X) Bool))]
+@defthing[first (∀ (X) (→fn (List X) X))]
+@defthing[second (∀ (X) (→fn (List X) X))]
+@defthing[rest (∀ (X) (→fn (List X) (List X)))]
+@defthing[member? (∀ (X) (→fn X (List X) Bool))]
+@defthing[reverse (∀ (X) (→fn (List X) (List X)))]
+@defthing[partition (∀ (X) (→fn (List X) (→fn X Bool) (List X)))]
+@defthing[map (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))]
+@defthing[argmax (∀ (X) (→fn (→fn X Int) (List X) X))]
+@defthing[argmin (∀ (X) (→fn (→fn X Int) (List X) X))]
+@defthing[remove (∀ (X) (→fn X (List X) (List X)))]
+@defthing[length (∀ (X) (→fn (List X) Int))]
+@defform[(list e ...)]
+)]{
+Like their Racket counterparts.
+}
+
 @subsection{Sets}
 
+@defform[(Set type)]{
+The type for sets whose elements are of type @racket[type].
+}
+
+@deftogether[(
+@defform[(set e ...)]
+@defform[(set-union st ...+)]
+@defform[(set-intersect st ...+)]
+@defform[(set-subtract st ...+)]
+@defthing[set-first (∀ (X) (→fn (Set X) X))]
+@defthing[set-empty? (∀ (X) (→fn (Set X) Bool))]
+@defthing[set-count (∀ (X) (→fn (Set X) Int))]
+@defthing[set-add (∀ (X) (→fn (Set X) X (Set X)))]
+@defthing[set-remove (∀ (X) (→fn (Set X) X (Set X)))]
+@defthing[set-member? (∀ (X) (→fn (Set X) X Bool))]
+@defthing[list->set (∀ (X) (→fn (List X) (Set X)))]
+@defthing[set->list (∀ (X) (→fn (Set X) (List X)))]
+)]{
+Like their Racket counterparts.
+}
+
 @subsection{Hashes}
 
+@defform[(Hash key-type value-type)]{
+The type for key/value hash tables.
+}
+
+@deftogether[(
+@defform[(hash key val ... ...)]
+@defthing[hash-set (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
+@defthing[hash-ref (∀ (K V) (→fn (Hash K V) K V))]
+@defthing[hash-ref/failure (∀ (K V) (→fn (Hash K V) K V V))]
+@defthing[hash-empty? (∀ (K V) (→fn (Hash K V) Bool))]
+@defthing[hash-has-key? (∀ (K V) (→fn (Hash K V) K Bool))]
+@defthing[hash-count (∀ (K V) (→fn (Hash K V) Int))]
+@defthing[hash-update (∀ (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))]
+@defthing[hash-update/failure (∀ (K V) (→fn (Hash K V) K (→fn V V) V (Hash K V)))]
+@defthing[hash-remove (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
+@defthing[hash-map (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
+@defthing[hash-keys (∀ (K V) (→fn (Hash K V) (List K)))]
+@defthing[hash-values (∀ (K V) (→fn (Hash K V) (List V)))]
+@defthing[hash-union (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
+@defthing[hash-union/combine (∀ (K V) (→fn (Hash K V) (Hash K V) (→fn V V V) (Hash K V)))]
+@defthing[hash-keys-subset? (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) Bool))]
+)]{
+Like their Racket counterparts. The /failure and /combine suffixes are in place
+of keyword arguments, which Typed Syndicate does not presently support.
+}
+
+@subsection{Sequences}
+
+@defform[(Sequence type)]{
+The type for a sequence of @racket[type] values.
+}
+
+@deftogether[(
+@defthing[empty-sequence (Sequence ⊥)]
+@defthing[sequence->list (∀ (X) (→fn (Sequence X) (List X)))]
+@defthing[sequence-length (∀ (X) (→fn (Sequence X) Int))]
+@defthing[sequence-ref (∀ (X) (→fn (Sequence X) Int Int))]
+@defthing[sequence-tail (∀ (X) (→fn (Sequence X) Int (Sequence X)))]
+@defthing[sequence-append (∀ (X) (→fn (Sequence X) (Sequence X) (Sequence X)))]
+@defthing[sequence-map (∀ (A B) (→fn (→fn A B) (Sequence A) (Sequence B)))]
+@defthing[sequence-andmap (∀ (X) (→fn (→fn X Bool) (Sequence X) Bool))]
+@defthing[sequence-ormap (∀ (X) (→fn (→fn X Bool) (Sequence X) Bool))]
+@defthing[sequence-fold (∀ (A B) (→fn (→fn A B A) (Sequence B) A))]
+@defthing[sequence-count (∀ (X) (→fn (→fn X Bool) (Sequence X) Int))]
+@defthing[sequence-filter (∀ (X) (→fn (→fn X Bool) (Sequence X) (Sequence X)))]
+@defthing[sequence-add-between (∀ (X) (→fn (Sequence X) X (Sequence X)))]
+@defthing[in-list (∀ (X) (→fn (List X) (Sequence X)))]
+@defthing[in-hash-keys (∀ (K V) (→fn (Hash K V) (Sequence K)))]
+@defthing[in-hash-values (∀ (K V) (→fn (Hash K V) (Sequence V)))]
+@defthing[in-range (→fn Int (Sequence Int))]
+@defthing[in-set (∀ (X) (→fn (Set X) (Sequence X)))]
+)]{
+Like their Racket counterparts.
+}
+
+@subsection{Maybe}
+
+@deftogether[(
+@defidform[None]
+@defthing[none None]
+@defstruct[some ([v any?]) #:omit-constructor]
+@defform[(Some type)]
+@defform[(Maybe type)]
+)]{
+@racket[(Maybe type)] is an alias for @racket[(U None (Some type))].
+}
+
+@subsection{Either}
+
+@deftogether[(
+@defstruct[left ([v any?]) #:omit-constructor]
+@defform[(Left type)]
+@defstruct[right ([v any?]) #:omit-constructor]
+@defform[(Right type)]
+@defform[(Either left-type right-type)]
+)]{
+@racket[(Either left-type right-type)] is an alias for @racket[(U (Left
+left-type) (Right right-type))].
+}
+
+@defthing[partition/either (∀ (X Y Z) (→fn (List X) (→fn X (Either Y Z)) (Tuple (List Y) (List Z))))]{
+Partition a list based on a function that returns an @racket[Either] value.
+}
+
 @section{Behavioral Checking}
diff --git a/racket/typed/syndicate/either.rkt b/racket/typed/syndicate/either.rkt
index cf16456..27b9746 100644
--- a/racket/typed/syndicate/either.rkt
+++ b/racket/typed/syndicate/either.rkt
@@ -19,13 +19,8 @@
   (U (Left A)
      (Right B)))
 
-(define (∀ (X) (f [x : X] -> X))
-  x)
-
-
 (define (∀ (X Y Z) (partition/either [xs : (List X)]
-                                     [pred : (→fn X (U (Left Y)
-                                                       (Right Z)))]
+                                     [pred : (→fn X (Either Y Z))]
                                      -> (Tuple (List Y) (List Z))))
   (for/fold ([lefts (List Y) (list)]
              [rights (List Z) (list)])
diff --git a/racket/typed/syndicate/for-loops.rkt b/racket/typed/syndicate/for-loops.rkt
index 3950f85..1a8bb7a 100644
--- a/racket/typed/syndicate/for-loops.rkt
+++ b/racket/typed/syndicate/for-loops.rkt
@@ -5,9 +5,7 @@
          for/list
          for/set
          for/sum
-         for/first
-         in-hash-values
-         in-hash-keys)
+         for/first)
 
 (require "core-types.rkt")
 (require "sequence.rkt")
@@ -257,14 +255,3 @@
      (⇒ ν-ep (τ-ep ...))
      (⇒ ν-s (τ-s ...))
      (⇒ ν-f (τ-f ...))])
-
-
-(define-typed-syntax (in-hash-values h) ≫
-  [⊢ h ≫ h- (⇒ : (~Hash K V))]
-  --------------------
-  [⊢ (#%app- in-hash-values- h-) (⇒ : (Sequence V))])
-
-(define-typed-syntax (in-hash-keys h) ≫
-  [⊢ h ≫ h- (⇒ : (~Hash K V))]
-  --------------------
-  [⊢ (#%app- in-hash-keys- h-) (⇒ : (Sequence K))])
diff --git a/racket/typed/syndicate/hash.rkt b/racket/typed/syndicate/hash.rkt
index 9aad13e..8e9b0a4 100644
--- a/racket/typed/syndicate/hash.rkt
+++ b/racket/typed/syndicate/hash.rkt
@@ -45,10 +45,8 @@
   #;[make-hash : (∀ (K V) (→fn (List (ConsPair K V)) (Hash K V)))]
   [hash-set : (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
   [hash-ref : (∀ (K V) (→fn (Hash K V) K V))]
-  ;; TODO hash-ref/failure
   [hash-has-key? : (∀ (K V) (→fn (Hash K V) K Bool))]
   [hash-update : (∀ (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))]
-  ;; TODO hash-update/failure
   [hash-remove : (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
   [hash-map : (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
   [hash-keys : (∀ (K V) (→fn (Hash K V) (List K)))]
@@ -61,7 +59,6 @@
 
 (require/typed racket/hash
   [hash-union : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
-  ;; TODO - hash-union with #:combine
   )
 
 (define- (hash-ref/failure- h k err)
diff --git a/racket/typed/syndicate/list.rkt b/racket/typed/syndicate/list.rkt
index c6edf6b..1b8d305 100644
--- a/racket/typed/syndicate/list.rkt
+++ b/racket/typed/syndicate/list.rkt
@@ -3,12 +3,14 @@
 (provide List
          (for-syntax ~List)
          list
-         (typed-out [[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
+         (typed-out [[empty- : (List ⊥)] empty]
+                    [[empty?- : (∀ (X) (→fn X (List X) Bool))] empty?]
+                    [[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
+                    [[cons?- : (∀ (X) (→fn X (List X) Bool))] cons?]
                     [[first- : (∀ (X) (→fn (List X) X))] first]
                     [[second- : (∀ (X) (→fn (List X) X))] second]
                     [[rest- : (∀ (X) (→fn (List X) (List X)))] rest]
                     [[member?- (∀ (X) (→fn X (List X) Bool))] member?]
-                    [[empty?- (∀ (X) (→fn (List X) Bool))] empty?]
                     [[reverse- (∀ (X) (→fn (List X) (List X)))] reverse]
                     [[partition- (∀ (X) (→fn (List X) (→fn X Bool) (List X)))] partition]
                     [[map- (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))] map]
diff --git a/racket/typed/syndicate/sequence.rkt b/racket/typed/syndicate/sequence.rkt
index d25c232..e1dd1fc 100644
--- a/racket/typed/syndicate/sequence.rkt
+++ b/racket/typed/syndicate/sequence.rkt
@@ -17,12 +17,15 @@
          sequence-add-between
          in-list
          in-set
+         in-hash-keys
+         in-hash-values
          in-range
          )
 
 (require "core-types.rkt")
 (require (only-in "list.rkt" List))
 (require (only-in "set.rkt" Set))
+(require (only-in "hash.rkt" Hash))
 (require (only-in "prim.rkt" Int Bool))
 #;(require (postfix-in - racket/sequence))
 
@@ -50,25 +53,8 @@
 
 (require/typed racket/base
   [in-list : (∀ (X) (→fn (List X) (Sequence X)))]
+  [in-hash-keys : (∀ (K V) (→fn (Hash K V) (Sequence K)))]
+  [in-hash-values : (∀ (K V) (→fn (Hash K V) (Sequence V)))]
   [in-range : (→fn Int (Sequence Int))])
 (require/typed racket/set
   [in-set : (∀ (X) (→fn (Set X) (Sequence X)))])
-
-#;(define-typed-syntax empty-sequence
-  [_ ≫
-   --------------------
-   [⊢ empty-sequence- (⇒ : (Sequence (U)))]])
-
-;; er, this is making everything a macro, as opposed to a procedure...
-;; think I ought to add polymorphous first :\
-#;(define-typed-syntax (sequence->list s) ≫
-  [⊢ s ≫ s- (⇒ : (~Sequence τ))]
-  #:fail-unless (pure? #'s-)
-  ------------------------------
-  [⊢ (sequence->list- s-) (⇒ : (List τ))])
-
-#;(define-typed-syntax (sequence-length s) ≫
-    [⊢ s ≫ s- (⇒ : (~Sequence τ))]
-    #:fail-unless (pure? #'s-)
-    ------------------------------
-    [⊢ (sequence-length- s-) (⇒ : Int)])
diff --git a/racket/typed/syndicate/set.rkt b/racket/typed/syndicate/set.rkt
index 9863eaa..ac50b5d 100644
--- a/racket/typed/syndicate/set.rkt
+++ b/racket/typed/syndicate/set.rkt
@@ -3,19 +3,24 @@
 (provide Set
          (for-syntax ~Set)
          set
-         set-member?
-         set-add
-         set-remove
-         set-count
+         ;; set-member?
+         ;; set-add
+         ;; set-remove
+         ;; set-count
          set-union
          set-subtract
          set-intersect
-         list->set
-         set->list
-         (typed-out [[set-first- : (∀ (X) (→fn (Set X) X))]
-                     set-first]
-                    [[set-empty?- : (∀ (X) (→fn (Set X) Bool))]
-                     set-empty?]))
+         ;; list->set
+         ;; set->list
+         (typed-out [[set-first- : (∀ (X) (→fn (Set X) X))] set-first]
+                    [[set-empty?- : (∀ (X) (→fn (Set X) Bool))] set-empty?]
+                    [[set-count- : (∀ (X) (→fn (Set X) Int))] set-count]
+                    [[set-add- : (∀ (X) (→fn (Set X) X (Set X)))] set-add]
+                    [[set-remove- : (∀ (X) (→fn (Set X) X (Set X)))] set-remove]
+                    [[set-member?- : (∀ (X) (→fn (Set X) X Bool))] set-member?]
+                    [[list->set- : (∀ (X) (→fn (List X) (Set X)))] list->set]
+                    [[set->list- : (∀ (X) (→fn (Set X) (List X)))] set->list]
+                    ))
 
 (require "core-types.rkt")
 (require (only-in "prim.rkt" Int Bool))
@@ -35,38 +40,6 @@
   ---------------
   [⊢ (#%app- set- e- ...) ⇒ (Set (U τ ...))])
 
-(define-typed-syntax (set-count e) ≫
-  [⊢ e ≫ e- ⇒ (~Set _)]
-  #:fail-unless (pure? #'e-) "expression must be pure"
-  ----------------------
-  [⊢ (#%app- set-count- e-) ⇒ Int])
-
-(define-typed-syntax (set-add st v) ≫
-  [⊢ st ≫ st- ⇒ (~Set τs)]
-  #:fail-unless (pure? #'st-) "expression must be pure"
-  [⊢ v ≫ v- ⇒ τv]
-  #:fail-unless (pure? #'v-) "expression must be pure"
-  -------------------------
-  [⊢ (#%app- set-add- st- v-) ⇒ (Set (U τs τv))])
-
-(define-typed-syntax (set-remove st v) ≫
-  [⊢ st ≫ st- ⇒ (~Set τs)]
-  #:fail-unless (pure? #'st-) "expression must be pure"
-  [⊢ v ≫ v- ⇐ τs]
-  #:fail-unless (pure? #'v-) "expression must be pure"
-  -------------------------
-  [⊢ (#%app- set-remove- st- v-) ⇒ (Set τs)])
-
-(define-typed-syntax (set-member? st v) ≫
-  [⊢ st ≫ st- ⇒ (~Set τs)]
-  #:fail-unless (pure? #'st-) "expression must be pure"
-  [⊢ v ≫ v- ⇒ τv]
-  #:fail-unless (pure? #'v-) "expression must be pure"
-  #:fail-unless (<: #'τv #'τs)
-    "type mismatch"
-  -------------------------------------
-  [⊢ (#%app- set-member?- st- v-) ⇒ Bool])
-
 (define-typed-syntax (set-union st0 st ...) ≫
   [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)]
   #:fail-unless (pure? #'st0-) "expression must be pure"
@@ -91,15 +64,3 @@
   #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
   -------------------------------------
   [⊢ (#%app- set-subtract- st0- st- ...) ⇒ (Set τ-st0)])
-
-(define-typed-syntax (list->set l) ≫
-  [⊢ l ≫ l- ⇒ (~List τ)]
-  #:fail-unless (pure? #'l-) "expression must be pure"
-  -----------------------
-  [⊢ (#%app- list->set- l-) ⇒ (Set τ)])
-
-(define-typed-syntax (set->list s) ≫
-  [⊢ s ≫ s- ⇒ (~Set τ)]
-  #:fail-unless (pure? #'s-) "expression must be pure"
-  -----------------------
-  [⊢ (#%app- set->list- s-) ⇒ (List τ)])