From c84d29f09b9ec3191b38f9cfd7c9493e7fa634a2 Mon Sep 17 00:00:00 2001 From: pca006132 Date: Tue, 19 Jan 2021 15:42:46 +0800 Subject: [PATCH] added explanation for substitution --- toy-impl/README.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/toy-impl/README.md b/toy-impl/README.md index 5f10826..71af54a 100644 --- a/toy-impl/README.md +++ b/toy-impl/README.md @@ -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