diff --git a/TODO.md b/TODO.md
index d8d0b63..610484c 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,30 @@
+#Typechecking Notes
+
+(cf. cardelli paper)
+
+Given a length function def:
+````
+fn length(x) {
+ if x.is_null {
+   0
+  } else {
+   succ(length(x.tail))
+  }
+}
+````
+Constraints:
+.null: List a -> bool
+.tail: List a -> List a
+0: Nat
+succ: Nat -> Nat
+
+
+
 
 # TODO Items
 
+-make the REPL more advanced!
+
 -Plan of attack:
   -write a visitor pattern for AST
   -convert AST type to including SourceMap'd wrappers (w/ .into())