chrisdone · October 11, 2025 13:03 · Nov 12, 2014 · Nov 12, 2014 · Nov 12, 2014 · Nov 12, 2014
diff --git a/BCommentary.md b/BCommentary.md
@@ -23,16 +23,20 @@ So `~` ends up sitting somewhere in between a lambda and a quote.
 
 I should be able to write:
 
-    (defmacro when (p body)
-      ~(if ,p
-           ,body
-         ()))
+``` lisp
+(defmacro when (p body)
+  ~(if ,p
+       ,body
+       ()))
+```
 
 And then the macro `when` will have type: `'Bool -> '() -> '()`, if that makes sense. I cannot write, for example, `(when 123 "go!")`. This would be rejected before the macro is even expanded. A well-typed macro is interesting. Haskell doesn't have normal Lisp symbolic quotation, you can't just write `'foo`, therefore I don't consider Haskell or its ML ancestors to be part of the Lisps family. It does have `'foo`, it instead requires that `foo` exists as a name in scope. But it doesn't encode any type information, which is not very Haskelly either.
 
 There's also the tricky problem of `eval`. In regular Lisp, `eval` throws exceptions. In even Shen this is true, because its quotation is not type-safe. Whereas if your eval is like in my little Lisp:
 
-    eval :: 'a -> a
+``` haskell
+eval :: 'a -> a
+```
 
 Then the quoted symbol carries the type information and means that eval will at least never produce a type error.
 

diff --git a/AnIntro.md b/AnIntro.md
@@ -1,45 +1,3 @@
-**Note:** I noticed this was posted to [/r/programming](http://www.reddit.com/r/programming/comments/2m262n/statically_typed_lisp/) but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed and what that might feel like. I'll have to implement at least `case` and `let` in order to deconstruct the quoted expressions and implement `eval` similar to [Roots of Lisp](http://ep.yimg.com/ty/cdn/paulgraham/jmc.lisp) before I can answer that to my satisfaction. 
-
-Including the reply I wrote in that thread:
-
-As the author of this gist, static typing in general isn't the goal. There are a bunch of statically typed Lisps.
-
-Shen has the type `symbol` for quoted things:
-
-* `'+` : `symbol`
-
-My lisp has two types of quotation:
-
-* `'+` :: 'Symbol
-* `~+` :: '(Int -> Int -> Int)
-
-I'm not quite decided whether I want staged lambda-calculus, or this mixing style. What you end up with is a kind of non-opaque lambda:
-
-* `(lambda (x) (+ x x))` — this is opaque, you can't "look inside" this lambda. But it means the things inside can be statically typed.
-* `'(lambda (x) (+ x x))` — this is transparent, you can look inside the lambda. It's just a tree. It's not typed, the whole thing is just "symbol" or "tree of symbols".
-* `~(lambda (x) (+ x x))` — this is both transparent and statically typed. The `+` must exist, which it does, and have a type, which it does, `Int -> Int -> Int`, therefore the type of  the `x`s must be `Int`. So the whole expression has type: `'(Int -> Int)`. Note the `'`, meaning "a quoted thing of type X".
-
-So `~` ends up sitting somewhere in between a lambda and a quote.
-
-I should be able to write:
-
-    (defmacro when (p body)
-      ~(if ,p
-           ,body
-         ()))
-
-And then the macro `when` will have type: `'Bool -> '() -> '()`, if that makes sense. I cannot write, for example, `(when 123 "go!")`. This would be rejected before the macro is even expanded. A well-typed macro is interesting. Haskell doesn't have normal Lisp symbolic quotation, you can't just write `'foo`, therefore I don't consider Haskell or its ML ancestors to be part of the Lisps family. It does have `'foo`, it instead requires that `foo` exists as a name in scope. But it doesn't encode any type information, which is not very Haskelly either.
-
-There's also the tricky problem of `eval`. In regular Lisp, `eval` throws exceptions. In even Shen this is true, because its quotation is not type-safe. Whereas if your eval is like in my little Lisp:
-
-    eval :: 'a -> a
-
-Then the quoted symbol carries the type information and means that eval will at least never produce a type error.
-
-Whether this works in practice I've yet to determine/decide. It's just an idea that interested me.
-
---
-
 Basic unit type:
 
 ``` haskell

diff --git a/BCommentary.md b/BCommentary.md
@@ -0,0 +1,39 @@
+**Note:** I noticed this was posted to [/r/programming](http://www.reddit.com/r/programming/comments/2m262n/statically_typed_lisp/) but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed and what that might feel like. I'll have to implement at least `case` and `let` in order to deconstruct the quoted expressions and implement `eval` similar to [Roots of Lisp](http://ep.yimg.com/ty/cdn/paulgraham/jmc.lisp) before I can answer that to my satisfaction. 
+
+Including the reply I wrote in that thread:
+
+As the author of this gist, static typing in general isn't the goal. There are a bunch of statically typed Lisps.
+
+Shen has the type `symbol` for quoted things:
+
+* `'+` : `symbol`
+
+My lisp has two types of quotation:
+
+* `'+` :: 'Symbol
+* `~+` :: '(Int -> Int -> Int)
+
+I'm not quite decided whether I want staged lambda-calculus, or this mixing style. What you end up with is a kind of non-opaque lambda:
+
+* `(lambda (x) (+ x x))` — this is opaque, you can't "look inside" this lambda. But it means the things inside can be statically typed.
+* `'(lambda (x) (+ x x))` — this is transparent, you can look inside the lambda. It's just a tree. It's not typed, the whole thing is just "symbol" or "tree of symbols".
+* `~(lambda (x) (+ x x))` — this is both transparent and statically typed. The `+` must exist, which it does, and have a type, which it does, `Int -> Int -> Int`, therefore the type of  the `x`s must be `Int`. So the whole expression has type: `'(Int -> Int)`. Note the `'`, meaning "a quoted thing of type X".
+
+So `~` ends up sitting somewhere in between a lambda and a quote.
+
+I should be able to write:
+
+    (defmacro when (p body)
+      ~(if ,p
+           ,body
+         ()))
+
+And then the macro `when` will have type: `'Bool -> '() -> '()`, if that makes sense. I cannot write, for example, `(when 123 "go!")`. This would be rejected before the macro is even expanded. A well-typed macro is interesting. Haskell doesn't have normal Lisp symbolic quotation, you can't just write `'foo`, therefore I don't consider Haskell or its ML ancestors to be part of the Lisps family. It does have `'foo`, it instead requires that `foo` exists as a name in scope. But it doesn't encode any type information, which is not very Haskelly either.
+
+There's also the tricky problem of `eval`. In regular Lisp, `eval` throws exceptions. In even Shen this is true, because its quotation is not type-safe. Whereas if your eval is like in my little Lisp:
+
+    eval :: 'a -> a
+
+Then the quoted symbol carries the type information and means that eval will at least never produce a type error.
+
+Whether this works in practice I've yet to determine/decide. It's just an idea that interested me.
diff --git a/AnIntro.md b/AnIntro.md
@@ -1,5 +1,43 @@
 **Note:** I noticed this was posted to [/r/programming](http://www.reddit.com/r/programming/comments/2m262n/statically_typed_lisp/) but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed and what that might feel like. I'll have to implement at least `case` and `let` in order to deconstruct the quoted expressions and implement `eval` similar to [Roots of Lisp](http://ep.yimg.com/ty/cdn/paulgraham/jmc.lisp) before I can answer that to my satisfaction. 
 
+Including the reply I wrote in that thread:
+
+As the author of this gist, static typing in general isn't the goal. There are a bunch of statically typed Lisps.
+
+Shen has the type `symbol` for quoted things:
+
+* `'+` : `symbol`
+
+My lisp has two types of quotation:
+
+* `'+` :: 'Symbol
+* `~+` :: '(Int -> Int -> Int)
+
+I'm not quite decided whether I want staged lambda-calculus, or this mixing style. What you end up with is a kind of non-opaque lambda:
+
+* `(lambda (x) (+ x x))` — this is opaque, you can't "look inside" this lambda. But it means the things inside can be statically typed.
+* `'(lambda (x) (+ x x))` — this is transparent, you can look inside the lambda. It's just a tree. It's not typed, the whole thing is just "symbol" or "tree of symbols".
+* `~(lambda (x) (+ x x))` — this is both transparent and statically typed. The `+` must exist, which it does, and have a type, which it does, `Int -> Int -> Int`, therefore the type of  the `x`s must be `Int`. So the whole expression has type: `'(Int -> Int)`. Note the `'`, meaning "a quoted thing of type X".
+
+So `~` ends up sitting somewhere in between a lambda and a quote.
+
+I should be able to write:
+
+    (defmacro when (p body)
+      ~(if ,p
+           ,body
+         ()))
+
+And then the macro `when` will have type: `'Bool -> '() -> '()`, if that makes sense. I cannot write, for example, `(when 123 "go!")`. This would be rejected before the macro is even expanded. A well-typed macro is interesting. Haskell doesn't have normal Lisp symbolic quotation, you can't just write `'foo`, therefore I don't consider Haskell or its ML ancestors to be part of the Lisps family. It does have `'foo`, it instead requires that `foo` exists as a name in scope. But it doesn't encode any type information, which is not very Haskelly either.
+
+There's also the tricky problem of `eval`. In regular Lisp, `eval` throws exceptions. In even Shen this is true, because its quotation is not type-safe. Whereas if your eval is like in my little Lisp:
+
+    eval :: 'a -> a
+
+Then the quoted symbol carries the type information and means that eval will at least never produce a type error.
+
+Whether this works in practice I've yet to determine/decide. It's just an idea that interested me.
+
 --
 
 Basic unit type:

diff --git a/AnIntro.md b/AnIntro.md
@@ -1,4 +1,4 @@
-**Note:** I noticed this was posted to /r/programming but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed and what that might feel like. I'll have to implement at least `case` and `let` in order to deconstruct the quoted expressions before I can answer that to my satisfaction. 
+**Note:** I noticed this was posted to [/r/programming](http://www.reddit.com/r/programming/comments/2m262n/statically_typed_lisp/) but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed and what that might feel like. I'll have to implement at least `case` and `let` in order to deconstruct the quoted expressions and implement `eval` similar to [Roots of Lisp](http://ep.yimg.com/ty/cdn/paulgraham/jmc.lisp) before I can answer that to my satisfaction. 
 
 --
 

diff --git a/AnIntro.md b/AnIntro.md
@@ -1,4 +1,4 @@
-**Note:** I noticed this was posted to /r/programming but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed.
+**Note:** I noticed this was posted to /r/programming but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed and what that might feel like. I'll have to implement at least `case` and `let` in order to deconstruct the quoted expressions before I can answer that to my satisfaction. 
 
 --
 

diff --git a/AnIntro.md b/AnIntro.md
@@ -1,3 +1,7 @@
+**Note:** I noticed this was posted to /r/programming but it's far from complete, it doesn't even have numbers or `let/if/case` special operators. It was just a Friday evening's whim to research whether quotation can be practically statically typed.
+
+--
+
 Basic unit type:
 
 ``` haskell

diff --git a/Type.hs b/Type.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE FlexibleContexts #-}

diff --git a/AnIntro.md b/AnIntro.md
@@ -32,6 +32,9 @@ Standard quotation:
 ``` haskell
 λ> replTy "'()"
 '() :: 'Symbol
+λ> repl "'(foo bar)"
+'(foo bar) :: 'Symbol
+(foo bar)
 ```
 
 Statically typed quotation:

diff --git a/AnIntro.md b/AnIntro.md
@@ -23,8 +23,8 @@ Statically typed:
 
 ``` haskell
 λ> repl "(() (fn x x))"
-*** Exception: Couldn't match expected type: ()
-against type: (b -> b) -> e
+-- *** Exception: Couldn't match expected type: ()
+-- against type: (b -> b) -> e
 ```
 
 Standard quotation:
@@ -47,7 +47,7 @@ in scope:
 
 ``` haskell
 λ> repl "~a"
-*** Exception: Not in scope: `a'
+-- *** Exception: Not in scope: `a'
 ```
 
 Quoted function:
@@ -78,8 +78,8 @@ won't accept anything not quoted:
 
 ``` haskell
 λ> replTy "(eval ())"
-*** Exception: Couldn't match expected type: 'a
-against type: ()
+-- *** Exception: Couldn't match expected type: 'a
+-- against type: ()
 ```
 
 If given a symbolic quoted expression, it will just return it as-is:

diff --git a/AnIntro.md b/AnIntro.md
@@ -1,13 +1,13 @@
 Basic unit type:
 
-``` lisp
+``` haskell
 λ> replTy "()"
 () :: ()
 ```
 
 Basic functions:
 
-``` lisp
+``` haskell
 λ> replTy "(fn x x)"
 (fn x x) :: b -> b
 
@@ -21,22 +21,22 @@ Basic functions:
 
 Statically typed:
 
-``` lisp
+``` haskell
 λ> repl "(() (fn x x))"
 *** Exception: Couldn't match expected type: ()
 against type: (b -> b) -> e
 ```
 
 Standard quotation:
 
-``` lisp
+``` haskell
 λ> replTy "'()"
 '() :: 'Symbol
 ```
 
 Statically typed quotation:
 
-``` lisp
+``` haskell
 λ> replTy "~()"
 ~() :: '()
 ```
@@ -45,21 +45,21 @@ All quotes have type `'a`. Normal symbolic Lisp style is `'Symbol`,
 quoting anything else, e.g. for unit, is `'()`. Also things have to be
 in scope:
 
-``` lisp
+``` haskell
 λ> repl "~a"
 *** Exception: Not in scope: `a'
 ```
 
 Quoted function:
 
-``` lisp
+``` haskell
 λ> replTy "'(fn x x)"
 '(fn x x) :: 'Symbol
 ```
 
 Quoted function:
 
-``` lisp
+``` haskell
 λ> replTy "~(fn x x)"
 ~(fn x x) :: '(b -> b)
 ```
@@ -68,23 +68,23 @@ Notice the type is `'(b -> b)`.
 
 There's an `eval` function:
 
-``` lisp
+``` haskell
 λ> replTy "eval"
 eval :: 'a -> a
 ```
 
 It accepts a quoted `a` and returns the `a` that it represents. It
 won't accept anything not quoted:
 
-``` lisp
+``` haskell
 λ> replTy "(eval ())"
 *** Exception: Couldn't match expected type: 'a
 against type: ()
 ```
 
 If given a symbolic quoted expression, it will just return it as-is:
 
-``` lisp
+``` haskell
 λ> repl "(eval '())"
 (eval '()) :: Symbol
 ()
@@ -95,7 +95,7 @@ If given a symbolic quoted expression, it will just return it as-is:
 
 Given a well-typed quoted expression it will run the code:
 
-``` lisp
+``` haskell
 λ> repl "(eval ~((fn x x) '()))"
 (eval ~((fn x x) '())) :: 'Symbol
 ()

diff --git a/AnIntro.md b/AnIntro.md
@@ -1,13 +1,13 @@
 Basic unit type:
 
-``` haskell
+``` lisp
 λ> replTy "()"
 () :: ()
 ```
 
 Basic functions:
 
-``` haskell
+``` lisp
 λ> replTy "(fn x x)"
 (fn x x) :: b -> b
 
@@ -21,22 +21,22 @@ Basic functions:
 
 Statically typed:
 
-``` haskell
+``` lisp
 λ> repl "(() (fn x x))"
 *** Exception: Couldn't match expected type: ()
 against type: (b -> b) -> e
 ```
 
 Standard quotation:
 
-``` haskell
+``` lisp
 λ> replTy "'()"
 '() :: 'Symbol
 ```
 
 Statically typed quotation:
 
-``` haskell
+``` lisp
 λ> replTy "~()"
 ~() :: '()
 ```
@@ -45,21 +45,21 @@ All quotes have type `'a`. Normal symbolic Lisp style is `'Symbol`,
 quoting anything else, e.g. for unit, is `'()`. Also things have to be
 in scope:
 
-``` haskell
+``` lisp
 λ> repl "~a"
 *** Exception: Not in scope: `a'
 ```
 
 Quoted function:
 
-``` haskell
+``` lisp
 λ> replTy "'(fn x x)"
 '(fn x x) :: 'Symbol
 ```
 
 Quoted function:
 
-``` haskell
+``` lisp
 λ> replTy "~(fn x x)"
 ~(fn x x) :: '(b -> b)
 ```
@@ -68,23 +68,23 @@ Notice the type is `'(b -> b)`.
 
 There's an `eval` function:
 
-``` haskell
+``` lisp
 λ> replTy "eval"
 eval :: 'a -> a
 ```
 
 It accepts a quoted `a` and returns the `a` that it represents. It
 won't accept anything not quoted:
 
-``` haskell
+``` lisp
 λ> replTy "(eval ())"
 *** Exception: Couldn't match expected type: 'a
 against type: ()
 ```
 
 If given a symbolic quoted expression, it will just return it as-is:
 
-``` haskell
+``` lisp
 λ> repl "(eval '())"
 (eval '()) :: Symbol
 ()
@@ -95,7 +95,7 @@ If given a symbolic quoted expression, it will just return it as-is:
 
 Given a well-typed quoted expression it will run the code:
 
-``` haskell
+``` lisp
 λ> repl "(eval ~((fn x x) '()))"
 (eval ~((fn x x) '())) :: 'Symbol
 ()

diff --git a/AnIntro.md b/AnIntro.md
@@ -0,0 +1,105 @@
+Basic unit type:
+
+``` haskell
+λ> replTy "()"
+() :: ()
+```
+
+Basic functions:
+
+``` haskell
+λ> replTy "(fn x x)"
+(fn x x) :: b -> b
+
+λ> replTy "((fn x ()) (fn x x))"
+((fn x ()) (fn x x)) :: ()
+
+λ> repl "((fn x x) (fn x x))"
+((fn x x) (fn x x)) :: c -> c
+(fn x x)
+```
+
+Statically typed:
+
+``` haskell
+λ> repl "(() (fn x x))"
+*** Exception: Couldn't match expected type: ()
+against type: (b -> b) -> e
+```
+
+Standard quotation:
+
+``` haskell
+λ> replTy "'()"
+'() :: 'Symbol
+```
+
+Statically typed quotation:
+
+``` haskell
+λ> replTy "~()"
+~() :: '()
+```
+
+All quotes have type `'a`. Normal symbolic Lisp style is `'Symbol`,
+quoting anything else, e.g. for unit, is `'()`. Also things have to be
+in scope:
+
+``` haskell
+λ> repl "~a"
+*** Exception: Not in scope: `a'
+```
+
+Quoted function:
+
+``` haskell
+λ> replTy "'(fn x x)"
+'(fn x x) :: 'Symbol
+```
+
+Quoted function:
+
+``` haskell
+λ> replTy "~(fn x x)"
+~(fn x x) :: '(b -> b)
+```
+
+Notice the type is `'(b -> b)`.
+
+There's an `eval` function:
+
+``` haskell
+λ> replTy "eval"
+eval :: 'a -> a
+```
+
+It accepts a quoted `a` and returns the `a` that it represents. It
+won't accept anything not quoted:
+
+``` haskell
+λ> replTy "(eval ())"
+*** Exception: Couldn't match expected type: 'a
+against type: ()
+```
+
+If given a symbolic quoted expression, it will just return it as-is:
+
+``` haskell
+λ> repl "(eval '())"
+(eval '()) :: Symbol
+()
+λ> repl "(eval '((fn x x) '()))"
+(eval '((fn x x) '())) :: Symbol
+((fn x x) ())
+```
+
+Given a well-typed quoted expression it will run the code:
+
+``` haskell
+λ> repl "(eval ~((fn x x) '()))"
+(eval ~((fn x x) '())) :: 'Symbol
+()
+λ> repl "(eval ~((fn x x) ()))"
+(eval ~((fn x x) ())) :: ()
+()
+```
diff --git a/Type.hs b/Type.hs
@@ -0,0 +1,348 @@
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+-- | Statically typed Lisp with typed quotation.
+
+module Type where
+
+import           Control.Applicative
+import           Control.Arrow ((***))
+import           Control.Monad.State.Strict
+import           Control.Monad.Writer
+import           Data.Attoparsec.Text (Parser)
+import qualified Data.Attoparsec.Text as P
+import           Data.Char
+import           Data.Map (Map)
+import qualified Data.Map as M
+import           Data.Set (Set)
+import qualified Data.Set as S
+import           Data.String
+import           Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+
+--------------------------------------------------------------------------------
+-- Types
+
+-- | A type.
+data Type
+  = VarTy (Name Type)
+  | FunTy Type Type
+  | UnitTy
+  | SymbolTy
+  | QuotedTy Type
+  deriving (Ord,Eq,Show)
+
+-- | An expression.
+data Exp
+  = Var (Name Exp)
+  | Fun (Name Exp) Type Exp
+  | Unit
+  | App Exp Exp
+  | TypedQuote Exp
+  | Quote Exp
+  | Eval (Exp -> Exp)
+
+-- | A name for some thing.
+newtype Name a = Name Text
+  deriving (Ord,Eq,Show)
+
+-- | A stream type.
+data Stream a =
+  Stream a (Stream a)
+
+--------------------------------------------------------------------------------
+-- REPL
+
+repl :: Text -> IO ()
+repl inp =
+  case P.parseOnly (ex nameStream <* P.endOfInput)
+                   inp of
+    Left err -> error err
+    Right (std -> expr,stream) ->
+      do T.putStrLn
+           (inp <> " :: " <>
+            prettyType (typeOf expr stream))
+         T.putStrLn
+           (prettyExp (eval expr))
+
+replTy :: Text -> IO ()
+replTy inp =
+  case P.parseOnly (ex nameStream <* P.endOfInput)
+                   inp of
+    Left err -> error err
+    Right (std -> expr,stream) ->
+      T.putStrLn
+        (inp <> " :: " <>
+         prettyType (typeOf expr stream))
+
+replCheck :: Text -> IO ()
+replCheck inp =
+  case P.parseOnly (ex nameStream <* P.endOfInput)
+                   inp of
+    Left err -> error err
+    Right (std -> expr,stream) ->
+      print ((prettyType ***
+              S.map (prettyType *** prettyType)) (evalState (check mempty expr) stream))
+
+--------------------------------------------------------------------------------
+-- Stdlib stuff
+
+-- | Bind standard library things.
+std :: Exp -> Exp
+std e =
+  (App (Fun (Name "eval")
+            (FunTy (QuotedTy (VarTy "a"))
+                   (VarTy "a"))
+            e)
+       (Eval eval))
+
+--------------------------------------------------------------------------------
+-- Parser
+
+ex :: Stream (Name Type) -> Parser (Exp,Stream (Name Type))
+ex ss = quote ss <|> tquote ss <|> app ss <|> fn ss <|> unit ss <|> var ss
+  where tquote s =
+          P.string "~" *>
+          fmap (\(x,s') -> (TypedQuote x,s'))
+               (ex s)
+        quote s =
+          P.string "'" *>
+          fmap (\(x,s') -> (Quote x,s'))
+               (ex s)
+        var s = fmap (\x -> (Var x,s)) ident
+        fn s =
+          do void (P.string "(fn ")
+             P.skipSpace
+             i <- ident
+             void P.space
+             P.skipSpace
+             (body,Stream n s') <- ex s
+             void (P.string ")")
+             return (Fun i (VarTy n) body,s')
+        app s =
+          do void (P.string "(")
+             (op,s') <- ex s
+             void P.space
+             P.skipSpace
+             (arg,s'') <- ex s'
+             void (P.string ")")
+             return (App op arg,s'')
+        unit s =
+          P.string "()" *>
+          pure (Unit,s)
+        ident :: Parser (Name a)
+        ident =
+          do c <- P.letter
+             cs <- P.takeWhile (\ch -> isLetter ch || isDigit ch)
+             return (Name (T.singleton c <> cs))
+
+--------------------------------------------------------------------------------
+-- Interpreter
+
+-- | Eval expression.
+eval :: Exp -> Exp
+eval (App op arg) =
+  case eval op of
+    Eval f ->
+      case arg of
+        TypedQuote e -> eval e
+        Quote e -> e
+        _ ->
+          error "Can only eval things of type 'a."
+    Fun param _ expr ->
+      case eval arg of
+        a@Var{} ->
+          error (T.unpack (prettyExp a <> " is not in scope"))
+        a -> eval (subst param a expr)
+    _ ->
+      error (T.unpack (prettyExp op <> " is not a function"))
+eval e@(Var{}) =
+  error (T.unpack (prettyExp e <> " is not in scope!"))
+eval e = e
+
+-- | Substitute name in function body.
+subst :: Name Exp -> Exp -> Exp -> Exp
+subst name val e@(Var name')
+  | name == name' = val
+  | otherwise = e
+subst name val (Fun name' ty e)
+  | name /= name' = Fun name' ty (subst name val e)
+subst name val (App f a) =
+  App (subst name val f) (subst name val a)
+--
+-- TODO: retain original name in quotes:
+--
+-- λ> repl "((fn f ~f) (fn a a))"
+-- ((fn f ~f) (fn a a)) :: '(c -> c)
+-- (fn a a)
+--
+-- This should really produce: f
+-- But it doesn't due to dumb beta reduction.
+--
+subst name val (TypedQuote e) =
+  TypedQuote (subst name val e)
+subst _ _ e = e
+
+--------------------------------------------------------------------------------
+-- Type checker
+
+-- | Get the type of the expression.
+typeOf :: Exp -> Stream (Name Type) -> Type
+typeOf t stream =
+  case evalState (check mempty t) stream of
+    (ty,cs) -> let s = evalState (unify (S.toList cs)) ()
+               in replace s ty
+
+-- | Check the exp with the given context.
+check :: MonadState (Stream (Name Type)) m
+      => Map (Name Exp) Type -> Exp -> m (Type,Set (Type,Type))
+check ctx expr =
+  case expr of
+    Var name@(Name text) ->
+      case M.lookup name ctx of
+        Nothing ->
+          error ("Not in scope: `" <> T.unpack text <> "'")
+        Just typ -> return (typ,mempty)
+    Fun x xty body ->
+      do (rty,cs) <- check (M.insert x xty ctx) body
+         return (FunTy xty rty,cs)
+    Unit -> return (UnitTy,mempty)
+    App f x ->
+      do (fty,cs1) <- check ctx f
+         (xty,cs2) <- check ctx x
+         sym <- genSym
+         let rty = VarTy sym
+             cs =
+               S.insert (fty,FunTy xty rty)
+                        (cs1 <> cs2)
+         return (rty,cs)
+    TypedQuote e ->
+      do (qty,cs) <- check ctx e
+         return (QuotedTy qty,cs)
+    Quote{} -> return (QuotedTy SymbolTy,mempty)
+    Eval _ ->
+      do ty <- genSym
+         return (VarTy ty,mempty)
+
+-- | Unify the list of constraints.
+unify :: Monad m => [(Type,Type)] -> m (Map (Name Type) Type)
+unify [] = return mempty
+unify ((a,b):cs)
+  | a == b = unify cs
+  | VarTy v <- a =
+    if occurs v b
+       then error (T.unpack ("Occurs check: " <> prettyType a <> " ~ " <>
+                             prettyType b))
+       else let subbed = M.singleton v b
+            in do rest <- unify (substitute subbed cs)
+                  return (rest <> subbed)
+  | VarTy v <- b =
+    if occurs v a
+       then error (T.unpack ("Occurs check: " <> prettyType a <> " ~ " <>
+                             prettyType b))
+       else let subbed = M.singleton v a
+            in do rest <- unify (substitute subbed cs)
+                  return (rest <> subbed)
+  | FunTy a1 b1 <- a
+  , FunTy a2 b2 <- b =
+    unify ([(a1,a2),(b1,b2)] <>
+           cs)
+  | QuotedTy a1 <- a
+  , QuotedTy b1 <- b =
+    unify ([(a1,b1)] <> cs)
+  | otherwise =
+    error (T.unpack ("Couldn't match expected type: " <> prettyType a <>
+                     "\nagainst type: " <> prettyType b))
+
+-- | Occurs check.
+occurs :: Name Type -> Type -> Bool
+occurs x (VarTy y)
+  | x == y = True
+  | otherwise = False
+occurs x (FunTy a b) =
+  occurs x a ||
+  occurs x b
+occurs x (QuotedTy t) = occurs x t
+occurs _ UnitTy = False
+occurs _ SymbolTy = False
+
+-- | Substitute the unified type into the constraints.
+substitute :: Map (Name Type) Type -> [(Type,Type)] -> [(Type,Type)]
+substitute subs = map go
+  where go (a,b) = (replace subs a,replace subs b)
+
+-- | Apply a substitution to a type.
+replace :: Map (Name Type) Type -> Type -> Type
+replace s' t' = M.foldrWithKey go t' s'
+  where go s1 t (VarTy s2)
+          | s1 == s2 = t
+          | otherwise = VarTy s2
+        go s t (FunTy t2 t3) =
+          FunTy (go s t t2)
+                (go s t t3)
+        go s t (QuotedTy qt) =
+          QuotedTy (go s t qt)
+        go _ _ UnitTy = UnitTy
+        go _ _ SymbolTy = SymbolTy
+
+-- | Generate a new name for a type.
+genSym :: MonadState (Stream (Name Type)) m => m (Name Type)
+genSym = do Stream next stream <- get
+            put stream
+            return next
+
+-- | An infinite stream of names.
+nameStream :: Stream (Name Type)
+nameStream = go 'b' (0 :: Integer)
+  where go c n =
+          Stream (Name (T.pack (c :
+                                if n == 0
+                                   then ""
+                                   else show n)))
+                 (go (toEnum (fromEnum 'a' + (mod (fromEnum c - fromEnum 'a' + 1) 26)))
+                     (if c == 'z'
+                         then n + 1
+                         else n))
+
+--------------------------------------------------------------------------------
+-- Pretty printing
+
+-- | Pretty printing for type.
+prettyType :: Type -> Text
+prettyType = go
+  where go t =
+          case t of
+            UnitTy -> "()"
+            SymbolTy -> "Symbol"
+            VarTy (Name n) -> n
+            FunTy a b -> (case a of
+                            FunTy{} -> "(" <> go a <> ")"
+                            _ -> go a)
+                           <> " -> " <> go b
+            QuotedTy qt ->
+              "'" <>
+              case qt of
+                FunTy{} -> "(" <> go qt <> ")"
+                _ -> go qt
+
+-- | Pretty printing for expression.
+prettyExp :: Exp -> Text
+prettyExp = go
+  where go t =
+          case t of
+            Unit -> "()"
+            Var (Name name) -> name
+            Fun (Name n) _ty e -> "(fn " <> n <> " " <> go e <> ")"
+            App f x -> "(" <> go f <> " " <> go x <> ")"
+            TypedQuote e -> go e
+            Quote e -> go e
+            Eval _ -> "eval"
+
+--------------------------------------------------------------------------------
+-- Instances
+
+-- | Handy for debugging.
+instance IsString (Name a) where
+  fromString = Name . fromString
No results found