order-of-evaluation props

[bennn]

Use props from checking a function to check its first argument,
use props from checking the first argument to check the second,
and so on.

Makes things like this type check: (lambda: ((x : (Un Symbol Natural))) (+ (assert x integer?) x))

---

TODO:

• add test where some arguments are unreachable
• accumulate props in tc-app-main on L91 L97 L98
• add test to show its a good idea to accumulate props even when the arguments have expected types
• stop extracting props from argument twice
• finish the RFC
• measure performance (using the pnwamk/tr-performance repo)
• see about accumulating props in the special tc-app cases (for values, vector-ref, etc.)

[pnwamk]

Would check-in-order/single-value (or something similar) be a clearer name? map-single-value seems too generic to me.

[bennn]

Renamed to map-single-value/unconditional-prop because:

• map single-value is what we were doing before
• map implies left-to-right order
• /unconditional-prop explains the 2nd argument
• and the prop that gets accumulated is the "unconditional prop" from the arguments

I'm happy with this name, but not opposed to changing it

[pnwamk]

I've thought more about this and looked at the code more; here are a few comments:

1. If this is a good change and the right thing to do (and I think it is) we should be doing it any time we can, every time we check function arguments. In particular we should also be accumulating the propositions here, here., here, etc, i.e. we should do it for both standard and dependent functions whenever there could be propositions that help the remaining arguments type check.

2. Does it make sense to also do this on arguments were we have calculated an expected type (i.e. here)? I can't remember... is there a way we can have an expected type but still extract meaningful propositions from an expression? If so we should remember those props as well.

3. With these changes, we're now extracting the unconditional propositions from argument type results twice (see here for the other time). I think we should probably just do this once (i.e. while we're checking the argument types in order from left-to-right as you have done here) and then we should pass that prop along (maybe as an additional argument to tc/funapp) so it can be propagated/used where needed. In other words, the logic from the code I linked above that is also extracting unconditional argument propositions should appear in whatever we call map-single-value/unconditional-prop.

4. I think map as a part of the name is a misnomer because it is accumulating something other than a list along the way (the unconditional props) that it should be returning in addition to the list of type results (i.e. we should pass along that accumulated logical info since it is used/needed elsewhere).

5. One other misc note: this behavior reminds me of tc-body/check which also accumulates unconditional info as It checks expressions guaranteed to be evaluated in order. This observation may not be useful... but I figured I'd mention it.

[bennn]

2. yes
4. "map" alone would be bad to me, but I like the current "map with prop". (I'm happy to take suggestions, but I'm personally not going to think about new names)

[pnwamk]

I wonder if with-lexical-env+props is right here and not with-lexical-env+props-simple? The latter seems to do a little less work... TBH I'm not sure which to favor here.

[bennn]

I used with-lexical-env+props because that's what tc-body/check uses for function bodies.

[pnwamk]

I think we need more tests. What about

1. Tests where the combinations of the first several arguments then allows the final argument(s) to type check?
2. Tests were at some point the environment becomes absurd (and thus the final arguments are dead code and don't need to be type checked)?

Maybe there's other's that would be useful.

[bennn]

update: testing has led to some internal typechecker errors wrt the optimizer, will fix

[pnwamk]

Questions:

1. Are there any downsides to doing this? The only possible conflict I can think of is that dependent function types allow arguments to depend on each other in any order (not in a fixed left to right order) and you may want to check those in that particular order... I'm not sure if/how these features would interact. Maybe we should add a check that the function is not a dependent function to be safe?

2. Does this affect performance at all? It seems like it probably wouldn't for most programs (most arguments don't have interesting propositions, right?) but it would be nice to double check w/ some numbers just so we know.

[pnwamk]

I like this PR -- I'm a little nervous because we could clearly never "undo" it so we need to make sure we feel like we've considered all the possible repercussions.

[samth]

I think this is something that would benefit from writing down the RFC as part of this process.

[bennn]

@pnwamk re 1. I don't think these changes affect dependent functions; looks like tc-app-main.rkt handles those (DepFun?) in a separate branch. BUT I think it would be safe to apply "this change" to applications of dependent functions as long as those still evaluate their arguments left-to-right

[pnwamk]

I think it might be useful to have the RFC be it's own pull request. That way we can agree on the idea itself separate from the work to implement, merge the RFC when it's ready, and then we can focus on working together to get this PR done and in sync with the RFC.