diff --git a/Frank.cabal b/Frank.cabal
--- a/Frank.cabal
+++ b/Frank.cabal
@@ -1,21 +1,22 @@
-name:		Frank
-version:	0.1
-synopsis:	An experimental programming language with typed algebraic effects
-description:	An experimental programming language with typed algebraic effects
-license:	PublicDomain
-author:		Conor McBride
-build-type:	Simple
-cabal-version:	>= 1.8
-homepage:	http://personal.cis.strath.ac.uk/~conor/pub/Frank/
-stability:	experimental
-category:	Languages
-license-file:	LICENCE
-maintainer:	conor@strictlypositive.org
+name:			Frank
+version:		0.2
+synopsis:		An experimental programming language with typed algebraic effects
+description:	   An experimental programming language with typed algebraic effects
+license:		PublicDomain
+author:			Conor McBride
+build-type:		Simple
+cabal-version:		>= 1.8
+homepage:		http://personal.cis.strath.ac.uk/~conor/pub/Frank/
+stability:		experimental
+category:		Languages
+license-file:		LICENCE
+maintainer:		conor@strictlypositive.org
+extra-source-files:	test.fk hello.fk keylog.fk
 
 executable frank
   main-is:		Main.lhs
   build-depends:	base < 5, void, newtype, mtl, she
-  extensions:		TypeOperators, KindSignatures, GADTs, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections, FunctionalDependencies, PatternGuards
+  extensions:		TypeOperators, KindSignatures, GADTs, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections, FunctionalDependencies, PatternGuards, MultiParamTypeClasses
   ghc-options:		-F -pgmF she
   other-modules:	Gubbins, Pa, Types, Template, Syntax, Check, ElabMonad, Unify, Elab, Run
 
diff --git a/Gubbins.lhs b/Gubbins.lhs
--- a/Gubbins.lhs
+++ b/Gubbins.lhs
@@ -1,6 +1,6 @@
 > {-# OPTIONS_GHC -F -pgmF she #-}
 > {-#  LANGUAGE TypeOperators, FlexibleInstances, FunctionalDependencies,
->      RankNTypes #-}
+>      RankNTypes, MultiParamTypeClasses #-}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/hello.fk b/hello.fk
new file mode 100644
--- /dev/null
+++ b/hello.fk
@@ -0,0 +1,8 @@
+data List X = nil | X :: (List X)
+
+map {X -> Y} (List X)   []   List Y
+map f nil        = nil
+map f (x :: xs)  = f x :: map f xs
+
+main [Console] List ()
+main = map ouch ('h' :: ('e' :: ('l' :: ('l' :: ('o' :: nil)))))
diff --git a/keylog.fk b/keylog.fk
new file mode 100644
--- /dev/null
+++ b/keylog.fk
@@ -0,0 +1,119 @@
+sig ReadLine
+  = peek [] Char
+  | nom
+
+sig Abort
+  = aborting [] {}
+
+abort [Abort] X
+abort = aborting ! {}
+
+default {[] X} [Abort ? X] [] X
+default d [x] = x
+default d [aborting ? k] = d!
+
+{[Abort] X} / {[] X} [] {[] X}
+e / d = {default d ? e!}
+
+if Bool then {[] X} else {[] X} [] X
+if tt then t else f = t!
+if ff then t else f = f!
+
+see Char [ReadLine, Abort] ()
+see c = if (peek! =Char= c) then {()} else {abort!}
+
+eat Char [ReadLine, Abort] ()
+eat c = see c >> nom!
+
+
+
+() >> Y [] Y
+_ >> y = y
+
+X << () [] X
+x << _ = x
+
+data List X
+  = nil
+  | X :: (List X)
+
+data SExp
+  = atom (List Char)
+  | SExp & SExp
+
+sexp [ReadLine, Abort] SExp
+sexp =
+  ({see '.' >> abort!} /
+   ({eat '(' >> open!} /
+    ({see ')' >> abort!} /
+     ({eat ' ' >> sexp!} /
+      {atom (name!)}
+  ))))!
+
+open [ReadLine, Abort] SExp
+open =
+  ({see '.' >> abort!} /
+   ({eat ' ' >> open!} /
+    ({eat ')' >> atom nil} /
+     {sexp! & cdr!}
+  )))!
+
+cdr [ReadLine, Abort] SExp
+cdr =
+  ({eat ' ' >> cdr!} /
+   ({eat '.' >> (sexp! << close!)} /
+    {open!}
+  ))!
+
+close [ReadLine, Abort] ()
+close =
+  ({eat ' ' >> close!} /
+   ({eat ')'} /
+    {abort!}
+  ))!
+
+elem Char (List Char) [] Bool
+elem c nil = ff
+elem c (c' :: cs) = if (c =Char= c') then {tt} else {elem c cs}
+
+name [ReadLine] List Char
+name = if (elem (peek!) (' ' :: ('(' :: (')' :: ('.' :: nil)))))
+  then {nil}
+  else {(peek! << nom!) :: name!}
+
+data Maybe X = no | yes X
+
+let X in {X -> [] Y} [] Y
+let x in f = f x
+
+noBS (Maybe Char) [ReadLine ? X] [Console] X
+noBS _ [x] = x
+noBS no [peek ? k] = let inch! in {c -> noBS (yes c) ? k c}
+noBS (yes c) [peek ? k] = noBS (yes c) ? k c
+noBS _ [nom ? k] = noBS no ? k ()
+
+data Stk X
+  = (Stk X) -peek {Char -> [ReadLine, Abort] X}
+  | (Stk X) -nom
+  | root {[ReadLine, Abort] X}
+
+withBS (Stk X) (Maybe Char) [ReadLine, Abort ? [{}] X] [Console] X
+withBS stk _ [x] = x
+withBS stk no [peek ? k] = let inch! in
+  { '\b' -> pop stk
+  | c -> withBS (stk -peek k) (yes c) ? k c
+  }
+withBS stk (yes c) [peek ? k] = withBS stk (yes c) ? k c
+withBS stk (yes c) [nom ? k] = ouch c >> withBS (stk -nom) no ? k ()
+withBS stk _ [aborting ? l] = pop stk
+
+note There's a need for indexing here, to prevent nom! before peek!
+
+pop (Stk X) [Console] X
+pop (stk -peek k) = withBS stk no ? k (peek!)
+pop (stk -nom) = ouch '\b' >> (ouch ' ' >> (ouch '\b' >> pop stk))
+pop (root r) = withBS (root r) no ? r!
+
+main [Console] SExp
+main = withBS (root {sexp!}) no ? sexp!
+
diff --git a/test.fk b/test.fk
new file mode 100644
--- /dev/null
+++ b/test.fk
@@ -0,0 +1,290 @@
+note
+  This is a test source file in the programming language Frank.
+
+note
+  Layout in Frank is really dumb. Each left-anchored line begins a new
+  top-level block, containing all the tokens until the next left-anchored
+  line. Other spacing is unimportant. A block beginning "note" is a comment.
+
+note
+  Frank's type system relates three notions
+    (1) value types, of things which *are*
+    (2) computation types, of things which *do*
+    (3) effect signatures, which specify what one *can*
+
+note
+  Some perfectly ordinary datatypes follow. List is parametrized.
+
+data Nat
+  = zero
+  | suc Nat
+
+data List X
+  = nil
+  | X :: (List X)
+
+note
+  Type constructors are always prefix and capitalized.
+  Type variables are always capitalized.
+  Value constructors are uncapitalized and form *templates*
+    with places given by the things which are types.
+  So :: is infix.
+
+note
+  Here are some perfectly ordinary functions.
+
+Nat + Nat [] Nat
+zero  + y = y
+suc x + y = suc (x + y)
+
+(List X) ++ (List X) [] List X
+nil        ++ ys = ys
+(x :: xs)  ++ ys = x :: (xs ++ ys)
+
+note
+  These definitions declare a function template, where the types show
+  the places for inputs. The [] (pronounced "returns") marks the end
+  of the template and the beginning of the output type.
+  You can drop [] (), if the output is the unit type.
+
+dull Nat
+dull zero = ()
+dull (suc n) = dull n
+
+note
+  An effect signature is also prefix and capitialized. It describes a
+  bunch of commands. Again [] means "returns" and you can drop [] ().
+
+sig State S
+  = get [] S
+  | set S
+
+note
+  Here's how to describe a way to run a stateful process.
+  The type [State S ? X] is the type of *requests* from stateful processes.
+  A request is either [x] ("return x", where x is an X) or
+  [command ? continuation].
+  Frank's ? construct allows a function from a request type to
+  *handle* a process.
+
+state S [State S ? X]  [] X
+state s [x]            = x
+state s [get ? k]      = state s ? k s
+state _ [set s ? k]    = state s ? k ()
+
+note
+  Unlike eff, Frank does not automatically compose the handler to the
+  continuation. Ultimately, there's no great difference in expressivity,
+  but this way is a little more first-order, and it's easier for the
+  handler to evolve. Here, for example, we handle the continuation for
+  set s using a suitably updated handler.
+
+
+note
+  Here's the Abort effect signature and one way to run it.
+  Frank currently does not allow polymorphic commands, so let's
+  use the empty type, {}.
+
+sig Abort
+  = aborting [] {}
+
+data Maybe X
+  = yes X
+  | no
+
+catch [Abort ? X] [] Maybe X
+catch [x]             = yes x
+catch [aborting ? k]  = no
+
+note
+  To invoke a command with no arguments, use a postfix "!". Without
+  arguments, a function symbol stands for the function itself, not the
+  result of invoking it. f is pure, but (f !) may not be.
+
+  Our aborting command has no arguments, so needs a !. It returns an
+  element of {}, which can be mapped to any type by the postfix {} operator,
+  pronounced "bunk".
+
+abort [Abort] X
+abort = aborting! {}
+
+
+note Nonempty {..}, pronounced "thunk", make a value type from a
+  computation type. You can think of a thunk as a "suspended
+  computation", and the fact that "suspenders" is American for
+  "braces" is handily mnemonic.  Frank distinguishes value type X (of
+  X values) from value type {[] X} of suspended computations that
+  return X values.
+
+  That distinction allows us to write control operators.
+
+note
+  Bool is built in, as if
+  data Bool = tt | ff
+
+if Bool then {[] X} else {[] X} [] X
+if tt then t else e = t!
+if ff then t else e = e!
+
+note The above if-then-else chooses which thunk to invoke. To
+  construct thunks, write expressions in {..}, so it looks
+  suspiciously like C. We may observe that
+
+    catch ? if tt then {zero} else {abort!}  =  yes zero
+
+  Contrast with the conditional function.
+
+cond Bool X X [] X
+cond tt t f = t
+cond ff t f = f
+
+note We'll find that
+
+    catch ? cons tt zero (abort!)  =  no
+
+  because the (abort!) is evaluated.
+
+
+note The reason [] is a bracket, not a :, is that it isn't always
+  empty.  It contains a bunch of signatures for effects the function
+  is allowed to do. Here's safe subtraction, which we can write
+  directly, thus.
+
+Nat - Nat [Abort] Nat
+x     - zero   = x
+zero  - suc y  = abort!
+suc x - suc y  = x - y
+
+note
+  You can invoke subtraction only where Abort is enabled, e.g., inside
+  catch. Frank programs are checked with respect to an ambient bunch of
+  signatures. The ? construct locally extends the ambient bunch of
+  signatures.
+
+note
+  Here's a little higher-order entertainment for you. A function type
+  is a computation type, and can thus be thunked. Thunks are always
+  pure, even if the function being thunked might perform some effects.
+  The inner [] could indeed contain some signatures, and if it does,
+  well, those signatures need to be enabled anywhere you *invoke* the
+  function.
+
+map {A -> [] B} (List A) [] List B
+map f nil        = nil
+map f (a :: as)  = f a :: map f as
+
+note
+  You are at liberty to suppress an empty [] in a computation type,
+  but be aware! When you write a function type, each [sigs] it contains
+  is really an *action* on the ambient signature, meaning "sigs extending
+  the ambient signature". That's to say, the types are ever so slightly
+  effect-polymorphic. For map, below, the meaning is that whatever effects
+  are available when map is invoked may be used at each element, too. Our
+  map is really Haskell's "mapM". The upshot is that you can write this:
+
+subs (List Nat) Nat [Abort] List Nat
+subs xs n = map {m -> m - n} xs
+
+note
+  But there's a subtlety. Consider trees represented with functional
+  branching. Each node packs a *pure* function from Bool.
+
+data Tree X
+  = leaf X
+  | node {Bool -> Tree X}
+
+note
+  The following definition of tree mapping is disallowed
+
+  tmap {A -> B} (Tree A) [] Tree B
+  tmap f (leaf a)  = leaf (f a)
+  tmap f (node g)  = node {b -> tmap f (g b)}
+
+  The type of f, longhand, is {A -> [] B} meaning that f can do
+  whatever the ambient effects are when tmap is invoked. But we
+  use f inside a node, where the function must be pure, so the
+  typechecker refuses.
+
+  The following is, however, accepted. Here, the signature in f's type
+  says {}, which as a signature is pronounced "pure". Its action on
+  the ambient signature is to empty it.
+
+tmap {A -> [{}] B} (Tree A) [] Tree B
+tmap f (leaf a)  = leaf (f a)
+tmap f (node g)  = node {b -> tmap f (g b)}
+
+note
+  You can't make a dangerous, nearly broken tree, like this.
+
+  subt (Tree Nat) Nat [Abort] Tree Nat
+  subt xt n = tmap {m -> m - n} xt
+
+note
+  But safe mapping is ok.
+
+addt (Tree Nat) Nat [] Tree Nat
+addt xt n = tmap {m -> m + n} xt
+
+note
+  Of course you can do something like.
+
+mkNode (Tree X) (Tree X) [] Tree X
+mkNode l r = node {tt -> l | ff -> r}
+
+tmapOk {A -> B} (Tree A) [] Tree B
+tmapOk f (leaf a) = leaf (f a)
+tmapOk f (node g) = mkNode (tmapOk f (g tt)) (tmapOk f (g ff))
+
+
+note
+  Here's a bit of stateful fun.
+  The defined command "bong" returns the value of a Boolean state
+  but flips it.
+
+not Bool [] Bool
+not tt = ff
+not ff = tt
+
+X but () [] X
+x but c = x
+
+bong [State Bool] Bool
+bong = get! but set (not (get!))
+
+
+note
+  So if we define pairing...
+
+data Pair A B = A & B
+
+note
+  ...we get
+
+   state ff ? bong! & bong!  =  ff & tt
+
+
+note
+  Bits and Pieces for examples
+
+two [] Nat
+two = suc (suc zero)
+
+note
+  I must allow the definition of non-functional values.
+
+note
+  main [] Nat
+  main = two! + two!
+
+note
+  main [] Maybe Nat
+  main = catch ? if tt then {zero} else {abort!}
+
+note
+  main [Abort] List Nat
+  main = subs (two ! :: (two ! :: nil)) (suc zero)
+
+main [Console] Char
+main = inch!
+
+