Commit e0458e4b authored by Mickael Laurent's avatar Mickael Laurent
Browse files

comparison with a kent

parent 10af280e
......@@ -97,7 +97,20 @@ The thesis is available at https://pnwamk.github.io/docs/dissertation.pdf
>> Mickael: premier draft et comparison avec worra
**ANSWER:**
The application inversion function from Kent's thesis is supposed to compute exactly the same type as our *worra* operator. However, we believe that there is a mistake (typo?) in its algorithmic definition (p108 fig 5.2).
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 branchs. 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 this idea in our paper.
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.
One advantage of our method is that we can test any type, whether A. Kent's system can only test if an expression is True or not (because it is the only information that has been stored). Although some built-in functions such as `is_int` can be introduced in order to test whether a variable has the type int or not, the system will not be able to refine subexpressions composing x: if x is defined as `f y`, no refinement can be made about `f` or `y` when testing if `is_int x` is True or not.
One drawback of our method, however, is the lack of control flow analysis. In particular, it forces us to inline the let bindings of an expression before typing it.
>> Should we put some of this answer in the paper?
*Concerning the application inversion function*
The application inversion function from A. Kent's thesis is supposed to compute exactly the same type as our *worra* operator. However, we believe that there is a mistake (typo?) in its algorithmic definition (p108 fig 5.2).
Indeed, the formula of \tau_a seems incorrect: we think the first union should be an intersection.
Here is an example for which the current definition seems unsound:
......@@ -109,7 +122,7 @@ inv (((True->False) /\ (False->True)) \/ ((True->True) /\ (False->False)), True)
However, a function with a type `((True->False) /\ (False->True)) \/ ((True->True) /\ (False->False))` could definitively give a result in `True`. The correct result should be `Bool`.
If we change this union into an intersection, then Kent's formula becomes equivalent to our algorithmic definition of *worra* (p13) with a simple application of De Morgan.
If we change this union into an intersection, it becomes equivalent to our algorithmic definition of *worra* (p13) with a simple application of De Morgan.
**(END OF ANSWER)**
......
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