Commit 7636ad0d authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added remarks

parent a2dadc10
......@@ -98,7 +98,8 @@ The thesis is available at https://pnwamk.github.io/docs/dissertation.pdf
**ANSWER:**
A. Kent's approach is based on control flow. As soon as a variable is defined, it computes and remember under which constraints this variable can be in True or ~True. Typecases can only be done on variables, and the former information is used to refine the context of the then and else branches. A new idea of A. Kent's thesis compared to previous works on occurence typing is the use of semantic types to store these constraints, and the use of an application inversion function to compute them. We also use these ideas in our paper.
A. Kent's approach is based on control flow. As soon as a variable is defined, it computes and remember under which constraints this variable can be in True or ~True (Beppe: isn it rather False and ¬False?). Typecases can only be done on variables (Beppe: really???), and the former information is used to refine the context of the then and else branches. A new idea of A. Kent's thesis compared to previous works on occurence typing is the use of semantic types to store these constraints, and the use of an application inversion function to compute them. We also use these ideas in our paper.
(Beppe: where do we use it other than for False and ¬False?)
However, our approach is not based on control flow. We do not store any additional information about variables except their types. Instead, our typecases can be applied to arbitrary expressions e and only at this moment we perform a *backward analysis* to refine the type of the subexpressions composing e.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment