feat!: Innards of non-empty holes should check against hole type#931
feat!: Innards of non-empty holes should check against hole type#931
Conversation
|
This sounds like a good idea. Do you see any possible downsides? |
Other than time required to implement, no I don't. However, I have not thought about how this would interact with hole removal (either automatically via smartholes, or manually via an action). I would also not be totally surprised if some unexpected problems arise during implementation. |
|
Okay. Maybe let's wait and see how often this comes up as an issue when we start using the app with saturated constructors. |
…ds we should change this; we have not caught it before as we don't PBT progactions -- @georgefst: (how) will this interact with your typedefs-in-openapi work?
| -- I have modified the original Hazel mechanised metatheory | ||
| -- (https://github.com/hazelgrove/agda-popl17) and changed it to have this rule | ||
| -- (and a few other knock-on changes). | ||
| -- See https://github.com/brprice/hazel-experiments |
There was a problem hiding this comment.
Either this repo doesn't exist, or I don't have read permissions.
There was a problem hiding this comment.
FTR
- this comment no longer exists in the source code
- the repo has moved to https://github.com/brprice/hazel-metatheory
|
I don't understand this sentence in the OP:
|
|
I think this sounds like a good idea. It seems very likely that students will be spending a lot of time editing misfit expressions [1] , and whatever we can do to make that workflow less confusing, the better. Automatically-inserted annotations will probably not be very intuitive, especially if they're unlikely to occur in other situations. [1] n.b.: I'm adopting our new terminology here, misfit expression rather than what we previously called non-empty hole |
brprice
force-pushed
the
brprice/nehole-chk
branch
from
0388897 to
ddc0c75
Compare
brprice
force-pushed
the
brprice/nehole-chk
branch
from
ccd6444 to
1a9cece
Compare
brprice
changed the title
brprice
changed the title
brprice
force-pushed
the
brprice/nehole-chk
branch
from
1a9cece to
7bb6ab1
Compare
| , ConstructVar $ LocalVarRef "x" | ||
| , ConstructAnn | ||
| , Move Child1 | ||
| , ConstructCase | ||
| , Move (Branch cTrue) | ||
| , constructSaturatedCon cZero | ||
| ] | ||
| ( ann | ||
| ( lam "x" $ | ||
| hole $ | ||
| ann | ||
| ( case_ | ||
| (lvar "x") | ||
| [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] | ||
| ) | ||
| tEmptyHole | ||
| case_ | ||
| (lvar "x") | ||
| [branch cTrue [] (con0 cZero), branch cFalse [] emptyHole] | ||
| ) |
There was a problem hiding this comment.
Note how we no longer have to annotate this case inside the hole.
|
I'm happy with this decision, and thanks for the well-motivated discussion in one of the code comments in the 2nd commit. However, I'll leave the code review to @georgefst. |
brprice
force-pushed
the
brprice/letrec-typing
branch
2 times, most recently
from
7875e91 to
4009eeb
Compare
brprice
force-pushed
the
brprice/nehole-chk
branch
2 times, most recently
from
afe9a61 to
202dc88
Compare
brprice
force-pushed
the
brprice/let-rename-offer
branch
from
242534d to
e375e09
Compare
Previously the typing rule was
e ∈ S
-----------
{? e ?} ∈ ?
Now the rule is
? ∋ e
-----------
{? e ?} ∈ ?
BREAKING CHANGE: since this changes the behaviour of smartholes and the
`SetConFieldType` action, it will change the interpretation of program
logs. Thus it may break replaying logs stored from older versions of
primer (e.g. when using 'undo' on a program loaded from an old
database).
Signed-off-by: Ben Price <ben@hackworthltd.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
brprice
force-pushed
the
brprice/nehole-chk
branch
from
202dc88 to
50dccbf
Compare
3 participants
Currently they must synthesise some type (and we don't care what), but there is no particular reason for this that I can recall, other than following Hazel. I think it may be nicer UX if we change this.
In particular, with checkable saturated constructors we would then be able to write a constructor directly inside a hole, without having to annotate it. Even without that, we could write a lambda directly inside a hole (currently it would need an annotation):
{? λx.t[x] ?}would be valid, and synthesise a hole exactly when we have thatx : ? ⊢ ? ∋ t[x].Essentially, whenever we now write
{? t : ? ?}, we could drop the annotation. Whenever we currently have a more-specific annotation (currently this is only possible when a human explicitly writes it, I think), then we could still write it exactly the same as before (e.g.{? λx.t[x] : Nat -> Bool ?}would be fine exactly whenx : Nat ⊢ Bool ∋ t[x]).