-
Notifications
You must be signed in to change notification settings - Fork 35
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Type refinement in conditional expressions #25
Comments
(comments from @josefs copied fom #23) Type refinement would be a very powerful feature to have. But it's also non-trivial to implement and it's unclear to me how important it is. So I think the right way forward is to first try and get the gradualizer into a state where people can use it. Perhaps a version 1.0. Then we can more easily see what features people need and miss and then start to tackle them in the right order. I haven't spent very much time thinking about type refinement but if you want to dig into that subject I think that you should at the very least read Sums of Uncertainty: Refinements Go Gradual, a paper from the POPL conference last year. I haven't yet read the whole paper but I assume we will be able to borrow quite a lot from that paper. |
@gomoripeti, since you opened this ticket we've implemented type refinement. It doesn't handle the cases that you imagined though. Are you still keen on pursuing the kind of refinement that you outlined or should we let the machinery we have now suffice? |
The code for The remaining part for the first example above is to implement refinement based on the |
Related to issue josefs#25
Related to issue josefs#25
(tbh I don't remember what was my original main idea, it looks like it might have been arguing for the introduction of "intersection") anyway as you both describe some common aspects are already implemented. and @zuiderkwast you point out, a full solution with "blaming" is quite complicated. |
The existing function Please look at my new PR! ^ |
Related to issue josefs#25
(this ticket was split from #23 which also contain some of the early comments)
let's see the following correct function with spec
AI
inExrp2
must be the subtype ofnumber() :: integer() | float()
as the first argument of+
AI
inExrp2
isatom() | integer()
based on the spec which is not a subtype ofinteger() | float()
How could Gradualizer realise that
Expr2
is only executed when type ofAI
isinteger()
?if NOT is_atom(AI) => typeof(AI) == (atom() | integer()) & (not atom()) == integer()
- however this is not always possibleLet's see a more generic example
In this case what the type checking could do is realise that
body(A)
is only executed in a subset of cases therefor type ofA
inbody(A)
is just a subset or subtype ofinput()
. In caseinput() & required() == none()
(the intersection of the two types is empty) then we can say thatbody(A)
will always fail, but otherwise we cannot know (and have to leave type checking at runtime). This method requires to be able to calculate the intersection of two types.What is the right way to handle these kind of constructs? (
if
,case
, multiple function clause)The text was updated successfully, but these errors were encountered: