README.md

@@ -181,6 +181,10 @@ class Foo(EnvExperiment):
   in area outside generics.
 * Type variable cannot occur alone in the result type, i.e. must be bound to the
   input parameters.
+* Polymorphic methods (with type variables in the type signature) must be
+  annotated with `@final`. This is because we need to know where does the method
+  come from when we do monomorphization, which we don't know for virtual
+  methods.
 
 ## For loop unrolling (#12)
 A pseudocomment can be used for unrolling for loops that iterates a fixed amount
@@ -193,6 +197,60 @@ for p in params:
     print(p)
 ```
 
+## Dynamic Dispatch
+Type annotations are invariant, so subtype (derived types) cannot be used
+when the base type is expected. Example:
+```python
+class Base:
+    def foo(self) -> int:
+        return 1
+
+class Derived(Base):
+    def foo(self) -> int:
+        return 2
+
+def bar(x: list[Base]) -> int:
+    sum = 0
+    for v in x:
+        sum += v.foo()
+    return sum
+
+# incorrect, this list cannot be typed (inhomogeneous)
+bar([Base(), Derived()])
+```
+
+Dynamic dispatch is supported, but requires explicit annotation, similar to
+[trait object](https://doc.rust-lang.org/book/ch17-02-trait-objects.html) in rust.
+`virtual[T]` is the type for `T` and its subtypes(derived types).
+
+This is mainly for performance consideration, as virtual method table that is
+required for dynamic dispatch would penalize performance, and prohibits function
+inlining etc. Note that type variables cannot be used inside `virtual[...]`.
+
+Example:
+```py
+def bar2(x: list[virtual[Base]]) -> int:
+    sum = 0
+    for v in x:
+        sum += v.foo()
+    return sum
+```
+
+The syntax for casting virtual objects is `virtual(obj, T)`, which casts an
+object of type `T1/virtual[T1]` to `virtual[T]` where `T1 <: T` (T1 is a subtype
+of T).
+
+The compiler may be able to infer the type cast. In that case, the cast
+is not required if `obj` is already of type `virtual[T1]`, or the user can write
+the cast as `virtual(obj)` and the compiler would infer the type `T`
+automatically.
+
+Methods would be automatically overriden, the type signature including parameter
+names and order must be exactly the same.
+
+Defining a method which was marked as final in the super class would be
+considered as an error.
+
 ## Lifetime
 Probably need more discussions...