diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,7 @@
 --------------------------------------------------------------------------------
 The Disciplined Disciple Compiler License (MIT style)
 
-Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force
+Copyrite (K) 2007-2016 The Disciplined Disciple Compiler Strike Force
 All rights reversed.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
diff --git a/ddc-code.cabal b/ddc-code.cabal
--- a/ddc-code.cabal
+++ b/ddc-code.cabal
@@ -1,5 +1,5 @@
 Name:           ddc-code
-Version:        0.4.2.1
+Version:        0.4.3.1
 License:        MIT
 License-file:   LICENSE
 Author:         The Disciplined Disciple Compiler Strike Force
@@ -28,11 +28,28 @@
         sea/primitive/Primitive.h
         sea/runtime/Runtime.h
 
+        tetra/base/Class/Applicative.ds
+        tetra/base/Class/Functor.ds
+        tetra/base/Class/Monad.ds
+        tetra/base/Class/Ord.ds
+        tetra/base/Class/Show.ds
+
+        tetra/base/Control/Parsec.ds
+
         tetra/base/Data/Numeric/Bool.ds
         tetra/base/Data/Numeric/Nat.ds
+        tetra/base/Data/Numeric/Word.ds
+
+        tetra/base/data/Text/Base.ds
+        tetra/base/data/Text/Char.ds
+        tetra/base/data/Text/List.ds
+        tetra/base/data/Text/Operator.ds
+        tetra/base/data/Text/Show.ds
+
         tetra/base/Data/Array.ds
         tetra/base/Data/Function.ds
         tetra/base/Data/List.ds
+        tetra/base/Data/Map.ds
         tetra/base/Data/Maybe.ds
         tetra/base/Data/Ref.ds
         tetra/base/Data/Stream.ds
@@ -46,7 +63,7 @@
 
 Library
   build-depends:
-        base            >= 4.6  &&  < 4.9,
+        base            >= 4.6  &&  < 4.10,
         filepath        >= 1.3  &&  < 1.5
 
   exposed-modules:
diff --git a/salt/runtime64/debug/Trace.dcs b/salt/runtime64/debug/Trace.dcs
--- a/salt/runtime64/debug/Trace.dcs
+++ b/salt/runtime64/debug/Trace.dcs
@@ -65,7 +65,7 @@
 
                  -- Some format that we don't handle yet, 
                  -- or the header is trashed.
-                 _      -> do   primPutString "Unknown\n"
+                 _      -> do   primPutString "Unknown\n"#
                                 0#
 
 
@@ -78,17 +78,17 @@
         format  = band# header 0x0fw32#
         tag     = shr#  header 8w32#
 
-        primPutString   "Thunk\n"
-        fieldAddr       "{   ptr     = " (takePtr# obj)
-        fieldWord32     "    format  = " format
-        fieldWord32     "    tag     = " tag
-        fieldNat        "    params  = " (paramsThunk obj)
-        fieldNat        "    boxes   = " (boxesThunk  obj)
-        fieldNat        "    args    = " (argsThunk   obj)
-        fieldNat        "    runs    = " (runsThunk   obj)
-        fieldAddr       "    fun     = " (funThunk    obj)
+        primPutString   "Thunk\n"#
+        fieldAddr       "{   ptr     = "# (takePtr# obj)
+        fieldWord32     "    format  = "# format
+        fieldWord32     "    tag     = "# tag
+        fieldNat        "    params  = "# (paramsThunk obj)
+        fieldNat        "    boxes   = "# (boxesThunk  obj)
+        fieldNat        "    args    = "# (argsThunk   obj)
+        fieldNat        "    runs    = "# (runsThunk   obj)
+        fieldAddr       "    fun     = "# (funThunk    obj)
         traceThunkPtrs obj 0#
-        primPutString   "}\n"
+        primPutString   "}\n"#
 
         case trace of
          True#  -> traceThunkPtrss obj 0#
@@ -104,11 +104,11 @@
 
          False# 
           -> do addr    = takePtr# (getThunk obj i)
-                primPutString "    arg "
+                primPutString "    arg "#
                 primPutString (primShowNat i)
-                primPutString "   = "
+                primPutString "   = "#
                 primPutString (primShowAddr addr)
-                primPutString ";\n"
+                primPutString ";\n"#
                 traceThunkPtrs obj (add# i 1#)
 
 
@@ -134,13 +134,13 @@
         tag     = shr#  header 8w32#
         arity   = peek# ptr 4#
 
-        primPutString   "Boxed\n"
-        fieldAddr       "{   ptr     = " (takePtr# obj)
-        fieldWord32     "    format  = " format
-        fieldWord32     "    tag     = " tag
-        fieldNat        "    arity   = " (promote# arity)
+        primPutString   "Boxed\n"#
+        fieldAddr       "{   ptr     = "# (takePtr# obj)
+        fieldWord32     "    format  = "# format
+        fieldWord32     "    tag     = "# tag
+        fieldNat        "    arity   = "# (promote# arity)
         traceBoxedPtrs obj (promote# arity) 0#
-        primPutString   "}\n"
+        primPutString   "}\n"#
 
         case trace of
          True#  -> traceBoxedPtrss obj (promote# arity) 0#
@@ -156,11 +156,11 @@
          False# 
           -> do addr     = takePtr# (getBoxed obj i)
 
-                primPutString "    arg "
+                primPutString "    arg "#
                 primPutString (primShowNat i)
-                primPutString "   = "
+                primPutString "   = "#
                 primPutString (primShowAddr addr)
-                primPutString ";\n"
+                primPutString ";\n"#
                 traceBoxedPtrs obj n (add# i 1#)
 
 
@@ -185,12 +185,12 @@
         tag     = shr#  header 8w32#
         size    = peek# ptr 4#
 
-        primPutString   "Raw\n"
-        fieldAddr       "{   ptr     = " (takePtr# obj)
-        fieldWord32     "    format  = " format
-        fieldWord32     "    tag     = " tag
-        fieldWord32     "    size    = " size
-        primPutString   "}\n"
+        primPutString   "Raw\n"#
+        fieldAddr       "{   ptr     = "# (takePtr# obj)
+        fieldWord32     "    format  = "# format
+        fieldWord32     "    tag     = "# tag
+        fieldWord32     "    size    = "# size
+        primPutString   "}\n"#
         0#
 
 
@@ -203,11 +203,11 @@
         format  =             band# header 0x0fw32#
         size    = shr# 4w32# (band# header 0xf0w32#)
 
-        primPutString   "Small\n"
-        fieldAddr       "{   ptr     = " (takePtr# obj)
-        fieldWord32     "    format  = " format
-        fieldWord32     "    size    = " size
-        primPutString   "}\n"
+        primPutString   "Small\n"#
+        fieldAddr       "{   ptr     = "# (takePtr# obj)
+        fieldWord32     "    format  = "# format
+        fieldWord32     "    size    = "# size
+        primPutString   "}\n"#
         0#
 
 
@@ -216,20 +216,20 @@
 fieldAddr (name: TextLit#) (val: Addr#): Void#
  = do   primPutString name
         primPutString (primShowAddr val)
-        primPutString ";\n"
+        primPutString ";\n"#
 
 
 -- | Print a Nat# field to stdout.
 fieldNat (name: TextLit#) (val: Nat#): Void#
  = do   primPutString name
         primPutString (primShowNat val)
-        primPutString ";\n"
+        primPutString ";\n"#
 
 
 -- | Print a Word32# field to stdout.
 fieldWord32 (name: TextLit#) (val: Word32#): Void#
  = do   primPutString name
         primPutString (primShowWord32 val)
-        primPutString ";\n"
+        primPutString ";\n"#
 
 
diff --git a/sea/primitive/Primitive.c b/sea/primitive/Primitive.c
--- a/sea/primitive/Primitive.c
+++ b/sea/primitive/Primitive.c
@@ -80,6 +80,11 @@
 }
 
 
+// Print a text literal to stdout.
+void primPutTextLit (string_t* str)
+{       fputs(str, stdout);
+}
+
 // Print a text vector to stdout.
 void primPutVector (Obj* obj)
 {       string_t* str = (string_t*) _payloadRaw(obj);
diff --git a/sea/primitive/Primitive.h b/sea/primitive/Primitive.h
--- a/sea/primitive/Primitive.h
+++ b/sea/primitive/Primitive.h
@@ -113,7 +113,8 @@
 
 // Other primitives -----------------------------------------------------------
 // These are defined in C land and linked into the runtime library.
-extern string_t* primShowInt   (int   i);
-extern string_t* primShowNat   (nat_t i);
-extern void      primPutString (string_t* str);
+extern string_t* primShowInt    (int   i);
+extern string_t* primShowNat    (nat_t i);
+extern void      primPutTextLit (string_t* str);
+extern void      primPutString  (string_t* str);
 
diff --git a/tetra/base/Class/Applicative.ds b/tetra/base/Class/Applicative.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Class/Applicative.ds
@@ -0,0 +1,61 @@
+
+module Class.Applicative
+export  
+{       dFunctorOfApplicative;
+        pure; ap;
+        liftA; liftA2; liftA3
+}
+import Class.Functor
+where
+
+
+-- A functor with application.
+data Applicative (f: Data -> Data) where
+        Applicative
+         :  Functor f 
+         -> ([a: Data].   a -> f a)                     -- pure
+         -> ([a b: Data]. f (a -> b) -> f a -> f b)     -- ap
+         -> Applicative f
+
+
+-- | Take the Functor dictionary from an Applicative dictionary.
+dFunctorOfApplicative 
+        : [f: Data -> Data]
+        . Applicative f -> Functor f
+
+dFunctorOfApplicative (Applicative dFunctor _ _)
+ = dFunctor
+
+
+-- | Return a value in the carrier.
+pure    : [f: Data -> Data]. [a: Data]
+        . Applicative f -> a -> f a
+
+pure    (Applicative _ pure' _) x
+ = pure' x
+
+
+-- | Apply a function in the carrier its argument in another carrier.
+ap      : [f: Data -> Data]. [a b: Data]
+        . Applicative f -> f (a -> b) -> f a -> f b
+
+ap      (Applicative _ _ ap') xfab xfa
+ = ap' xfab xfa
+
+
+-- Lifting functions.
+liftA   (dapp: Applicative f) (f: a -> b) (xa: f a): f b
+ = ap dapp (pure dapp f) xa
+
+
+liftA2  (dapp: Applicative f)
+        (f: a -> b -> c) (xa: f a) (xb: f b): f c
+ = let  dfun    = dFunctorOfApplicative dapp
+   in   ap dapp (fmap dfun f xa) xb
+
+
+liftA3  (dapp: Applicative f) 
+        (f: a -> b -> c -> d) (xa: f a) (xb: f b) (xc: f c): f d
+ = let  dfun    = dFunctorOfApplicative dapp
+   in   ap dapp (ap dapp (fmap dfun f xa) xb) xc
+
diff --git a/tetra/base/Class/Functor.ds b/tetra/base/Class/Functor.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Class/Functor.ds
@@ -0,0 +1,19 @@
+
+module  Class.Functor 
+export  fmap
+where
+
+
+-- | Class of collection types that can be mapped over.
+data Functor (f: Data -> Data) where
+        Functor
+         :  ([a b: Data]. (a -> b) -> f a -> f b)       -- fmap
+         -> Functor f
+
+
+-- | Apply a function to values of type 'a' in the input collection.
+fmap    : [f: Data -> Data]. [a b: Data]
+        . Functor f -> (a -> b) -> f a -> f b
+
+fmap (Functor fmap') = fmap'
+
diff --git a/tetra/base/Class/Monad.ds b/tetra/base/Class/Monad.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Class/Monad.ds
@@ -0,0 +1,54 @@
+
+module Class.Monad
+export  
+{       dFunctorOfMonad; dApplicativeOfMonad;
+        return; bind
+}
+import Class.Functor
+import Class.Applicative
+where
+
+
+-- | Class of types that support associative sequencing.
+data Monad (m: Data -> Data) where
+        Monad
+         :  Applicative m
+         -> ([a: Data].   a   -> m a)                   -- return
+         -> ([a b: Data]. m a -> (a -> m b) -> m b)     -- bind
+         -> Monad m
+
+
+-- | Take the Functor dictionary from a Monad dictionary.
+dFunctorOfMonad 
+        : [m: Data -> Data]
+        . Monad m -> Functor m
+
+dFunctorOfMonad dMonad
+        = dFunctorOfApplicative (dApplicativeOfMonad dMonad)
+
+
+-- | Take the Applicative dictionary from a Monad dictionary.
+dApplicativeOfMonad
+        : [m: Data -> Data]
+        . Monad m -> Applicative m
+
+dApplicativeOfMonad (Monad dApplicative _ _)
+        = dApplicative
+
+
+-- | Return a value in a monad.
+return  : [m: Data -> Data]. [a: Data]
+        . Monad m -> a -> m a
+
+return (Monad _ return' _) x
+ = return' x
+
+
+-- | Evaluate a monadic compuation and pass the result to 
+--   a function that produces a new monadic computation.
+bind    : [m: Data -> Data]. [a b: Data]
+        . Monad m -> m a -> (a -> m b) -> m b
+
+bind    (Monad _ _ bind') ma mf 
+ = bind' ma mf
+
diff --git a/tetra/base/Class/Ord.ds b/tetra/base/Class/Ord.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Class/Ord.ds
@@ -0,0 +1,14 @@
+
+module Class.Ord
+where
+
+
+data Ordering where
+        LT      : Ordering
+        GT      : Ordering
+        EQ      : Ordering
+
+
+data Ord (k: Data) where
+        Ord     : (k -> k -> Ordering) -> Ord k
+
diff --git a/tetra/base/Class/Show.ds b/tetra/base/Class/Show.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Class/Show.ds
@@ -0,0 +1,48 @@
+
+module Class.Show
+export
+{       show; show_bool; show_nat;
+        show_text;
+        show_tup2;
+        show_list;
+}
+import Data.Text
+import Data.List
+where
+
+
+-- | Class dictionary for Show.
+data Show (a: Data) where
+        Show    : (a -> Text) -> Show a
+
+show ((Show sh): Show a) (x: a): Text
+ = sh x
+
+
+-------------------------------------------------------------------------------
+-- Instances for basic types.
+-- We define these in this module to avoid making it recursive
+-- with the modules that define basic data types.
+show_bool       = Show showBool
+show_nat        = Show showNat
+
+
+-- ISSUE: #381: Escape non-printable characters in base Show library.
+show_text: Show Text
+ = Show sh
+ where  sh tx           = "\"" % tx % "\""
+
+
+show_tup2 ((Show sh_a): Show a) ((Show sh_b): Show b)
+        : Show (Tup2 a b)
+ = Show sh
+ where  
+        sh (T2 x y)     = parens $ "T2" %% sh_a x %% sh_b y
+
+
+show_list ((Show sh_a): Show a): Show (List a)
+ = Show sh
+ where  
+        sh Nil          = "Nil"
+        sh (Cons x xs)  = parens $ "Cons" %% sh_a x %% sh xs
+
diff --git a/tetra/base/Control/Parsec.ds b/tetra/base/Control/Parsec.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Control/Parsec.ds
@@ -0,0 +1,166 @@
+
+module Control.Parsec
+export  
+{       parse; zero; item; satisfies;
+        from; alt;
+        monad_Parser;
+        some; many;
+}
+import Class.Monad
+import Data.List
+import Data.Tuple
+import Data.Maybe
+where
+
+data Parser (t a: Data) where
+        Parser: (List t → List (Tup2 a (List t))) → Parser t a
+
+
+-- | Apply a parser to a list of input tokens.
+parse ((Parser p): Parser t a) (ts: List t): List (Tup2 a (List t))
+ = p ts
+
+
+-- Functor --------------------------------------------------------------------
+functor_Parser [t: Data]: Functor (Parser t)
+ = Functor parser_fmap
+
+ where  parser_fmap [t a b: Data] (f: a → b) (parserA: Parser t a): Parser t b
+         = Parser $ λts
+         → for (parse parserA ts) $ λ(T2 resultA ts2)
+         → T2  (f resultA) ts2
+
+
+-- Applicative ----------------------------------------------------------------
+applicative_Parser [t: Data]: Applicative (Parser t)
+ = Applicative 
+        functor_Parser
+        parser_pure
+        parser_ap
+
+ where  parser_pure (x: a): Parser t' a
+         = Parser $ λts → Cons (T2 x ts) Nil
+
+        parser_ap   (parserF: Parser t' (a → b))
+                    (parserA: Parser t' a)
+                    : Parser t' b
+         = Parser $ λts → concat
+         $ for (parse parserF ts)  $ λ(T2 resultF ts2)
+         → for (parse parserA ts2) $ λ(T2 resultA ts3)
+         → T2 (resultF resultA) ts3
+
+
+-- Monad ----------------------------------------------------------------------
+monad_Parser [t: Data]: Monad (Parser t)
+ = Monad applicative_Parser
+         parser_return
+         parser_bind
+
+ where  parser_return (x: a): Parser t' a
+         = Parser $ λts → Cons (T2 x ts) Nil
+
+        parser_bind
+                (parserA:   Parser t' a)
+                (mkParserB: a → Parser t' b)
+                : Parser t' b
+         = Parser $ λts → concat  
+         $ for (parse parserA ts)              $ λ(T2 resultA ts2)
+         → for (parse (mkParserB resultA) ts2) $ λ(T2 resultB ts3)
+         → T2 resultB ts3
+
+
+-------------------------------------------------------------------------------
+-- | Always fail, producing no possible parses.
+zero: Parser t a
+ = Parser $ λ_ → Nil
+
+
+-- | Consume the first input token, failing if there aren't any.
+item: Parser t t
+ = Parser $ λts
+ → case ts of
+        Nil             → Nil
+        Cons t ts'      → Cons (T2 t ts) Nil
+
+
+-- | A parser that accepts a single token that satisfies the given predicate,
+--   producing the given value if it matches.
+satisfies (pred: t → Bool): Parser t t
+ = Parser $ λts
+ → case ts of
+        Nil            → Nil
+        Cons t ts
+         | pred t      → Cons (T2 t ts) Nil
+         | otherwise   → Nil
+
+
+-- | Use the given function to check whether to accept the next token,
+--   returning the result that it produces.
+from (accept: t → Maybe a): Parser t a
+ = Parser $ λts
+ → case ts of
+        Nil            → Nil
+        Cons t ts'
+         → case accept t of
+               Nothing → Nil
+               Just x  → Cons (T2 x ts') Nil
+
+
+-- | Combine two argument parsers, producing a new one that accepts
+--   strings parsed by either of the argument parsers.
+plus (parserA parserB: Parser t a): Parser t a
+ = Parser $ λts 
+ → append (parse parserA ts) (parse parserB ts)
+
+
+-- | Combine two argument parsers, producing a new one that accepts
+--   strings parser by either of the argument parser, but not both.
+--   We prefer result produced by the first parser over the second.
+alt (parserA parserB: Parser t a): Parser t a
+ = Parser $ λts
+ → case parse parserA ts of
+        Nil    → parse parserB ts
+        res    → res
+
+
+-- | Combine a list of argument parsers, producing a new one that
+--   gives the result produced by the first matching argument parser.
+alts (parsers: List (Parser t a)): Parser t a
+ = case parsers of
+        Nil             → zero
+        Cons p ps       → alt p (alts ps)
+
+
+-- | Like `alts`, accept use the given default parser if no 
+--   parser from the first list succeeds.
+altss (parsers: List (Parser t a)) (def: Parser t a): Parser t a
+ = case parsers of
+        Nil             → def
+        Cons p ps       → alt p (altss ps def)
+
+
+-- | Apply a parser followed by another parser,
+--   producing a tuple that contains both results.
+follows (parserA: Parser t a) (parserB: Parser t b): Parser t (Tup2 a b)
+ = Parser $ λts → concat
+ $ for (parse parserA ts)  $ λ(T2 resultA ts2)
+ → for (parse parserB ts2) $ λ(T2 resultB ts3)
+ → T2 (T2 resultA resultB) ts3
+
+
+-- | Parse zero or more things, yielding a list of those things.
+some (parserA: Parser t a): Parser t (List a)
+ = alt  (bind   monad_Parser parserA        $ λx  → 
+         bind   monad_Parser (some parserA) $ λxs →
+         return monad_Parser (Cons x xs))
+        (return monad_Parser Nil)
+
+
+-- | Parse one or more things, yielding a list of those things.
+many [a t: Data] (parserA: Parser t a): Parser t (List a)
+ = alt  (bind   monad_Parser parserA        $ λx  →
+         bind   monad_Parser (some parserA) $ λxs →
+         return monad_Parser (Cons x xs))
+        (bind   monad_Parser parserA        $ λx  →
+         return monad_Parser (Cons x Nil))
+
diff --git a/tetra/base/Data/Array.ds b/tetra/base/Data/Array.ds
--- a/tetra/base/Data/Array.ds
+++ b/tetra/base/Data/Array.ds
@@ -1,11 +1,17 @@
 
 module Data.Array
-export { allocArray; readArray; writeArray }
+export { allocArray; readArray; writeArray; }
+import Data.Numeric.Nat
 
 import foreign boxed type
  Array : Region ~> Data ~> Data
 
 import foreign c value
+ -- ISSUE #377: Use type equations during Tetra to Salt transform.
+ -- The Tetra to Salt transform isn't looking through type equations,
+ -- so types of primitives that use type synonyms break. Eg if we use
+ -- 'Nat' here instead of 'Nat#' the transform won't know these primtives
+ -- accept unboxed values.
  allocArray : [r: Region]. [a: Data]. Nat# -> a -> S (Alloc r) (Array r a)
  readArray  : [r: Region]. [a: Data]. Array r a -> Nat# -> S (Read r) a
  writeArray : [r: Region]. [a: Data]. Array r a -> Nat# -> a -> S (Write r) Void#
diff --git a/tetra/base/Data/Function.ds b/tetra/base/Data/Function.ds
--- a/tetra/base/Data/Function.ds
+++ b/tetra/base/Data/Function.ds
@@ -1,6 +1,6 @@
 
 module  Data.Function
-export  { id; apply; compose }
+export  { id; apply; compose; }
 where
 
 
@@ -18,5 +18,5 @@
 -- | Compose two functions.
 --   The operator '∘' is desugared to applications of this function.
 compose [a b c: Data] (f: b -> c) (g: a -> b): a -> c
- = λx : a. f (g x)
+ = λ(x : a) -> f (g x)
 
diff --git a/tetra/base/Data/List.ds b/tetra/base/Data/List.ds
--- a/tetra/base/Data/List.ds
+++ b/tetra/base/Data/List.ds
@@ -1,22 +1,30 @@
 
 module Data.List 
-export  { singleton;    replicate
-        ; enumFromTo
-        ; append
-        ; length
-        ; head
-        ; tail; tail1
-        ; last; index
-        ; reverse 
-        ; map;    mapS
-        ; forS
-        ; zipWith; zipWithS
-        ; foldl;  foldlS;       sum;    prod
-        ; foldr;  foldrS
-        ; scanl
-        ; filter; filterS
-        ; any }
+export
+{       singleton;  replicate;
+        enumFromTo; append; concat;
+        length;
+        head;
+        tail; tail1;
+        last; index;
+        lookupBy; find;
+        reverse;
+        map; mapS; for;
+        forS;
+        zipWith; zipWithS;
+        foldl;  foldlS;       sum;    prod;
+        foldr;  foldrS;
+        scanl;
+        filter; filterS;
+        any;
+}
 import  Data.Numeric.Nat
+import  Data.Numeric.Bool
+import  Data.Tuple
+import  Data.Maybe
+import  Data.Function
+import  Class.Functor
+import  Class.Monad
 where
 
 -- | Standard Cons-lists.
@@ -33,13 +41,13 @@
 
 -- | Construct a list of the given length where all elements are'
 --   the same value.
-replicate (n: Nat#) (x: a): List a
+replicate (n: Nat) (x: a): List a
  | n == 0       = Nil
  | otherwise    = Cons x (replicate (n - 1) x)
 
 
 -- | Construct a range of values.
-enumFromTo (start: Nat#) (end: Nat#): List Nat#
+enumFromTo (start: Nat) (end: Nat): List Nat
  | start >= end = singleton start
  | otherwise    = Cons start (enumFromTo (start + 1) end)
 
@@ -51,9 +59,35 @@
         Cons x xs       -> Cons x (append xs yy)
 
 
+-- | Concatenate a list of lists.
+concat (xss0: List (List a)): List a
+ = case xss0 of
+        Nil             -> Nil
+        Cons xs xss1    -> go xs xss1
+ where
+        go Nil         Nil              = Nil
+        go Nil         (Cons xs' xss')  = go xs' xss'
+        go (Cons x xs) xss              = Cons x (go xs xss)
+
+
+-- | Generate a list of the given length by repeatedly 
+--   applying a stateful function.
+unfold   (s0: s) (f: s -> Maybe (Tup2 a s)): List a
+ = case f s0 of
+        Nothing         -> Nil
+        Just (T2 a s1)  -> Cons a (unfold s1 f)
+
+
+generate (len: Nat) (f: Nat -> a): List a
+ = unfold 0
+ $ (\ix -> if ix >= len 
+                then Nothing
+                else Just (T2 (f ix) (ix + 1)))
+
+
 -- Projections ----------------------------------------------------------------
 -- | Take the length of a list.
-length (xx: List a): Nat#
+length (xx: List a): Nat
  = case xx of
         Nil             -> 0
         Cons x xs       -> 1 + length xs
@@ -77,23 +111,19 @@
 tail1   (def: a) (xx: List a): List a
  = case xx of
         Nil             -> singleton def
-        Cons x xs        
-         -> case xs of
-                Nil     -> singleton x
-                _       -> xs
+        Cons x Nil      -> singleton x
+        Cons _ xs       -> xs
 
 
 -- | Take the last element of a list, if there is one.
 last (def: a) (xx: List a): a
  = case xx of
         Nil                     -> def
-        Cons x xs
-         -> case xs of
-                Nil             -> x
-                Cons y ys       -> last def xs
+        Cons x Nil              -> x
+        Cons x (Cons y ys)      -> last def (Cons y ys)
 
 
-index (def: a) (n: Nat#) (xx: List a): a
+index (def: a) (n: Nat) (xx: List a): a
  = case xx of   
         Nil     -> def
         Cons x xs 
@@ -102,6 +132,26 @@
                 _       -> index def (n - 1) xs
 
 
+-- Searches -------------------------------------------------------------------
+-- | Given a list of key value pairs, lookup the first
+--   value whose key is selected by the given predicate.
+lookupBy (f: a -> Bool) (xx: List (Tup2 a b)): Maybe b
+ = case xx of
+        Nil             -> Nothing
+        Cons (T2 x y) xs
+         | f x          -> Just y
+         | otherwise    -> lookupBy f xs
+
+
+-- | Find the first element in a list that matches the given predicate.
+find (f: a -> Bool) (xx: List a): Maybe a
+ = case xx of
+        Nil             -> Nothing
+        Cons x xs
+         | f x          -> Just x
+         | otherwise    -> find f xs
+
+
 -- Transforms -----------------------------------------------------------------
 -- | Reverse the elements of a list.
 --   This is a naive O(n^2) version for testing purposes.
@@ -119,6 +169,18 @@
         Cons x xs       -> Cons (f x) (map f xs)
 
 
+-- | Like `map`, but with the arguments swapped.
+for     (xx: List a) (f: a -> b): List b
+ = case xx of
+        Nil             -> Nil
+        Cons x xs       -> Cons (f x) (for xs f)
+
+
+-- | Functor instance for List.
+functor_list 
+ = Functor map
+
+
 -- | Apply a stateful worker function to every element of a list,
 --   yielding a new list. 
 --   The worker is applied to the source elements left-to-right.
@@ -137,29 +199,37 @@
                 forS xs f
 
 
--- Zips -----------------------------------------------------------------------
-zipWith (f: a -> b -> c) 
-        (xx: List a) (yy: List b): List c
+-- | Monadic map.
+mapM    (dMonad: Monad m) 
+        (f: a -> m b) (xx: List a): m (List b)
  = case xx of
-        Nil     -> Nil
+        Nil    
+         -> return dMonad Nil
+
         Cons x xs
-         -> case yy of
-                Cons y ys
-                 -> Cons (f x y) (zipWith f xs ys)
+         -> bind   dMonad (f x)              $ λx'
+         -> bind   dMonad (mapM dMonad f xs) $ λxs'
+         -> return dMonad (Cons x' xs')
 
-                Nil -> Nil
 
+-- Zips -----------------------------------------------------------------------
+zipWith (f: a -> b -> c) 
+        (xx: List a) (yy: List b): List c
+ = case T2 xx yy of
+        T2 Nil _                -> Nil
+        T2 (Cons x xs) Nil      -> Nil
+        T2 (Cons x xs) (Cons y ys)
+         -> Cons (f x y) (zipWith f xs ys)
 
+
+-- | Stateful zipWith.
 zipWithS (f: a -> b -> S e c) 
          (xx: List a) (yy: List b): S e (List c)
- = case xx of
-        Nil     -> Nil
-        Cons x xs
-         -> case yy of
-                Cons y ys
-                 -> Cons (f x y) (zipWithS f xs ys)
-
-                Nil -> Nil
+ = case T2 xx yy of
+        T2 Nil _                -> Nil
+        T2 (Cons x xs) Nil      -> Nil
+        T2 (Cons x xs) (Cons y ys)
+         -> Cons (f x y) (zipWithS f xs ys)
 
 
 -- Folds ----------------------------------------------------------------------
@@ -196,15 +266,20 @@
 
 
 -- | Take the sum of a list of Nats.
-sum (xs: List Nat#): Nat#
+sum (xs: List Nat): Nat
  = foldl (+) 0 xs
 
 
 -- | Take the product of a list of Nats.
-prod (xs: List Nat#): Nat#
+prod (xs: List Nat): Nat
  = foldl (*) 1 xs
 
 
+-- | Monadic sequence.
+sequence (dMonad: Monad m) (xs: List (m a)): m (List a)
+ = mapM dMonad id xs
+
+
 -- Scans ----------------------------------------------------------------------
 scanl (f: b -> a -> b) (acc: b) (xx: List a): List b
  = case xx of
@@ -218,31 +293,28 @@
 
 -- Filters --------------------------------------------------------------------
 -- | Keep only those elements that match the given predicate.
-filter (p: a -> Bool#) (xx: List a): List a
+filter (p: a -> Bool) (xx: List a): List a
  = case xx of
         Nil             -> Nil
         Cons x xs  
-         -> if p x 
-                then Cons x (filter p xs)
-                else filter p xs
+         | p x          -> Cons x (filter p xs)
+         | otherwise    -> filter p xs
 
 
 -- | Keep only those elements that match the given stateful predicate.
 --   The predicate is applied to the list elements from left to right.
-filterS (p: a -> S e Bool#) (xx: List a): S e (List a)
+filterS (p: a -> S e Bool) (xx: List a): S e (List a)
  = case xx of
         Nil             -> Nil
         Cons x xs  
-         -> if p x 
-                then Cons x (filterS p xs)
-                else filterS p xs
+         | p x          -> Cons x (filterS p xs)
+         | otherwise    -> filterS p xs
 
 
 -- | Check if any of the members of the list match the given predicate.
-any (p: a -> Bool#) (xx: List a): Bool#
+any (p: a -> Bool) (xx: List a): Bool
  = case xx of
-        Nil
-         -> False
+        Nil             -> False
 
         Cons x xs 
          | p x          -> True
diff --git a/tetra/base/Data/Map.ds b/tetra/base/Data/Map.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Data/Map.ds
@@ -0,0 +1,325 @@
+
+module Data.Map
+export  
+{       map_empty;  map_singleton;
+        map_null;   map_size;
+        map_lookup; map_member;
+        map_insert; map_insertWithKey;
+        map_foldr;  map_foldrWithKey; map_foldlWithKey;
+        map_fromList;
+        map_toList; map_toAscList; map_toDescList;
+        show_map;
+}
+import Data.Numeric.Nat
+import Data.Numeric.Bool
+import Data.Text
+import Data.Maybe
+import Data.List
+import Data.Tuple
+import Class.Ord
+import Class.Show
+where
+
+
+-- | A map from keys @k@ to values @a@.
+data Map (k a: Data) where
+        Bin : Size -> k -> a -> Map k a -> Map k a -> Map k a
+        Tip : Map k a
+
+
+type Size = Nat
+
+
+show_map (show_k: Show k) (show_a: Show a): Show (Map k a)
+ = Show sh
+ where  
+        sh (Bin s k a l r)
+         = parens $ "Bin"
+                %% show show_nat s
+                %% show show_k   k
+                %% show show_a   a
+                %% show (show_map show_k show_a) l
+                %% show (show_map show_k show_a) r
+
+        sh Tip
+         = "Tip"
+
+
+-- Construction -----------------------------------------------------------------------------------
+-- | O(1). The empty map.
+map_empty : Map k a
+ = Tip
+
+
+-- | O(1). A map with a single element.
+map_singleton (k: k) (x: a) : Map k a
+ = Bin 1 k x Tip Tip
+
+
+-- Query ------------------------------------------------------------------------------------------
+-- | /O(1)/. Is the map empty?
+--
+-- > Data.Map.null (empty)           == True
+-- > Data.Map.null (singleton 1 'a') == False
+map_null (mp: Map k a): Bool
+ = case mp of
+        Tip             -> True
+        Bin _ _ _ _ _   -> False
+
+
+-- | /O(1)/. The number of elements in the map.
+--
+-- > size empty                                   == 0
+-- > size (singleton 1 'a')                       == 1
+-- > size (fromList([(1,'a'), (2,'c'), (3,'b')])) == 3
+map_size (mp: Map k a): Size
+ = case mp of
+        Tip             -> 0
+        Bin sz _ _ _ _  -> sz
+  
+
+-- | /O(log n)/. Lookup the value at a key in the map.
+--
+-- The function will return the corresponding value as @('Just' value)@,
+-- or 'Nothing' if the key isn't in the map.
+map_lookup ((Ord compare): Ord k) (kx: k) (mp: Map k a): Maybe a
+ = go kx mp
+ where  
+        go _ Tip 
+         = Nothing [a]
+
+        go k (Bin _ kx x l r)
+         = case compare k kx of
+                LT -> go k l
+                GT -> go k r
+                EQ -> Just x
+
+
+-- | /O(log n)/. Is the key a member of the map?
+--
+-- > member 5 (fromList [(5,'a'), (3,'b')]) == True
+-- > member 1 (fromList [(5,'a'), (3,'b')]) == False
+--
+map_member ((Ord compare): Ord k) (kx: k) (mp: Map k a): Bool
+ = go kx mp
+ where  
+        go _ Tip 
+         = False
+
+        go k (Bin _ kx _ l r)
+         = case compare k kx of
+                LT -> go k l
+                GT -> go k r
+                EQ -> True
+
+
+-- Insertion --------------------------------------------------------------------------------------
+-- | /O(log n)/. Insert a new key and value in the map.
+--   If the key is already present in the map, the associated value is
+--   replaced with the supplied value. 'insert' is equivalent to
+--   @'insertWith' 'const'@.
+--
+-- > insert 5 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'x')]
+-- > insert 7 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'a'), (7, 'x')]
+-- > insert 5 'x' empty                         == singleton 5 'x'
+--
+map_insert
+        ((Ord compare): Ord k) 
+        (kx0: k) (x0: a) (mp: Map k a): Map k a
+ = go kx0 x0 mp
+ where
+        go kx x Tip 
+         = map_singleton kx x
+
+        go kx x (Bin sz ky y l r)
+         = case compare kx ky of
+                LT -> map_balance ky y (go kx x l) r
+                GT -> map_balance ky y l (go kx x r)
+                EQ -> Bin sz kx x l r
+
+
+-- | /O(log n)/. Insert with a function, combining new value and old value.
+--   @'insertWith' f key value mp@
+--   will insert the pair (key, value) into @mp@ if key does
+--   not exist in the map. If the key does exist, the function will
+--   insert the pair @(key, f new_value old_value)@.
+--
+map_insertWith
+        (ord: Ord k)
+        (f: a -> a -> a)
+        (kx: k) (x: a) (mp: Map k a)
+        : Map k a
+ = map_insertWithKey ord
+        (\_ x' y' -> f x' y')
+        kx x mp
+
+
+-- | /O(log n)/. Insert with a function, combining key, new value and old value.
+--   @'insertWithKey' f key value mp@
+--   will insert the pair (key, value) into @mp@ if key does
+--   not exist in the map. If the key does exist, the function will
+--   insert the pair @(key,f key new_value old_value)@.
+--   Note that the key passed to f is the same key passed to 'insertWithKey'.
+--
+map_insertWithKey
+        ((Ord compare): Ord k)
+        (f: k -> a -> a -> a)
+        (kx: k) (x: a) (mp: Map k a)
+        : Map k a
+ = go kx x mp
+ where
+        go kx x Tip
+         = map_singleton kx x
+
+        go kx x (Bin sy ky y l r)
+         = case compare kx ky of
+                LT -> map_balance ky y (go kx x l) r
+                GT -> map_balance ky y l (go kx x r)
+                EQ -> Bin sy kx (f kx x y) l r
+
+
+-- Folds ------------------------------------------------------------------------------------------
+-- | /O(n)/. Fold the values in the map using the given right-associative
+--   binary operator.
+--
+map_foldr (f: a -> b -> b) (z: b) (mp: Map k a): b
+ = go z mp
+ where
+        go z' Tip             = z'
+        go z' (Bin _ _ x l r) = go (f x (go z' r)) l
+
+
+-- | /O(n)/. Fold the keys and values in the map using the given right-associative
+--   binary operator..
+--
+map_foldrWithKey (f: k -> a -> b -> b) (z: b) (mp: Map k a): b
+ = go z mp
+ where
+        go z' Tip              = z'
+        go z' (Bin _ kx x l r) = go (f kx x (go z' r)) l
+
+
+-- | /O(n)/. Fold the keys and values in the map using the given left-associative
+-- binary operator.
+map_foldlWithKey (f: a -> k -> b -> a) (z: a) (mp: Map k b): a
+ = go z mp
+ where  go z' Tip              = z'
+        go z' (Bin _ kx x l r) = go (f (go z' l) kx x) r
+
+
+-- Conversion -------------------------------------------------------------------------------------
+map_fromList 
+        (ord: Ord k)
+        (xx: List (Tup2 k a))
+        : Map k a
+ = foldl (λ  mp tp
+          -> case tp of
+                 T2 kx x -> map_insert ord kx x mp)
+         map_empty xx
+
+
+-- | /O(n)/. Convert the map to a list of key\/value pairs. 
+map_toList (mp: Map k a): List (Tup2 k a)
+        = map_toAscList mp
+
+
+-- | /O(n)/. Convert the map to a list of key\/value pairs where the
+--   keys are in ascending order. 
+map_toAscList (mp: Map k a): List (Tup2 k a)
+        = map_foldrWithKey (λk x xs -> Cons (T2 k x) xs) Nil mp
+
+
+-- | /O(n)/. Convert the map to a list of key\/value pairs where the
+--   keys are in descending order.
+map_toDescList (mp: Map k a): List (Tup2 k a)
+        = map_foldlWithKey (λxs k x -> Cons (T2 k x) xs) Nil mp
+
+
+---------------------------------------------------------------------------------------------------
+-- [balance l x r] balances two trees with value x.
+--  The sizes of the trees should balance after decreasing the
+--  size of one of them. (a rotation).
+--
+--  [delta] is the maximal relative difference between the sizes of
+--          two trees, it corresponds with the [w] in Adams' paper.
+--
+--  [ratio] is the ratio between an outer and inner sibling of the
+--          heavier subtree in an unbalanced setting. It determines
+--          whether a double or single rotation should be performed
+--          to restore balance. It is corresponds with the inverse
+--          of $\alpha$ in Adam's article.
+--
+--  Note that according to the Adam's paper:
+--  - [delta] should be larger than 4.646 with a [ratio] of 2.
+--  - [delta] should be larger than 3.745 with a [ratio] of 1.534.
+--
+--  But the Adam's paper is erroneous:
+--  - It can be proved that for delta=2 and delta>=5 there does
+--    not exist any ratio that would work.
+--  - Delta=4.5 and ratio=2 does not work.
+--
+--  That leaves two reasonable variants, delta=3 and delta=4,
+--  both with ratio=2.
+--
+--  - A lower [delta] leads to a more 'perfectly' balanced tree.
+--  - A higher [delta] performs less rebalancing.
+--
+--  In the benchmarks, delta=3 is faster on insert operations,
+--  and delta=4 has slightly better deletes. As the insert speedup
+--  is larger, we currently use delta=3.
+--
+--  NOTE: The Haskell implementation from the containers package
+--  contains an unfolded version of balance to optimise pattern 
+--  matching, but there is no point using that until we have the
+--  same sort of pattern matching compiler optimisations as GHC.
+-- 
+delta   = 2
+ratio   = 5
+
+
+map_balance (k: k) (x: a) (l: Map k a) (r: Map k a): Map k a
+ = let  sizeL = map_size l in
+   let  sizeR = map_size r in
+   let  sizeX = sizeL + sizeR + 1 
+   in   match
+         | sizeL + sizeR <= 1    = Bin sizeX k x l r
+         | sizeR > delta*sizeL   = rotateL k x l r
+         | sizeL > delta*sizeR   = rotateR k x l r
+         | otherwise             = Bin sizeX k x l r
+
+
+rotateL (k: k) (x: a)
+        (l: Map k a) (r@(Bin _ _ _ ly ry): Map k a)
+        : Map k a
+ | map_size ly < ratio*map_size ry = singleL k x l r
+ | otherwise                       = doubleL k x l r
+
+
+rotateR (k: k) (x: a)
+        (l@(Bin _ _ _ ly ry): Map k a) (r: Map k a)
+        : Map k a
+ | map_size ry < ratio*map_size ly = singleR k x l r
+ | otherwise                       = doubleR k x l r
+
+
+singleL (k1: k) (x1: a) (t1: Map k a) (tR: Map k a): Map k a
+ | Bin _ k2 x2 t2 t3 <- tR
+ = bin k2 x2 (bin k1 x1 t1 t2) t3
+
+singleR (k1: k) (x1: a) (tL: Map k a) (t3: Map k a): Map k a
+ | Bin _ k2 x2 t1 t2 <- tL
+ = bin k2 x2 t1 (bin k1 x1 t2 t3)
+
+doubleL (k1: k) (x1: a) (t1: Map k a) (tR: Map k a): Map k a
+ | Bin _ k2 x2 (Bin _ k3 x3 t2 t3) t4 <- tR
+ = bin k3 x3 (bin k1 x1 t1 t2) (bin k2 x2 t3 t4)
+
+doubleR (k1: k) (x1: a) (tL: Map k a) (t4: Map k a): Map k a
+ | Bin _ k2 x2 t1 (Bin _ k3 x3 t2 t3) <- tL
+ = bin k3 x3 (bin k2 x2 t1 t2) (bin k1 x1 t3 t4)
+
+
+-- | The bin constructor maintains the size of the tree
+bin (k: k) (x: a) (l: Map k a) (r: Map k a): Map k a
+ = Bin (map_size l + map_size r + 1) k x l r
+
diff --git a/tetra/base/Data/Maybe.ds b/tetra/base/Data/Maybe.ds
--- a/tetra/base/Data/Maybe.ds
+++ b/tetra/base/Data/Maybe.ds
@@ -1,6 +1,10 @@
 
 module Data.Maybe
 export  { isNothing; isJust; fromMaybe }
+import Class.Functor
+import Class.Applicative
+import Class.Monad
+import Data.Numeric.Bool
 where
 
 
@@ -10,20 +14,73 @@
         Just    : a -> Maybe a
 
 
+-- Functor --------------------------------------------------------------------
+functor_maybe
+ = Functor 
+        maybe_fmap
+ where 
+        maybe_fmap : [a b: Data]. (a -> b) -> Maybe a -> Maybe b
+        maybe_fmap f xx 
+         = case xx of
+               Nothing -> Nothing
+               Just x  -> Just (f x)
+
+
+-- Applicative ----------------------------------------------------------------
+applicative_maybe
+ = Applicative 
+        functor_maybe 
+        maybe_pure
+        maybe_ap
+ where
+        maybe_pure : [a: Data]. a -> Maybe a
+        maybe_pure x
+         = Just x
+
+        maybe_ap   : [a b: Data]. Maybe (a -> b) -> Maybe a -> Maybe b
+        maybe_ap mf ma
+         | Just xf      <- mf
+         , Just xa      <- ma
+         = Just (xf xa)
+
+         | otherwise
+         = Nothing
+
+
+-- Monad ----------------------------------------------------------------------
+monad_maybe
+ = Monad
+        applicative_maybe
+        maybe_return
+        maybe_bind
+ where  
+        maybe_return : [a: Data]. a -> Maybe a
+        maybe_return x
+         = Just x
+
+        maybe_bind   : [a b: Data]. Maybe a -> (a -> Maybe b) -> Maybe b
+        maybe_bind ma f         
+         = case ma of
+                Nothing -> Nothing
+                Just xa -> f xa
+
+
+-- Predicates -----------------------------------------------------------------
 -- | Check if the given value is a `Nothing`.
-isNothing (m: Maybe a): Bool#
+isNothing (m: Maybe a): Bool
  = case m of
         Nothing -> True
         Just x  -> False
 
 
 -- | Check if the given value is a `Just`.
-isJust (m: Maybe a): Bool#
+isJust (m: Maybe a): Bool
  = case m of
         Nothing -> False
         Just x  -> True
 
 
+-- Destructors ----------------------------------------------------------------
 -- | Take the value from a `Just`, or return a default value.
 fromMaybe (def: a) (m: Maybe a): a
  = case m of
@@ -36,3 +93,4 @@
  = case m of
         Nothing -> def
         Just x  -> f x
+
diff --git a/tetra/base/Data/Numeric/Bool.ds b/tetra/base/Data/Numeric/Bool.ds
--- a/tetra/base/Data/Numeric/Bool.ds
+++ b/tetra/base/Data/Numeric/Bool.ds
@@ -1,23 +1,24 @@
 
 module Data.Numeric.Bool
-export  { not; and; or }
+export { not; and; or; }
 where
 
+type Bool = Bool#
 
 -- | Boolean NOT.
-not (x: Bool#): Bool#
+not (x: Bool): Bool
  = if x then False  
         else True
 
 
 -- | Boolean AND.
-and (x y: Bool#): Bool#
+and (x y: Bool): Bool
  = if x then y 
         else False
 
 
 -- | Boolean OR.
-or (x y: Bool#): Bool#
+or (x y: Bool): Bool
  = if x then True 
         else y
 
diff --git a/tetra/base/Data/Numeric/Nat.ds b/tetra/base/Data/Numeric/Nat.ds
--- a/tetra/base/Data/Numeric/Nat.ds
+++ b/tetra/base/Data/Numeric/Nat.ds
@@ -1,12 +1,18 @@
 
 module Data.Numeric.Nat
-export  { add; sub;  mul; div; rem
-        ; eq;  neq; lt;   le;  gt;  ge
-        ; shl; shr; band; bor; bxor
-        ; divMod }
+export  
+{       add; sub;  mul; div; rem;
+        eq;  neq; lt;   le;  gt;  ge;
+        shl; shr; band; bor; bxor;
+        divMod;
+        ord_nat;
+}
 import Data.Tuple
+import Class.Ord
 where
 
+type Nat = Nat#
+
 -------------------------------------------------------------------------------
 -- Names used by the Source Tetra desugarer to implement infix operators.
 add x y         = add# [Nat#] x y
@@ -37,7 +43,16 @@
 bxor x y        = bxor# [Nat#] x y 
 
 
-divMod (n m: Nat#): Tup2 Nat# Nat#
+divMod (n m: Nat): Tup2 Nat Nat
  = T2 (div n m) (rem n m)
 
+
+-------------------------------------------------------------------------------
+-- Type class instances.
+nat_compare n1 n2
+ | n1 > n2      = GT
+ | n1 < n2      = LT
+ | otherwise    = EQ
+
+ord_nat         = Ord nat_compare
 
diff --git a/tetra/base/Data/Numeric/Word.ds b/tetra/base/Data/Numeric/Word.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Data/Numeric/Word.ds
@@ -0,0 +1,9 @@
+
+module Data.Numeric.Word
+where
+
+type Word8      = Word8#
+type Word16     = Word16#
+type Word32     = Word32#
+type Word64     = Word64#
+
diff --git a/tetra/base/Data/Stream.ds b/tetra/base/Data/Stream.ds
--- a/tetra/base/Data/Stream.ds
+++ b/tetra/base/Data/Stream.ds
@@ -1,10 +1,13 @@
 
 module Data.Stream
-export  { streamOfList; listOfStream
-        ; sgenerate; senumFrom; srepeat; scons
-        ; smap; smapacc
-        ; sfold; sany
-        ; stake; stakeWhile; sfilter }
+export  
+{       streamOfList; listOfStream;
+        sgenerate; senumFrom; srepeat; scons;
+        smap; smapacc;
+        sfold; sany;
+        stake; stakeWhile; 
+        sfilter;
+}
 import Data.Numeric.Nat
 import Data.List
 import Data.Maybe
@@ -15,6 +18,7 @@
 where
 
 
+-------------------------------------------------------------------------------
 -- | Unbounded streams, 
 --   wraps a function that produces elements on demand.
 data Stream (s a: Data) where
@@ -26,31 +30,30 @@
         Done    : Step s a
 
 
--- Conversions ------------------------------------------------------------------------------------
+-- Conversions ----------------------------------------------------------------
 -- | Convert a list to a stream.
 streamOfList (xx: List a): Stream (List a) a
- = let  step (s1: List a)
+ = MkStream step xx
+ where  
+        step (s1: List a)
          = case s1 of
                 Nil       -> Done
                 Cons x xs -> Yield x xs
-   in   MkStream step xx
 
 
 -- | Convert a stream to a list.
-listOfStream  (ss: Stream s a): List a
- = case ss of
-        MkStream f s0
-         -> case f s0 of
-                Yield x s1      -> Cons x (listOfStream (MkStream f s1))
-                Skip  s1        -> listOfStream (MkStream f s1)
-                Done            -> Nil
+listOfStream (ss: Stream s a): List a
+ | MkStream f s0 <- ss
+ = case f s0 of
+        Yield x s1      -> Cons x (listOfStream (MkStream f s1))
+        Skip  s1        -> listOfStream (MkStream f s1)
+        Done            -> Nil
 
 
 -- | Load the given number of elements from a stream and write them
 --   into a freshly allocated array.
 arrayOfStream 
-        [r1: Region] 
-        (n: Nat#)        -- ^ Length of result array.
+        (n: Nat)         -- ^ Length of result array.
         (d: a)           -- ^ Default element value.
         (ss: Stream s a) -- ^ Stream to evaluate.
         : S (Alloc r1) (Array r1 a)
@@ -68,94 +71,101 @@
 
 -- | Unstream all available elements into the given array.
 unstreamToArray
-        [r: Region] 
-        (ss: Stream s a) (arr: Array r a) (ix: Nat#)
+        (ss: Stream s a) (arr: Array r a) (ix: Nat)
         : S (Write r) Unit
- = case ss of
-        MkStream f s0
-         -> case f s0 of
+ | MkStream f s0  <- ss
+ = go s0 0
+ where  
+        go (s: s) (ix: Nat): S (Write r) Unit
+         = case f s of
                 Yield x s1
                  -> do  writeArray arr ix x
-                        unstreamToArray (MkStream f s1) arr (ix + 1)
+                        go s1 (ix + 1)
 
                 Skip s1
-                 ->     unstreamToArray (MkStream f s1)  arr ix
+                 ->     go s1 ix 
 
                 Done
                  ->     ()
 
 
--- Constructors -----------------------------------------------------------------------------------
+-- Constructors ---------------------------------------------------------------
 -- | Generate a stream, given a starting value and a stepper function.
 sgenerate (x: s) (step: s -> Tup2 s a): Stream s a
- = let  step' sA
+ = MkStream step' x
+ where  
+        step' sA
          = case step sA of
                 T2 s' x -> Yield x s'
-   in   MkStream step' x
 
-senumFrom (x: Nat#): Stream Nat# Nat#
- = sgenerate x (λs: Nat#. T2 (s + 1) s)
+senumFrom (x: Nat): Stream Nat Nat
+ = sgenerate x (λ(s: Nat) -> T2 (s + 1) s)
 
 
 -- | Create a stream that returns copies of the same value.
 srepeat (x: a): Stream a a
- = sgenerate x (λs: a. T2 s s)
+ = sgenerate x (λ(s: a) -> T2 s s)
 
 
 -- | Cons an element to the front of a stream.
-scons (x: a) (ss: Stream s a): Stream (Tup2 s Bool#) a
- = case ss of
-        MkStream stepA sA0
-         -> let stepA2 q
-                 = case q of
-                        T2 sA1 b
-                         -> case b of
-                                True    -> Yield x (T2 sA1 False)
-                                False   -> case stepA sA1 of
-                                                Yield y sA2 -> Yield y (T2 sA2 False)
-                                                Skip  sA2   -> Skip    (T2 sA2 False)
-                                                Done        -> Done
-            in  MkStream stepA2 (T2 sA0 True)
+scons   (x: a) (ss: Stream s a)
+        : Stream (Tup2 s Bool) a
+ | MkStream stepA  sA0 <- ss
+ = MkStream stepA2 (T2 sA0 True)
+ where  
+        stepA2 (T2 sA1 True)
+         = Yield x (T2 sA1 False)
 
+        stepA2 (T2 sA1 False)
+         = case stepA sA1 of
+                Yield y sA2 -> Yield y (T2 sA2 False)
+                Skip  sA2   -> Skip    (T2 sA2 False)
+                Done        -> Done
 
--- Maps -------------------------------------------------------------------------------------------
+
+-- Maps -----------------------------------------------------------------------
 -- | Apply a function to every element of a stream.
-smap (f: a -> b) (ss: Stream s a): Stream s b
- = case ss of  
-        MkStream stepA sA0
-         -> let stepB q 
-                 = case stepA q of
-                        Yield x sA1     -> Yield (f x) sA1
-                        Skip sA2        -> Skip sA2
-                        Done            -> Done
-            in  MkStream stepB sA0
+smap    (f: a -> b) 
+        (ss: Stream s a)
+        : Stream s b
+ | MkStream stepA sA0 <- ss
+ = MkStream stepB sA0
+ where
+        stepB q 
+         = case stepA q of
+                Yield x sA1     -> Yield (f x) sA1
+                Skip sA2        -> Skip sA2
+                Done            -> Done
 
 
--- Scans ------------------------------------------------------------------------------------------
+-- Scans ----------------------------------------------------------------------
 -- | Like `smap`, but keep a running accumulator as we walk along the stream.
-smapacc (f: a -> b -> Tup2 a c) (z: a) 
-        (ss: Stream s b): Stream (Tup2 s a) c
- = case ss of
-        MkStream fB sB0
-         -> let stepC q
-                 = case q of
-                        T2 sB1 xA1
-                         -> case fB sB1 of
-                                Yield xB1 sB2 
-                                 -> case f xA1 xB1 of
-                                        T2 xA2 xC2
-                                         -> Yield xC2 (T2 sB2 xA2)
-                                Skip sB2 -> Skip      (T2 sB2 xA1)
-                                Done     -> Done
-            in  MkStream stepC (T2 sB0 z)
+smapacc :  [a b c s: Data]
+        .  (a -> b -> Tup2 a c)
+        -> a
+        -> Stream s b
+        -> Stream (Tup2 s a) c
 
+smapacc f z (MkStream fB sB0)
+ = MkStream stepC (T2 sB0 z)
+ where
+        stepC (T2 sB1 xA1)
+         = case fB sB1 of
+                Yield xB1 sB2 
+                 -> case f xA1 xB1 of
+                        T2 xA2 xC2
+                         -> Yield xC2 (T2 sB2 xA2)
+                Skip sB2 -> Skip      (T2 sB2 xA1)
+                Done     -> Done
 
--- Folds ------------------------------------------------------------------------------------------
+
+-- Folds ----------------------------------------------------------------------
 -- | Fold all the elements from a stream.
-sfold    (f: a -> b -> a) (acc: a) (ss: Stream s b): a
- = case ss of
-        MkStream step s0 
-         -> sconsume f acc step s0
+sfold   (f: a -> b -> a) 
+        (acc: a) 
+        ((MkStream step s0): Stream s b)
+        : a
+ = sconsume f acc step s0
 
 
 sconsume (f:    a -> b -> a)   (acc:   a) 
@@ -168,54 +178,57 @@
 
 -- | Check if any of the elements of this stream are true,
 --   demanding only the prefix of non-true elements from the stream.
-sany [s: Data] (ss: Stream s Bool#): Bool#
+sany [s: Data] (ss: Stream s Bool): Bool
  = sfold or False $ stakeWhile id ss
 
 
--- Projections ------------------------------------------------------------------------------------
+-- Projections ----------------------------------------------------------------
 -- | Take the given number of elements from a stream.
-stake (n: Nat#) (ss: Stream s a): Stream (Tup2 s Nat#) a
- = case ss of
-        MkStream fA sA0
-         -> let stepB q
-                 = case q of
-                        T2 sA ix 
-                         | ix >= n   -> Done
-                         | otherwise 
-                         -> case fA sA of
-                                Yield x sA2 -> Yield x (T2 sA2 (ix + 1))
-                                Skip sA3    -> Skip  (T2 sA3 ix)
-                                Done        -> Done
-            in   MkStream stepB (T2 sA0 0)
+stake   (n: Nat)
+        ((MkStream fA sA0): Stream s a)
+        : Stream (Tup2 s Nat) a
 
+ = MkStream stepB (T2 sA0 0)
+ where  
+        stepB (T2 sA ix)
+         | ix >= n   = Done
+         | otherwise 
+         = case fA sA of
+                Yield x sA2 -> Yield x (T2 sA2 (ix + 1))
+                Skip sA3    -> Skip  (T2 sA3 ix)
+                Done        -> Done
 
--- | Take elements from a strem while they match the given predicate.
-stakeWhile (p: a -> Bool#) (ss: Stream s a): Stream s a
- = case ss of
-        MkStream stepA sA0
-         -> let stepB q
-                 = case stepA q of
-                        Yield x sA1     
-                         | p x          -> Yield x sA1
-                         | otherwise    -> Done [s] [a]
 
-                        Skip sA1        -> Skip    sA1
-                        Done            -> Done
+-- | Take elements from a stream while they match the given predicate.
+stakeWhile 
+        (p: a -> Bool) 
+        ((MkStream stepA sA0): Stream s a)
+        : Stream s a
 
-            in  MkStream stepB sA0
+ = MkStream stepB sA0
+ where  
+        stepB (q: s)
+         = case stepA q of
+                Yield x sA1     
+                 | p x          -> Yield x sA1
+                 | otherwise    -> Done
 
+                Skip sA1        -> Skip    sA1
+                Done            -> Done
 
+
 -- | Take elements from a stream that match the given predicate.
-sfilter (p: a -> Bool#) (ss: Stream s a): Stream s a
- = case ss of
-        MkStream stepA sA0
-         -> let stepB q
-                 = case stepA q of
-                        Yield x sA1     
-                         | p x          -> Yield x sA1
-                         | otherwise    -> Skip    sA1
+sfilter (p: a -> Bool)
+        ((MkStream stepA sA0): Stream s a)
+        : Stream s a
+ = MkStream stepB sA0
+ where
+        stepB (q: s)
+         = case stepA q of
+                Yield x sA1     
+                 | p x          -> Yield x sA1
+                 | otherwise    -> Skip sA1
 
-                        Skip sA1        -> Skip    sA1
-                        Done            -> Done
+                Skip sA1        -> Skip sA1
+                Done            -> Done 
 
-            in  MkStream stepB sA0
diff --git a/tetra/base/Data/Text.ds b/tetra/base/Data/Text.ds
--- a/tetra/base/Data/Text.ds
+++ b/tetra/base/Data/Text.ds
@@ -1,308 +1,6 @@
 
 module Data.Text 
-export  
-{       -- * Construction
-        textLit; textOfVector; vectorOfText;
-        paste; pastes;
-
-        -- * Projections
-        sizeOfText;
-
-        -- * Conversions
-        copyTextToVector;
-        copyTextLitToVector;
-        copyTextVecToVector;
-
-        -- * Operators
-        textOfWord8;
-
-        -- * Showing
-        showBool;
-        showNat; showBinaryNat; showDecimalNat; showHexNat; showBaseNat;
-        digitBinary; digitDecimal; digitHex;
-}
-import Data.Numeric.Nat
-import Data.Numeric.Bool
-import Data.Function
-import Data.List
-
-
--- | The TextLit type is define in the runtime system and contains
---   a pointer to the literal utf-8 text data in static memory.
-import foreign boxed type
-        TextLit         : Data
-
-
--- | Runtime functions for dealing with unboxed text literals.
-import foreign c value
-
-        -- | Box a text literal.
-        makeTextLit     : TextLit# -> TextLit
-
-        -- | Get the size of a boxed text literal.
-        sizeOfTextLit   : TextLit  -> Nat#
-
-        -- | Get a single byte from a boxed text literal.
-        indexTextLit    : TextLit  -> Nat# -> Word8#
-
-
--- | Top level region containing text vectors.
-import foreign abstract type
-        RegionText      : Region
-
-
--- | Capabilities to allocate and read top-level text vectors.
-import foreign abstract capability
-        capTopTextAlloc : Alloc RegionText
-        capTopTextRead  : Read  RegionText
-
-where
-
-
--------------------------------------------------------------------------------
--- Names used by the Source Tetra desugarer to implement string literals.
-textLit (x : TextLit#) : Text
- = TextLit (makeTextLit x)
-
-paste  (x y : Text) : Text
- = TextApp x y
-
-pastes (x y : Text) : Text
- = x % " " % y
-
-
--------------------------------------------------------------------------------
-data Text where
-        TextLit : TextLit                   -> Text
-        TextVec : Vector# RegionText Word8# -> Text
-        TextApp : Text -> Text              -> Text
-
-
--- Construction ---------------------------------------------------------------
--- | O(1). Wrap a vector of utf8 data into a text object.
-textOfVector (vec: Vector# RegionText Word8#): Text
- = TextVec vec
-
-
--- | Copy a Text object into a flat vector of utf-8 bytes.
-vectorOfText [r1: Region] (tt: Text)
-        : S (Alloc r1) (Vector# r1 Word8#)
- = extend r1 using r2 with { Alloc r2; Write r2 } in
-   do   
-        -- Allocate a vector to hold all the data, 
-        -- including an extra null terminator byte.
-        vec     = vectorAlloc# [r2] [Word8#] (add (sizeOfText tt) 1)
-
-        -- Copy the text data into the vector.
-        iEnd    = copyTextToVector tt vec 0
-
-        -- Write the null terminator.
-        vectorWrite# vec iEnd 0w8
-
-        vec
-
-
--- | Wrap a single 8-bit character into a text object.
---
-textOfWord8 (w8: Word8#): Text
- = TextVec
-  (extend RegionText using r1 with { Alloc r1; Write r1 } in
-   do   -- Allocate the vector to hold the data,
-        -- including an extra null terminator byte.
-        vec     = vectorAlloc# [r1] [Word8#] 2
-
-        -- Write the character.
-        vectorWrite# vec 0 w8
-
-        -- Write the null terminator.
-        vectorWrite# vec 1 0w8
-
-        vec)
-
-
--- Projections ----------------------------------------------------------------
--- | Get the size of the utf8 data in a Text object, in bytes.
---
---   * This is NOT the same as the length of the text string in characters,
---     as single characters can be encoded using multiple bytes.
---
-sizeOfText (tt: Text): Nat#
- = case tt of
-        TextLit lit
-         -> sizeOfTextLit lit
-
-        -- The size of a text vector is the vector size minus
-        -- the null terminator byte.
-        TextVec vec     
-         -> vectorLength# vec - 1
-
-        TextApp t1 t2
-         -> sizeOfText t1 + sizeOfText t2
-
-
--- Conversions ----------------------------------------------------------------
--- | Copy a text literal to a mutable vector of utf-8 bytes.
-copyTextToVector 
-        [r: Region] (tt: Text) (vec: Vector# r Word8#) (i0: Nat#)
-        : S (Write r) Nat#
- = case tt of
-        TextLit lit
-         -> copyTextLitToVector lit  vec i0 0 (sizeOfTextLit lit)
-
-        TextVec vec2
-         -> copyTextVecToVector vec2 vec i0 0 (vectorLength# vec2)
-
-        TextApp t1 t2
-         -> do  i1 = copyTextToVector t1 vec i0
-                i2 = copyTextToVector t2 vec i1
-                i2
-
-
--- | Copy a text literal to a mutable vector of utf-8 bytes.
-copyTextLitToVector 
-        [r: Region] (tt: TextLit) (vec: Vector# r Word8#) 
-        (iDst iSrc nSrc: Nat#)
-        : S (Write r) Nat#
- = case iSrc >= nSrc of
-        True  -> iDst
-        False 
-         -> do  vectorWrite# vec iDst (indexTextLit tt iSrc)
-
-                copyTextLitToVector 
-                        tt vec (iDst + 1) (iSrc + 1) nSrc
-
-
--- | Copy a text source vector to a mutable destination of utf-8 bytes.
-copyTextVecToVector 
-        [r1 r2: Region] 
-        (vecSrc: Vector# r1 Word8#) (vecDst: Vector# r2 Word8#)
-        (iDst iSrc nSrc: Nat#)
-        : S (Read r1 + Write r2) Nat#
- = case iSrc >= nSrc of
-        True    -> iDst
-
-        False   -> do
-                vectorWrite# vecDst iDst (vectorRead# vecSrc iSrc)
-
-                copyTextVecToVector 
-                        vecSrc vecDst (iDst + 1) (iSrc + 1) nSrc
-
-
--- Operators ------------------------------------------------------------------
--- | If this text is not already in flat form then flatten it.
---
---   This allocates a new contiguous vector for the text object and
---   allows the program to release space for intermediate append nodes.
---
-flattenText (tt: Text): Text
- = case tt of
-        -- Single text literals are already flat.
-        TextLit lit     -> tt
-
-        -- Single text vectors are already flat.
-        TextVec vec     -> tt
-
-        -- Text has an outer append-node, 
-        -- so flatten the whole thing.
-        TextApp _ _     -> textOfVector (run vectorOfText [RegionText] tt)
-
-
--- Showing --------------------------------------------------------------------
--- | Convert a Bool to a String.
-showBool (x : Bool#) : Text
- = if x then "True" 
-        else "False"
-
-
--- | Show a natural number.
-showNat (x: Nat#): Text
- = showBaseNat 10 digitDecimal 0 "X" x
-
-
--------------------------------------------------------------------------------
--- | Show a natural number, in binary.
-showBinaryNat (x: Nat#): Text
- = showBaseNat 2 digitBinary 0 "X" x
-
-digitBinary (n: Nat#): Text
- = case n of
-        0       -> "0"
-        1       -> "1"
-        _       -> "X"
-
-
--- | Show a natural number in decimal.
-showDecimalNat (x: Nat#): Text
- = showBaseNat 10 digitDecimal 0 "X" x
-
-digitDecimal (n: Nat#): Text
- = case n of
-        0       -> "0"
-        1       -> "1"
-        2       -> "2"
-        3       -> "3"
-        4       -> "4"
-        5       -> "5"
-        6       -> "6"
-        7       -> "7"
-        8       -> "8"
-        9       -> "9"
-        _       -> "X"
-
-
--- | Show a natural number in hex.
-showHexNat (x: Nat#): Text
- = showBaseNat    16 digitHex 0 "X" x
-
-digitHex (n: Nat#): Text
- = case n of
-        0       -> "0"
-        1       -> "1"
-        2       -> "2"
-        3       -> "3"
-        4       -> "4"
-        5       -> "5"
-        6       -> "6"
-        7       -> "7"
-        8       -> "8"
-        9       -> "9"
-        10      -> "a"
-        11      -> "b"
-        12      -> "c"
-        13      -> "d"
-        14      -> "e"
-        15      -> "f"
-        _       -> "X"
-
-
--------------------------------------------------------------------------------
--- | Show a natural number using an arbitrary base encoding.
-showBaseNat 
-        (base:  Nat#)           -- ^ Base of encoding.
-        (digit: Nat# -> Text)   -- ^ Show a digit in this base.
-        (width: Nat#)           -- ^ Width of output, or 0 to not pad.
-        (pad:   Text)           -- ^ Character to pad output with.
-        (x:     Nat#)           -- ^ Number to print.
-        : Text
-
- = do   s       = showBaseNat' base digit width pad True x
-        if x < 0 
-         then "-" % s 
-         else s
-
-showBaseNat' base digit width pad first x
- | and (x == 0) first
- = showBaseNat' base digit (width - 1) pad False x
- % "0"
-
- | and (x == 0) (width > 0)
- = showBaseNat' base digit (width - 1) pad False x
- % pad
-
- | x == 0
- = ""
-
- | otherwise
- = showBaseNat' base digit (width - 1) pad False (div x base) 
- % digit (rem x base) 
-
+import Data.Text.Base
+import Data.Text.List
+import Data.Text.Operator
+import Data.Text.Show
diff --git a/tetra/base/Data/Text/Base.ds b/tetra/base/Data/Text/Base.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Data/Text/Base.ds
@@ -0,0 +1,244 @@
+
+-- | Basic types and operators on Text objects.
+module Data.Text.Base
+export
+{       -- Runtime operators.
+        makeTextLit;
+        sizeOfTextLit;
+        indexTextLit;
+
+        -- Construction.
+        textOfChar;
+        textOfWord8;
+        textOfVector;
+
+        -- Conversion.
+        vectorOfText;
+
+        -- Projections.
+        sizeOfText;
+        indexText;
+
+        -- Operators.
+        eqText;
+}
+import Data.Text.Char
+import Data.Numeric.Nat
+import Data.Numeric.Word
+import Data.Maybe
+
+
+-------------------------------------------------------------------------------
+-- Foreign imports.
+
+-- | A TextLit is a boxed object that contains a pointer to literal
+--   UTF-8 data in static memory.  
+import foreign boxed type
+        TextLit         : Data
+
+
+-- | Runtime operators for working with unboxed text literals.
+import foreign c value
+
+        -- | Make a text literal.
+        --   The TextLit# type is a pointer to literal UTF-8 data in 
+        --   static memory, which we pack into a boxed object.
+        makeTextLit     : TextLit# -> TextLit
+
+        -- | Get the size of a boxed text literal.
+        sizeOfTextLit   : TextLit  -> Nat#
+
+        -- | Get a single byte from a boxed text literal.
+        --   This is a byte rather than a character,
+        --   as UTF-8 encoded characters can consist of multiple bytes.
+        indexTextLit    : TextLit  -> Nat# -> Word8#
+
+
+-- | Top level region containing text vectors.
+--   All our dynamic character data is in this region.
+import foreign abstract type
+        RegionText      : Region
+
+
+-- | Capabilities to allocate and read top-level text vectors.
+import foreign abstract capability
+        capTopTextAlloc : Alloc RegionText
+        capTopTextRead  : Read  RegionText
+
+where
+
+
+-- Text -----------------------------------------------------------------------
+data Text where
+        -- | Wrap a text literal into a text object.
+        --   The characterdata is stored in static memory.
+        TextLit : TextLit                   -> Text
+
+        -- | Wrap some character data into a text object.
+        --   The character data is stored on the heap.
+        TextVec : Vector# RegionText Word8# -> Text
+
+        -- | Append two text objects.
+        TextApp : Text -> Text              -> Text
+
+
+-- Construction ---------------------------------------------------------------
+-- | O(1). Wrap a single character into a text object.
+--   We're only taking the lowest 8 bit bytes,
+--   rather than doing proper UTF-8 encoding.
+textOfChar (c: Word32): Text
+ = textOfWord8 (truncate# c)
+
+
+-- | O(1). Wrap a single byte into a text object.
+textOfWord8 (w8: Word8): Text
+ = TextVec
+ $ extend RegionText using r1 with { Alloc r1; Write r1 } in
+   do   -- Allocate the vector to hold the data,
+        -- including an extra null terminator byte.
+        vec     = vectorAlloc# [r1] 2
+
+        -- Write the character.
+        vectorWrite# vec 0 w8
+
+        -- Write the null terminator.
+        vectorWrite# vec 1 0w8
+
+        vec
+
+
+-- | O(1). Wrap a vector of UTF-8 data into a text object.
+textOfVector (vec: Vector# RegionText Word8): Text
+ = TextVec vec
+
+
+-- Conversion -----------------------------------------------------------------
+-- | Copy a Text object into a flat vector of UTF-8 data.
+vectorOfText
+        [r1: Region] (tt: Text)
+        : S (Alloc r1) (Vector# r1 Word8)
+ = extend r1 using r2 with { Alloc r2; Write r2 } in
+   do   
+        -- Allocate a vector to hold all the data, 
+        -- including an extra null terminator byte.
+        vec     = vectorAlloc# [r2] (add (sizeOfText tt) 1)
+
+        -- Copy the text data into the vector.
+        iEnd    = copyTextToVector tt vec 0
+
+        -- Write the null terminator.
+        vectorWrite# vec iEnd 0w8
+
+        vec
+
+
+-- | Copy a text object to a mutable vector of UTF-8 data.
+copyTextToVector 
+        [r: Region] (tt: Text) (vec: Vector# r Word8) (i0: Nat)
+        : S (Write r) Nat
+ = case tt of
+        TextLit lit
+         -> copyTextLitToVector lit  vec i0 0 (sizeOfTextLit lit)
+
+        TextVec vec2
+         -> copyTextVecToVector vec2 vec i0 0 (vectorLength# vec2 - 1)
+
+        TextApp t1 t2
+         -> do  i1 = copyTextToVector t1 vec i0
+                i2 = copyTextToVector t2 vec i1
+                i2
+
+
+-- | Copy a text literal to a mutable vector of UTF-8 data.
+copyTextLitToVector 
+        [r: Region] (tt: TextLit) (vec: Vector# r Word8) 
+        (iDst iSrc nSrc: Nat)
+        : S (Write r) Nat
+ | iSrc >= nSrc = iDst
+ | otherwise
+ = do   vectorWrite# vec iDst (indexTextLit tt iSrc)
+        copyTextLitToVector 
+                tt vec (iDst + 1) (iSrc + 1) nSrc
+
+
+-- | Copy a text source vector to a mutable vector of UTF-8 data.
+copyTextVecToVector 
+        [r1 r2: Region] 
+        (vecSrc: Vector# r1 Word8) (vecDst: Vector# r2 Word8)
+        (iDst iSrc nSrc: Nat)
+        : S (Read r1 + Write r2) Nat
+ | iSrc >= nSrc = iDst
+ | otherwise
+ = do   vectorWrite# vecDst iDst (vectorRead# vecSrc iSrc)
+        copyTextVecToVector 
+                vecSrc vecDst (iDst + 1) (iSrc + 1) nSrc
+
+
+-- Projections ----------------------------------------------------------------
+-- | Get the size of the utf8 data in a Text object, in bytes.
+--
+--   * This is NOT the same as the length of the text string in characters,
+--     as single characters can be encoded using multiple bytes.
+--
+sizeOfText (tt: Text): Nat
+ = case tt of
+        TextLit lit
+         -> sizeOfTextLit lit
+
+        -- The size of a text vector is the vector size minus
+        -- the null terminator byte.
+        TextVec vec     
+         -> vectorLength# vec - 1
+
+        TextApp t1 t2
+         -> sizeOfText t1 + sizeOfText t2
+
+
+-- | Get a single word8 character from a Text object.
+indexText (tt: Text) (ix: Nat): Maybe Word8
+ = case tt of
+        TextLit lit
+         | ix >= sizeOfTextLit lit      -> Nothing
+         | otherwise                    -> Just (indexTextLit lit ix)
+
+        TextVec vec
+         | ix >= vectorLength# vec - 1  -> Nothing
+         | otherwise                    -> Just (vectorRead# vec ix)
+
+        TextApp t1 t2
+         -> case indexText t1 ix of
+                Just x                  -> Just x
+                Nothing                 -> indexText t2 (ix - sizeOfText t1)
+
+
+-- Comparison -----------------------------------------------------------------
+-- | O(max len1 len2).
+--   Check if two text objects represent the same characters.
+eqText (tx1 tx2: Text): Bool
+ = private r with {Read r; Alloc r} in
+   do   
+        -- We copy both strings into new vectors before doing the comparison.
+        -- It would be better to do it in-place.
+        vec1    = vectorOfText  [r] tx1 
+        len1    = vectorLength# vec1
+
+        vec2    = vectorOfText  [r] tx2
+        len2    = vectorLength# vec2
+
+        match
+         | len1 /= len2 = False
+         | len1 == 0    = True
+         | otherwise    = go vec1 vec2 len1 0
+
+ where
+        go (vec1 vec2: Vector# r Word8)
+           (len: Nat) (ix: Nat): S (Read r) Bool
+         | ix >= (len - 1)
+         = True
+
+         | not (eq# (vectorRead# vec1 ix) (vectorRead# vec2 ix))
+         = False
+
+         | otherwise
+         = go vec1 vec2 len (ix + 1)
+
diff --git a/tetra/base/Data/Text/Char.ds b/tetra/base/Data/Text/Char.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Data/Text/Char.ds
@@ -0,0 +1,28 @@
+
+module Data.Text.Char
+export
+{       isDigit;
+        isUpper;
+        isLower;
+}
+import Data.Numeric.Bool
+where
+
+-- Character literals are special syntax for a unicode codepoint
+-- represented as a 32-bit word.
+type Char = Word32#
+
+
+-- | Check if a character is a digit.
+isDigit (c: Char): Bool
+ = ge# c 0x030w32 ∧ le# c 0x039w32
+
+
+-- | Check if a character is an upper-case letter.
+isUpper (c: Char): Bool
+ = ge# c 65w32    ∧ le# c 90w32
+
+
+-- | Check if a character is a lower-case letter.
+isLower (c: Char): Bool
+ = ge# c 97w32    ∧ le# c 122w32
diff --git a/tetra/base/Data/Text/List.ds b/tetra/base/Data/Text/List.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Data/Text/List.ds
@@ -0,0 +1,66 @@
+
+-- | Conversions between Text and Lists.
+module Data.Text.List
+export 
+{       textOfCharList;
+        charListOfText;
+}
+import Data.Numeric.Word
+import Data.Text.Base
+import Data.Text.Char
+import Data.List
+where
+
+
+-- | Convert a list of characters to a Text object.
+textOfCharList (xx: List Char): Text
+ = TextVec
+ $ extend RegionText using r with { Alloc r; Read r; Write r }
+   in  vectorOfCharList [r] xx
+
+
+-- | O(n). Convert a text object to a list of characters.
+charListOfText (tx: Text): List Char
+ = case tx of
+        TextVec vec -> charListOfTextVec vec
+        _           -> charListOfTextVec (vectorOfText [RegionText] tx)
+
+
+-- | Unpack a list of characters from a vector.
+charListOfTextVec
+        (vec: Vector# r Word8)
+        : S (Read r) (List Char)
+ = go 0
+ where  
+        go (ix: Nat): S (Read r) (List Char)
+         | ix >= (vectorLength# vec - 1)
+         = Nil
+
+         | otherwise               
+         = do   txChar = promote# (vectorRead# vec ix)
+                Cons txChar (go (ix + 1))
+
+
+-- | Pack a list of characters into a mutable vector.
+vectorOfCharList
+        [r: Region]
+        (xx: List Char)
+        : S (Alloc r + Write r) (Vector# r Word8)
+ = do
+        len     = length xx
+        vec     = vectorAlloc# [r] (len + 1)
+
+        fill (ix: Nat) (xx: List Char): S (Write r) Unit
+         = case xx of
+                Nil     -> ()
+                Cons x xs
+                 -> do  vectorWrite# vec ix (truncate# x)
+                        fill (ix + 1) xs
+
+                 | otherwise
+                 -> do  fill (ix + 1) xs
+        fill 0 xx
+
+        vectorWrite# vec len 0w8
+        vec
+
diff --git a/tetra/base/Data/Text/Operator.ds b/tetra/base/Data/Text/Operator.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Data/Text/Operator.ds
@@ -0,0 +1,54 @@
+
+-- | Useful operators on text objects.
+module Data.Text.Operator
+export
+{       -- * Desugaring
+        textLit; paste; pastes;
+
+        -- * Optimizations
+        flattenText;
+
+        -- * Pretty Printing
+        parens;
+}
+import Data.Text.Base
+where
+
+
+-- Desuguaring -----------------------------------------------------------------
+-- Names used by the Source Tetra desugarer to implement string literals.
+textLit (x : TextLit#) : Text
+ = TextLit (makeTextLit x)
+
+paste  (x y : Text) : Text
+ = TextApp x y
+
+pastes (x y : Text) : Text
+ = x % " " % y
+
+
+-- Optimizations --------------------------------------------------------------
+-- | If this text is not already in flat form then flatten it.
+--
+--   This allocates a new contiguous vector for the text object and
+--   allows the program to release space for intermediate append nodes.
+--
+flattenText (tt: Text): Text
+ = case tt of
+        -- Single text literals are already flat.
+        TextLit lit     -> tt
+
+        -- Single text vectors are already flat.
+        TextVec vec     -> tt
+
+        -- Text has an outer append-node, 
+        -- so flatten the whole thing.
+        TextApp _ _     -> textOfVector (run vectorOfText [RegionText] tt)
+
+
+-- Pretty Printing ------------------------------------------------------------
+-- | Wrap a some text in parenthesis.
+parens (tx: Text): Text
+ = "(" % tx % ")"
+
+
diff --git a/tetra/base/Data/Text/Show.ds b/tetra/base/Data/Text/Show.ds
new file mode 100644
--- /dev/null
+++ b/tetra/base/Data/Text/Show.ds
@@ -0,0 +1,119 @@
+
+-- | Showing various data types as text.
+module Data.Text.Show
+export
+{       showBool;
+
+        showNat;
+        showBinaryNat;  digitBinary;
+        showDecimalNat; digitDecimal;
+        showHexNat;     digitHex;
+        showBaseNat;
+}
+import Data.Numeric.Word
+import Data.Text.Base
+import Data.Text.Char
+import Data.Text.Operator
+where
+
+
+-------------------------------------------------------------------------------
+-- | Convert a Bool to a String.
+showBool (x : Bool): Text
+ = if x then "True" 
+        else "False"
+
+
+-- | Show a natural number.
+showNat (x: Nat): Text
+ = showBaseNat 10 digitDecimal 0 'X' x
+
+
+-------------------------------------------------------------------------------
+-- | Show a natural number, in binary.
+showBinaryNat (x: Nat): Text
+ = showBaseNat 2 digitBinary 0 'X' x
+
+digitBinary (n: Nat): Char
+ = case n of
+        0       -> '0'
+        1       -> '1'
+        _       -> 'X'
+
+
+-------------------------------------------------------------------------------
+-- | Show a natural number in decimal.
+showDecimalNat (x: Nat): Text
+ = showBaseNat 10 digitDecimal 0 'X' x
+
+digitDecimal (n: Nat): Word32
+ = case n of
+        0       -> '0'
+        1       -> '1'
+        2       -> '2'
+        3       -> '3'
+        4       -> '4'
+        5       -> '5'
+        6       -> '6'
+        7       -> '7'
+        8       -> '8'
+        9       -> '9'
+        _       -> 'X'
+
+
+-------------------------------------------------------------------------------
+-- | Show a natural number in hex.
+showHexNat (x: Nat): Text
+ = showBaseNat 16 digitHex 0 'X' x
+
+digitHex (n: Nat): Char
+ = case n of
+        0       -> '0'
+        1       -> '1'
+        2       -> '2'
+        3       -> '3'
+        4       -> '4'
+        5       -> '5'
+        6       -> '6'
+        7       -> '7'
+        8       -> '8'
+        9       -> '9'
+        10      -> 'a'
+        11      -> 'b'
+        12      -> 'c'
+        13      -> 'd'
+        14      -> 'e'
+        15      -> 'f'
+        _       -> 'X'
+
+
+-------------------------------------------------------------------------------
+-- | Show a natural number using an arbitrary base encoding.
+showBaseNat 
+        (base:  Nat)            -- ^ Base of encoding.
+        (digit: Nat -> Char)    -- ^ Show a digit in this base.
+        (width: Nat)            -- ^ Width of output, or 0 to not pad.
+        (pad:   Char)           -- ^ Character to pad output with.
+        (x:     Nat)            -- ^ Number to print.
+        : Text
+ = do   s       = showBaseNat' base digit width pad True x
+        if x < 0 
+         then "-" % s 
+         else s
+
+showBaseNat' base digit width pad first x
+ | and (x == 0) first
+ = showBaseNat' base digit (width - 1) pad False x 
+        % "0"
+
+ | and (x == 0) (width > 0)
+ = showBaseNat' base digit (width - 1) pad False x
+        % textOfChar pad
+
+ | x == 0  
+ = ""
+
+ | otherwise
+ = showBaseNat' base digit (width - 1) pad False (div x base) 
+        % textOfChar (digit (rem x base))
+
diff --git a/tetra/base/Math/Combinations.ds b/tetra/base/Math/Combinations.ds
--- a/tetra/base/Math/Combinations.ds
+++ b/tetra/base/Math/Combinations.ds
@@ -6,37 +6,36 @@
 import Data.List
 where
 
+
 -- | Compute the factorial of a number.
 --
 --   factorial n is the number of possible permutations
 --   of a sequence of n things.
 --
-factorial (n: Nat#): Nat#
- = if n == 0
-        then 1
-        else n * factorial (n - 1)
+factorial (n: Nat): Nat
+ | n == 0       = 1
+ | otherwise    = n * factorial (n - 1)
 
 
--- | Compute the number of was of choosing r things from n things.
+-- | Compute the number of ways of choosing r things from n things.
 ---
 --   Note that the textbook definition of this is,
 --     div (factorial n) ( factorial (n - 1) * factorial r )
 --   but we factor out the (factorial (n - 1)) term beforehand to 
 --   make it easier to compute.
 --
-choose (n r: Nat#): Nat#
- = if r > n 
-        then 0
-        else div (prodRange n (n - (r - 1))) (factorial r)
+choose (n r: Nat): Nat
+ | r > n        = 0
+ | otherwise    = div (prodRange n (n - (r - 1))) (factorial r)
 
+
 -- | Compute the product of the range [n, n-1 .. m] inclusive.
-prodRange (n m: Nat#): Nat#
- = if n == m
-        then n
-        else n * prodRange (n - 1) m
+prodRange (n m: Nat): Nat
+ | n == m       = n
+ | otherwise    = n * prodRange (n - 1) m
 
 
 -- | Compute the number of ways of choosing collections of things
 --   of sizes rs from n things.
-chooseMany (n: Nat#) (rs: List Nat#): Nat#
+chooseMany (n: Nat) (rs: List Nat): Nat
  = div (factorial n) (prod (map factorial rs))