... | @@ -55,12 +55,9 @@ Those with an MR actually have code. |
... | @@ -55,12 +55,9 @@ Those with an MR actually have code. |
|
- Paper
|
|
- Paper
|
|
- Type-set checking function
|
|
- Type-set checking function
|
|
- Commit to syntax for Delta
|
|
- Commit to syntax for Delta
|
|
- à la Refinement type? But then we aren't in DNF (i.e. union only on the top-level).
|
|
- Like in the presentation: Have a "value set" that is a refinement of the type of the value vector, Delta ::= { Gamma | Constraints }
|
|
- But if we have the "\Theta = union of \theta" idea, then how does \theta look? -> Just a list of constraints, of course (which are `all` true at the same time). Then \oplus just lifts adding a constraint over all the thetas.
|
|
- Gamma binds only match vars. This implies that Constraint trees have the notion of scoping, like list comprehensions
|
|
- How do we call the empty \theta? \epsilon (neutral element of constraint list) seems misleading compared to \emptyset (neutral element of union).
|
|
|
|
- What are FV (the things we bind in Gamma) of Theta? Only the match variables or also let-bound stuff? We don't have any binding constructs in our representation of theta, so probably the latter? That is quite weird, because Gamma will bind stuff from other closed lexical scopes. See `h` in #17378, where in the second equation, Gamma would have to bind `y` although it's only a thing in the first equation.
|
|
|
|
- Having the condensed form `Redundant | Inaccessible | Reachable` is inconsequential, because then we need to concern `pmcheck` with inhabitation testing (\cup_C and \cup_D, for example), when in the rest of the checking function we don't test for inhabitants eagerly. I think we should commit to either early or late inhabitation testing, not this in-between stuff. Also we need the Covered set for long distance info anyway. But where should we attach Gamma then? To the ClauseResult triple? To the incoming uncovered set? Both need it. But for `pmcheck` we can just take Gamma as a parameter, so we should be fine. But also Gamma is specific to each theta. Yuck!!!
|
|
- Having the condensed form `Redundant | Inaccessible | Reachable` is inconsequential, because then we need to concern `pmcheck` with inhabitation testing (\cup_C and \cup_D, for example), when in the rest of the checking function we don't test for inhabitants eagerly. I think we should commit to either early or late inhabitation testing, not this in-between stuff. Also we need the Covered set for long distance info anyway. But where should we attach Gamma then? To the ClauseResult triple? To the incoming uncovered set? Both need it. But for `pmcheck` we can just take Gamma as a parameter, so we should be fine. But also Gamma is specific to each theta. Yuck!!!
|
|
- So: Gamma must be part of theta/we should name the list of constraints delta and have `\theta ::= \Gamma \vdash \Delta`.
|
|
|
|
- Think about how to fix "regression" in T11822
|
|
- Think about how to fix "regression" in T11822
|
|
- SG bets a smart `CoreMap` would do
|
|
- SG bets a smart `CoreMap` would do
|
|
- Maybe pattern-match check typed TH quotations? SG doesn't think this is a good idea, because they might not even end up in that form in spliced code.
|
|
- Maybe pattern-match check typed TH quotations? SG doesn't think this is a good idea, because they might not even end up in that form in spliced code.
|
... | | ... | |