diff --git a/hm-inference/README.md b/hm-inference/README.md
new file mode 100644
index 0000000..e2a6f46
--- /dev/null
+++ b/hm-inference/README.md
@@ -0,0 +1,48 @@
+# Type Inference
+
+This is a prototype before Rust implementation of the algorithm.
+
+## Implemented Features
+- Primitive types: bool, float, integer. (limited magic methods are implemented,
+    no casting for now)
+- Statements:
+    - For loop.
+    - While loop.
+    - If expression.
+    - Simple assignment. (without type annotation, allows pattern matcing for
+        tuples)
+- Expressions:
+    - Boolean operations.
+    - Binary operations. (+, -, *, /, //)
+    - Compare.
+    - Function call. (posargs/kwargs/optional are supported)
+    - Lambda.
+    - Object Attribute.
+    - List/tuple subscript. (tuple requires constant indexing)
+    - Virtual.
+    - Constraints for type variables.
+
+User can define functions/types by adding them to the prelude.
+
+Note that variables can be used before definition for now, we would do another
+pass after type checking to prevent this. The pass would also check for return.
+
+## TODO
+- Parse class/function definition.
+- Occur check to prevent infinite function types.
+- Pretty print for types. (especially type variables)
+- Better error message. (we did not keep any context for now)
+
+## Implementation Notes
+
+- Type variables would now retain a lot of information, including fields and its
+  range for later checking.
+- Function type is seperated from call type. We maintain a list of calls to the
+  same function (potentially with different type signature) to allow different
+  instantiation of the same function.
+- We store the list of calls and the list of virtual types, and check the
+  constraints at the end of the type inference phase. E.g. check subtyping
+  relationship, check whether the type variable can be instantiated to a certain
+  type.
+
+