feat: display and edit kinds on foralls #1120

brprice · 2023-08-17T23:04:29Z

Notes for reviewers: Sorry the PR is so large; I think most of it is fairly mechanical refactors and I have tried to split those into separate commits where I can

primer/src/Primer/TypeDef.hs

georgefst

Great stuff. Thank you for taking on this work!

georgefst · 2023-09-11T12:08:11Z

primer/test/Tests/Zipper.hs

@@ -25,7 +26,7 @@ tasty_focus_unfocus_roundtrip = property $ do
 tasty_focusOn_unfocus_roundtrip :: Property
 tasty_focusOn_unfocus_roundtrip = property $ do
  e <- forAll $ evalExprGen 0 genExpr
-  i <- forAll $ Gen.element $ idsIn e
+  i <- forAll $ Gen.element $ e ^.. exprIDs


It seems a stretch to call this a refactor: given that (^.. exprIDs) has different behaviour to idsIn and thus the test is more general.

primer-api/src/Primer/API.hs

georgefst · 2023-09-11T13:54:25Z

primer/src/Primer/Action/Available.hs

@@ -167,7 +167,8 @@ data NoInputAction
  | DeleteTypeParam
  | MakeKType
  | MakeKFun
-  | DeleteKind
+  | -- TODO: RaiseKind?


Yes, we probably should have a "raise kind" action. Though I don't mind whether that's in a separate PR.

See also #1141 (comment) and #66 (comment).

This is now tracked in #1145

georgefst · 2023-09-11T13:55:31Z

primer/src/Primer/Typecheck.hs

+        -- TODO/REVIEW: when testing editable-forall-kinds, I noticed that we would not elide the hole in
+        --   foo : ∀a:*.? ; foo = {? ? : ∀a:*.? ?}
+        -- but this is odd -- the annotations are identical (so not acting as a typechange)!
+        -- (also, note that we keep hole-wrapped-holey-anns around because of the below even when we would accept the non-wrapped version (indeed, have an action that will do that!)


This is odd. Do you have any inkling as to why it occurs?

Yes. This is actually #7. The current design is

When synthesising "never elide holes", i.e. do not automatically do {? e ?} ~> e when we have no information about the context. NB: if we did elide, it could change the synthesised type and force new holes to appear elsewhere in the program.

When checking T ∋ {? e ?} we attempt to elide the hole if that would be type-correct by the transformations

if checking nested holes T ∋ {? {? e ?} ?}, drop one layer and recurse T ∋ {? e ?}

if have an annotation in a hole (this is the case referred to in this comment) T ∋ {? s : S ?}, we

drop a hole-and-trivial-annotation, if it is still type-correct {? s : ? ?} changes to s, if we have T ∋ s

never touch holes-and-incomplete-annotations (this is our current example), i.e. if there is a type hole in the annotation S, as (quoting Typecheck.hs)

Don't want to, e.g., remove {? λx.x : ? ?} to get λx.x : ? Since holey annotations behave like non-empty holes, we will not elide non-empty holes if they have a holey annotation. (This is needed for idempotency, since we return non-empty holes with holey-annotated contents in the case a construction cannot typecheck, e.g. Bool ∋ λx.t returns {? λx.t : ? ?}

otherwise fall through to the "have a hole, and don't care about the contents" case

if none of the above are true, we have a hole and don't care about the contents, in which case we elide the hole leaving e as long as that is type-correct

(NB: above, where I say "elide...as long as that is type correct" and similar, by "type correct" I actually mean "smart holes accepts the term and does not create a hole at top level", i.e. it could result in "pushing down the hole")

(If you think this seems somewhat convoluted, then I agree: this logic should be revisited!)

Can you add a comment in the code here with a link to the parent post, and also a link to #7, please?

Can you add a comment in the code here with a link to the parent post, and also a link to #7, please?

Will do, but in a separate PR since it is orthogonal to the current changes.

Can you add a comment in the code here with a link to the parent post, and also a link to #7, please?

Will do, but in a separate PR since it is orthogonal to the current changes.

See #1147

primer/src/Primer/TypeDef.hs

Signed-off-by: Ben Price <[email protected]>

Before this commit, it used `idsIn` which only gave IDs of expression nodes, and not type nodes within type annotations or applications. Thus these tests are now slightly stronger. Signed-off-by: Ben Price <[email protected]>

Signed-off-by: Ben Price <[email protected]>

This is usually instantiated to `()`, matching the previous hardcoded choice. There are intended to be no functional changes in this commit, it is simply setup for adding IDs to kinds in foralls (and thus to enable actions in those positions). (Note that there are a couple of TODOs added in comments which will be addressed in a subsequent commit.) Signed-off-by: Ben Price <[email protected]>

This requires reworking `forgetTypeDefMetadata` and `generateTypeDefIDs`, where we can use generic optics instead of the current traversals. We do this in preparation for adding metadata to kinds in types. This will include kinds within fields of constructors. When that happens, the same type parameter will control the metadata in two separate fields of ASTTypeDef, meaning the old type-changing lens-style definitions would become very awkward. Signed-off-by: Ben Price <[email protected]>

We now have a general "nested zipper" definition, which will be used to focus on kinds-inside-types{,-inside-exprs} later. Signed-off-by: Ben Price <[email protected]>

We define a helper datatype, rather than nesting `Either`s. This gives much better names of constructors, and makes it easier to extend when we shortly enable focusing on kinds. Signed-off-by: Ben Price <[email protected]>

We add a `Void` field to such selections so that it is clear we don't yet create them, and it is easy to stub out some codepaths that do not yet make sense (mostly due to kinds not having IDs yet). Note that `findTypeOrKind` (and friends) only work for the kind parameter being `()`, and consequently do not actually focus on kinds (they have no IDs). Signed-off-by: Ben Price <[email protected]>

This will be reused shortly, when we enable actions on kinds in foralls. Signed-off-by: Ben Price <[email protected]>

This is setup for kinds being selectable. (Currently we actually return a second summand of `(KindTZ, Void)`, since we never actually focus on kinds. This `Void` will be dropped shortly.) Signed-off-by: Ben Price <[email protected]>

We also remove `findType` usage from API, in favor of `findTypeOrKind` (currently these are equivalent, but the latter more clearly expresses the plan to enable kinds-in-foralls to be selectable. Note that the refactoring is slightly stricter with throwing a `NodeIDNotFound` error. Signed-off-by: Ben Price <[email protected]>

This is a trivial-but-invasive refactoring to set up for adding IDs to kinds-in-foralls. The new definitions khole', ktype', kfun' are temporary and will be collapsed into their non-primed versions when we have added IDs. Signed-off-by: Ben Price <[email protected]>

This removes our usage of `Void`, and fills out those codepaths that were stubbed out due to lacking ids. Note that this commit introduces some TODOs which will be addressed in a subsequent commit. Signed-off-by: Ben Price <[email protected]>

Signed-off-by: Ben Price <[email protected]>

Now that we have unique IDs on kinds, this is possible whilst giving unique `nodeId`s in the api's result. BREAKING CHANGE: this affects our API. Our advertised OpenAPI interface remains the same, but the data we return will differ. Signed-off-by: Ben Price <[email protected]>

This does not change our API, we simply accept some actions in positions that we previously did not. Signed-off-by: Ben Price <[email protected]>

We replace the last usage and delete the function. There is no need to keep this footgun around (it is too easy to forget that it doesn't select kinds). Signed-off-by: Ben Price <[email protected]>

Signed-off-by: Ben Price <[email protected]>

This is consistent with other actions. BREAKING CHANGE: this changes the richly-typed API Signed-off-by: Ben Price <[email protected]>

brprice linked an issue Aug 17, 2023 that may be closed by this pull request

FR: Provide API for displaying and editing kinds on foralls #1098

Closed

brprice mentioned this pull request Sep 4, 2023

fix: tcWholeProg updates metadata of ADT parameter selections #1129

Merged

brprice force-pushed the brprice/forall-kind-edit branch 2 times, most recently from 985a2cc to 7cfe2e4 Compare September 7, 2023 14:06

brprice changed the title ~~WIP: display and edit kinds on foralls~~ feat: display and edit kinds on foralls Sep 7, 2023

brprice commented Sep 7, 2023

View reviewed changes

primer/src/Primer/TypeDef.hs Outdated Show resolved Hide resolved

brprice commented Sep 7, 2023

View reviewed changes

primer/src/Primer/TypeDef.hs Outdated Show resolved Hide resolved

brprice marked this pull request as ready for review September 7, 2023 14:13

brprice requested a review from a team September 7, 2023 14:13

georgefst approved these changes Sep 11, 2023

View reviewed changes

georgefst mentioned this pull request Sep 12, 2023

Duplicate typedef action #1141

Open

brprice mentioned this pull request Sep 18, 2023

style: bump fourmolu -> 0.13.1.0 #1099

Closed

brprice added 4 commits September 18, 2023 18:31

docs: clarify comment on moveType

3b135d3

Signed-off-by: Ben Price <[email protected]>

docs: explicitly say regenerateExprIDs goes into types

7d74d5e

Signed-off-by: Ben Price <[email protected]>

refactor: Gen uses TypeG consistently

583031e

Signed-off-by: Ben Price <[email protected]>

refactor: Primer.Module uses generateTypeDefIDs

c51d1c6

Signed-off-by: Ben Price <[email protected]>

brprice force-pushed the brprice/forall-kind-edit branch from 7cfe2e4 to b0f5a68 Compare September 18, 2023 17:32

brprice added 13 commits September 19, 2023 11:49

test: focusOn tests use exprIDs

c1ec1e1

Before this commit, it used `idsIn` which only gave IDs of expression nodes, and not type nodes within type annotations or applications. Thus these tests are now slightly stronger. Signed-off-by: Ben Price <[email protected]>

refactor: Zipper/Type.hs uses TypeZip' synonym more

053e07d

Signed-off-by: Ben Price <[email protected]>

refactor: use Loc rather than Either ExprZ TypeZ

3a76080

Signed-off-by: Ben Price <[email protected]>

refactor: generalise TypeZ machinery

efb3afc

We now have a general "nested zipper" definition, which will be used to focus on kinds-inside-types{,-inside-exprs} later. Signed-off-by: Ben Price <[email protected]>

refactor: copyPasteBody to avoid nested Either

13082f7

We define a helper datatype, rather than nesting `Either`s. This gives much better names of constructors, and makes it easier to extend when we shortly enable focusing on kinds. Signed-off-by: Ben Price <[email protected]>

refactor: abstract out Action.Available:forKind

010b4e6

This will be reused shortly, when we enable actions on kinds in foralls. Signed-off-by: Ben Price <[email protected]>

feat: add kind ids inside types

e9ef32f

This removes our usage of `Void`, and fills out those codepaths that were stubbed out due to lacking ids. Note that this commit introduces some TODOs which will be addressed in a subsequent commit. Signed-off-by: Ben Price <[email protected]>

brprice added 7 commits September 19, 2023 11:52

refactor: replace temporary khole' with khole (and for kfun, ktype)

f6f5bf1

Signed-off-by: Ben Price <[email protected]>

feat: offer & accept kind actions in foralls

07c9ffc

This does not change our API, we simply accept some actions in positions that we previously did not. Signed-off-by: Ben Price <[email protected]>

refactor: remove findType in favor of findTypeOrKind

a521394

We replace the last usage and delete the function. There is no need to keep this footgun around (it is too easy to forget that it doesn't select kinds). Signed-off-by: Ben Price <[email protected]>

refactor: ParamKindAction uses existing machinery

bbca25a

Signed-off-by: Ben Price <[email protected]>

refactor: ParamKindAction sets the selection

6a30798

Signed-off-by: Ben Price <[email protected]>

refactor!: ParamKindAction does not take ID, use SetCursor instead

36ed018

This is consistent with other actions. BREAKING CHANGE: this changes the richly-typed API Signed-off-by: Ben Price <[email protected]>

brprice mentioned this pull request Sep 19, 2023

More actions on kinds #1145

Open

brprice force-pushed the brprice/forall-kind-edit branch from a537e6e to 36ed018 Compare September 19, 2023 12:02

brprice mentioned this pull request Sep 19, 2023

chore(hole/annotation elision): link to github bug tracker #1147

Merged

brprice added this pull request to the merge queue Sep 19, 2023

Merged via the queue into main with commit 2bf2349 Sep 19, 2023
70 checks passed

brprice deleted the brprice/forall-kind-edit branch September 19, 2023 14:09

georgefst mentioned this pull request Nov 8, 2023

Add IDs to kinds, so that we can render them as trees in frontend #593

Closed

brprice mentioned this pull request Nov 8, 2023

Support polymorphism #122

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: display and edit kinds on foralls #1120

feat: display and edit kinds on foralls #1120

brprice commented Aug 17, 2023 •

edited

Loading

georgefst left a comment

georgefst Sep 11, 2023

georgefst Sep 11, 2023 •

edited

Loading

georgefst Sep 12, 2023 •

edited

Loading

brprice Sep 19, 2023

georgefst Sep 11, 2023 •

edited

Loading

brprice Sep 19, 2023 •

edited

Loading

dhess Sep 19, 2023

brprice Sep 19, 2023

brprice Sep 19, 2023

feat: display and edit kinds on foralls #1120

feat: display and edit kinds on foralls #1120

Conversation

brprice commented Aug 17, 2023 • edited Loading

georgefst left a comment

Choose a reason for hiding this comment

georgefst Sep 11, 2023

Choose a reason for hiding this comment

georgefst Sep 11, 2023 • edited Loading

Choose a reason for hiding this comment

georgefst Sep 12, 2023 • edited Loading

Choose a reason for hiding this comment

brprice Sep 19, 2023

Choose a reason for hiding this comment

georgefst Sep 11, 2023 • edited Loading

Choose a reason for hiding this comment

brprice Sep 19, 2023 • edited Loading

Choose a reason for hiding this comment

dhess Sep 19, 2023

Choose a reason for hiding this comment

brprice Sep 19, 2023

Choose a reason for hiding this comment

brprice Sep 19, 2023

Choose a reason for hiding this comment

brprice commented Aug 17, 2023 •

edited

Loading

georgefst Sep 11, 2023 •

edited

Loading

georgefst Sep 12, 2023 •

edited

Loading

georgefst Sep 11, 2023 •

edited

Loading

brprice Sep 19, 2023 •

edited

Loading