added explanation for substitution

This commit is contained in:
pca006132 2021-01-19 15:42:46 +08:00
parent 09234a416b
commit c84d29f09b

View File

@ -18,7 +18,7 @@ for simplicity reasons:
* AugAssign, `a += b` etc.
* `with`, `try except`, etc.
* const indexing with tuple.
* method override check modulo variable renaming.
* method override check modulo type variable renaming.
* more complicated type guard
## Running Example
@ -122,6 +122,10 @@ conditions:
allowed.
### Substitution
> Actually this scheme is to simplify type inference... as we think that
> standard type inference which solves equations is a bit hard to reason about,
> and hard to add subtyping into it.
The crucial constraint and assumption in our system is that, every
(sub-)expressions must have their types fully determined, and cannot depend on
statements/expressions after them. Hence, in a function call, every arguments