Provide APIs for viewing and editing kinds of type parameters #1095

georgefst · 2023-07-13T14:29:30Z

We can now finally construct any typedef supported by the backend.

There are a number of things which I intend to punt to #1098. This PR is already big enough.

georgefst · 2023-07-26T19:10:45Z

primer/src/Primer/Action.hs

@@ -1290,7 +1309,7 @@ toProgActionInput def0 sel0 opt0 = \case
    opt <- optNoCxt
    sel <- typeSel
    index <- length . astTypeDefParameters <$> typeDef -- for now, we always add on to the end
-    pure [AddTypeParam sel.def index opt C.KType]
+    pure [AddTypeParam sel.def index opt $ C.KHole ()]


Do we actually want this last commit? Starting with a hole seems like the obvious thing to do now that we can actually construct kinds, and it's consistent with terms and types, but it may be more annoying to use.

There's a wider conversation to be had about the extent to which we want to hide kinds from beginners. If we do, this is potentially a step in the wrong direction.

Good question. I'm not sure.

There is one sense in which kinds are different to terms/types: since they are so simple, there is a canonical thing to put in the leaves of a non-holey tree: a KType. Since our kind actions will all push the current kind down (i.e. k ~> k -> ?), one will always end up filling in this hole with a KType. (This is not true in types/terms, since there are more options for leaves.).

Indeed, if we are going the direction of "leave as KType because of the above justification", I would perhaps argue that inserting an arrow should not create k -> ?, but k -> KType.

@brprice's proposal sounds good to me.

Interesting. One could argue that we should go a step further and not allow constructing KHole at all. In practice I suppose this would mean, in addition to reverting the change above, replacing the "delete kind" action with a "raise" action, offered only on KFun nodes.

Now that I think about it, the purpose of KHole is somewhat unclear, given that we have such a simple kind system. Is it just used to give a kind to TEmptyHole? And would it be reasonable to just say that that has the kind KType instead?

Interesting. One could argue that we should go a step further and not allow constructing KHole at all. In practice I suppose this would mean, in addition to reverting the change above, replacing the "delete kind" action with a "raise" action, offered only on KFun nodes.

Potentially, but see below about why KHole exists (and is not easily going away). Thus if we forbade constructing KHole at all, it would be somewhat inconsistent.

Being able to give hole kinds does enable students to write more "programs" (i.e. things the system accepts, but are obvious nonsense). This may be good or bad depending on whether this is the sort of confusion/freedom that is good for learning(!), and on whether these states actually have utility as intermediate states in interactive use (I have not got any intuition on this as yet). In particular, one could write something like data T (p : ?) = C (p p) p, where p is being used at multiple kinds: (roughly speaking) k -> *, k and * (for some unknown k). It is not possible to fill in the KHole here to get a valid complete program. (As an aside, it is possible to make sense of this in a richer type system, by giving p a polymorphic kind; e.g. ghc will accept data D (p :: forall k . k) = C p (p p). I don't know whether things of this ilk are practically useful.)

Now that I think about it, the purpose of KHole is somewhat unclear, given that we have such a simple kind system. Is it just used to give a kind to TEmptyHole? And would it be reasonable to just say that that has the kind KType instead?

It is indeed used to kind TEmptyHole (iirc). In the past we did say TEmptyHole has kind KType, but there was an issue with that, and I changed it https://github.com/hackworthltd/vonnegut/commit/0f291a3db0904e1d05b1af60201358565089ac9a . In particular, we really want to be able to create type applications via the sequence (e.g.) ? ; ? ? ; List ? ; List Bool, but the intermediate type ? ? is checked by synthesising a kind for the first hole, ensuring it is (consistent with) an arrow kind and the second hole matches the domain -- this would fail if we gave the kind KType. (This is not the only way to solve this problem, but is the one we currently use, and would need to revisit this if we wanted to give the kind KType to type holes.)

Being able to give hole kinds does enable students to write more "programs" (i.e. things the system accepts, but are obvious nonsense).

This is interesting, and I'd never really considered that our type holes work in this way. And it is unique to type-level holes, because of the lack of kind-polymorphism: we allow terms like λx. x x (which GHC doesn't accept without further annotations), but this can be completed with appropriate annotations and type applications.

Anyway, the point about kindchecking ? ? (EDIT: also made at #108 (comment)) is a good one (although, just to put it out there, it would go away if we were able to treat type constructors as always-saturated, like we do for value constructors). So
I'll implement your original proposal.

georgefst · 2023-07-26T19:12:43Z

primer-api/src/Primer/API.hs

-          maybe (throw' $ ParamNotFound p) (pure . Kind . viewTreeKind . snd) $
-            find ((== p) . fst) (astTypeDefParameters def)
+          maybe (throw' $ ParamNotFound p.param) (pure . Kind . viewTreeKind . snd) $
+            find ((== p.param) . fst) (astTypeDefParameters def)


This means we also display the whole kind when a node in the kind is selected. This is a bit weird, but I don't really know what else we could do - just say "kind"?

I'm not a fan of the current behaviour. I think it would be better to (as you suggest) just say "kind".

It would be easy enough to implement, changing data TypeOrKind = Type Tree | Kind Tree to data TypeOrKind = Type Tree | Kind Tree | SortKind (naming?). But I don't know how we would want to communicate this last case in our primer-app UI.

@dhess Any thoughts?

For the record:

ghci> :k * * :: *

But I think mimicking this would be less technically correct for Primer (in modern GHC Haskell, kinds really are just types).

I think I understand the question, but let's make sure. Is this about what type (aka "kind") to display when a kind is, say, * -> * -> *, and the student selects a non-root node in that tree?

Prior to this PR, we have a function Selection -> (Type | Kind). When any value-level node is selected it returns its type, and when any type-level node is selected we return its kind. The question is essentially: now that a selection can be of a kind-level node, what should be returned in that case?

(which I think is almost what you were saying, except that it includes root nodes)

Let's discuss in the upcoming developer meeting. (This item is now in the agenda.)

georgefst · 2023-07-26T21:57:40Z

primer/src/Primer/App.hs

                                    }
                            }
                  }
          )
+  ParamKindAction tyName paramName id actions -> editModuleOfCrossType (Just tyName) prog $ \(mod, mods) defName def -> do


This commit is, as mentioned in the commit message, a little bit of a hack, but not one that I'm concerned about merging, since it will be made more robust as part of #1098. The current approach is not ideal since we traverse both branches even though only one will have a matching ID, and we don't fail if the ID isn't found anywhere. See "type edits currently only allowed in typedefs" in applyAction': the main logic should in principle be implemented there, but can't be until Loc (part of our zipper interface) is generalised to account for kinds.

We also end up performing a full typechecking pass (checkEverything) for now because manually fixing up typecaches, as we do with many of the other typedef actions, would be more difficult to implement. Another option would be to further restrict the rules for when the action is offered, such that not only can the type not be in use, but also the parameter could not be in use within the body of any of the type's constructors' fields.

The current approach is not ideal since we traverse both branches even though only one will have a matching ID, and we don't fail if the ID isn't found anywhere

Do you think it is worth fixing this in this PR? I think it would be somewhat easy to do, but perhaps not worth it if you expect to revisit Loc soon.
Three ways spring to mind, all roughly implementing a modifyKindNode :: ID -> Kind -> (Kind -> Kind) -> Either Error Kind (or some variety of focusKind) function (where error could be "id not found" or "multiple id"):

just do it in the "findNode" style -- we may already have the ability to use a generic uniplate zipper on things which HasID to find a particular node

since kinds are simple, we could use some uniplate magic: something like contexts to get a focus on each node, then filter this by ID, then do the transform

some small applicative-state hack on this current code where we work not in the current monad m, but in something like StateT Int m (or maybe AccumT or WriterT may be better) where every time the modifyKind actually runs the function, it also emits a +1. We then check that we counted to exactly 1 (i.e. did exactly one edit). (It may be nicer to work in the "0-1-many" monoid, rather than the integers, as that more clearly expresses what we care about).

We also end up performing a full typechecking pass

This seems fine to me (at least, it is consistent with other actions)

I hadn't considered using uniplate. That seems like a good idea. But I'd rather wait until #1098 anyway. I'm sure we'll get to that very soon.

georgefst · 2023-07-26T22:02:10Z

primer/src/Primer/Action/Available.hs

+        else case k of
+          KHole _ -> Nothing
+          KType _ -> Nothing
+          KFun _ k1 k2 -> findKind i k1 <|> findKind i k2


This is another thing which can be simplified once we have zippers etc. for kinds.

georgefst · 2023-07-26T22:02:48Z

primer/test/Tests/Action/Available.hs

+                                    let allKindIDs = \case
+                                          KHole m -> [getID m]
+                                          KType m -> [getID m]
+                                          KFun m k1 k2 -> [getID m] <> allKindIDs k1 <> allKindIDs k2


This is another thing which can be simplified once we have zippers etc. for kinds.

georgefst · 2023-07-26T22:03:06Z

primer/src/Primer/App/Base.hs

@@ -70,7 +72,7 @@ data NodeType = BodyNode | SigNode
 -- | Describes which element of a (type or term) definition the student has selected.
 -- We have the following invariant: when this contains a `NodeSelection` with @nodeType = SigNode@,
 -- or any `TypeDefConsFieldSelection`, then they will always have @meta = Right _@.
-type Selection = Selection' (Either ExprMeta TypeMeta)
+type Selection = Selection' (Either ExprMeta (Either TypeMeta KindMeta))


This nested Either is maybe a bit ugly, but it's still in some ways simpler than defining a new type, whilst still being fairly self-explanatory.

dhess · 2023-07-27T08:27:13Z

Thanks, this was obviously a lot of work.

For posterity, can you provide here in the comments an example of a program/typedef that this PR allows us to create using the frontend API that we could not previously? (e.g., we can write Fix now, yes?) And can you also provide an example of a program that we still cannot write and will need #1098 for?

georgefst · 2023-07-27T13:42:12Z

Sure. We can now construct types like Fix or MaybeT but we're limited in being able to use them since all foralls implicitly quantify over variables with the kind "type". For example, we can't remove the mismatch here:

brprice · 2023-07-31T12:46:57Z

primer/src/Primer/Core/Type.hs

-  | TForall a TyVarName Kind (Type' a)
+  | TForall a TyVarName (Kind' ()) (Type' a)


For clarity: we intentionally don't put metadata on the kind here as is out of scope for this PR. See FR #1098. Here we are only interested in type parameters, and not foralls

Since I already need to rebase, I'll add this to the commit message when doing so.

brprice · 2023-07-31T12:53:16Z

primer/src/Primer/Module.hs

+primitiveModule :: MonadFresh ID m => m Module
+primitiveModule = do
+  allPrimTypeDefs' <- traverse (traverseOf (#primTypeDefParameters % traversed % _2) generateKindIDs) allPrimTypeDefs
+  -- allPrimTypeDefs' <- traverse _ allPrimTypeDefs
+  -- boolDef' <- traverseOf _typedefFields generateTypeIDs $ TypeDefAST boolDef


Did you mean to commit these comments?

No, thanks, will remove.

brprice · 2023-07-31T13:15:20Z

primer/src/Primer/Action.hs

+  ConstructKType -> const $ throwError $ CustomFailure ConstructKType "type edits currently only allowed in typedefs"
+  ConstructKFun -> const $ throwError $ CustomFailure ConstructKFun "type edits currently only allowed in typedefs"


Should these errors read "kind edits"?

Yes, will edit.

brprice · 2023-07-31T13:33:49Z

primer-service/test/outputs/OpenAPI/openapi.json

-                    "DeleteTypeParam"
+                    "DeleteTypeParam",
+                    "MakeKType",
+                    "MakeKFun",
+                    "DeleteKind"


This commit should maybe be a breaking change? We may emit new stuff from the api

Yes, you're right.

brprice

I've left a few minor things above, but this generally looks good to me. Thanks!

We take advantage of this to output proper universally-unique IDs in `API.viewTreeKind`. We still use `Kind' ()` in the definition of `TForall`, since adding the ability to edit such kinds is a complicated change which is out of scope for now. We're initially focused on kinds in typedefs. NB. Even though we are considering getting rid of IDs entirely, we'd almost certainly still want some sort of metadata on nodes, even just for caching, and thus we'd benefit from the significant majority of the changes in this commit, since it's mostly concerned with giving the option to attach metadata to kind nodes. In other words, the exact nature of the metadata on kinds is irrelevant to most of the lines which are changed here. Signed-off-by: George Thomas <[email protected]>

This is analogous to the existing synonym for types, and we use it in roughly the same places. Signed-off-by: George Thomas <[email protected]>

Signed-off-by: George Thomas <[email protected]>

NB. We never actually construct a `Right (Right _)` case yet, but we will after the next commit. Signed-off-by: George Thomas <[email protected]>

Signed-off-by: George Thomas <[email protected]>

The implementation of this is rather ad-hoc (arguably hacky), because some of the machinery used for other actions, in particular `Primer.Zipper`, only supports expressions and types, but not kinds. This is something which should be revisited imminently. Signed-off-by: George Thomas <[email protected]>

Signed-off-by: George Thomas <[email protected]>

georgefst force-pushed the georgefst/typedef-param-kinds-api branch 4 times, most recently from 78e5e4d to 161af8a Compare July 20, 2023 13:04

georgefst force-pushed the georgefst/typedef-param-kinds-api branch from 6151ff8 to 896d9c8 Compare July 24, 2023 12:55

georgefst changed the title ~~Provide API for viewing and editing kinds~~ Provide APIs for viewing and editing kinds of type parameters Jul 24, 2023

georgefst force-pushed the georgefst/typedef-param-kinds-api branch 4 times, most recently from 4798b9b to 5bbf4d0 Compare July 26, 2023 18:45

georgefst commented Jul 26, 2023

View reviewed changes

georgefst mentioned this pull request Jul 26, 2023

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

Closed

georgefst requested a review from a team July 26, 2023 22:29

dhess mentioned this pull request Jul 31, 2023

style: bump fourmolu -> 0.13.1.0 #1099

Closed

brprice reviewed Jul 31, 2023

View reviewed changes

brprice approved these changes Jul 31, 2023

View reviewed changes

georgefst added 5 commits August 7, 2023 22:07

refactor: Define a synonym for no-metadata kinds used in typechecking

7e4fc34

This is analogous to the existing synonym for types, and we use it in roughly the same places. Signed-off-by: George Thomas <[email protected]>

feat!: Include the kinds of type parameters in API trees

fd7c8e3

Signed-off-by: George Thomas <[email protected]>

feat!: Add kind metadata to type def parameter selections

3654893

NB. We never actually construct a `Right (Right _)` case yet, but we will after the next commit. Signed-off-by: George Thomas <[email protected]>

feat!: Allow selections to refer to kinds of type parameters

63b0dd8

Signed-off-by: George Thomas <[email protected]>

georgefst force-pushed the georgefst/typedef-param-kinds-api branch from 5bbf4d0 to 161fc4e Compare August 7, 2023 21:53

georgefst added 2 commits August 7, 2023 23:20

feat!: Add typedef parameter kind actions to "available actions" API

f8b1ea1

Signed-off-by: George Thomas <[email protected]>

georgefst force-pushed the georgefst/typedef-param-kinds-api branch from 161fc4e to f8b1ea1 Compare August 7, 2023 22:21

georgefst added this pull request to the merge queue Aug 8, 2023

Merged via the queue into main with commit e603e61 Aug 8, 2023
2 checks passed

georgefst deleted the georgefst/typedef-param-kinds-api branch August 8, 2023 09:41

georgefst mentioned this pull request Aug 8, 2023

Display and allow editing of typedef parameter kinds hackworthltd/primer-app#1020

Merged

dhess mentioned this pull request Aug 8, 2023

Should we support type definitions with holes? #270

Closed

brprice mentioned this pull request Sep 4, 2023

fix: tcWholeProg updates metadata of ADT parameter selections #1129

Merged

georgefst mentioned this pull request Sep 12, 2023

Editable typedefs: type parameters #402

Open

georgefst mentioned this pull request Sep 25, 2023

Should consistentTypes compare kinds up to holes? #1146

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Provide APIs for viewing and editing kinds of type parameters #1095

Provide APIs for viewing and editing kinds of type parameters #1095

georgefst commented Jul 13, 2023 •

edited

Loading

georgefst Jul 26, 2023

brprice Jul 31, 2023

dhess Jul 31, 2023

georgefst Jul 31, 2023

brprice Jul 31, 2023

georgefst Aug 1, 2023 •

edited

Loading

georgefst Jul 26, 2023

brprice Jul 31, 2023

georgefst Jul 31, 2023

georgefst Jul 31, 2023

dhess Jul 31, 2023

georgefst Jul 31, 2023

dhess Jul 31, 2023 •

edited

Loading

georgefst Jul 26, 2023 •

edited

Loading

brprice Jul 31, 2023

georgefst Aug 1, 2023

georgefst Jul 26, 2023

georgefst Jul 26, 2023

georgefst Jul 26, 2023

dhess commented Jul 27, 2023 •

edited

Loading

georgefst commented Jul 27, 2023

brprice Jul 31, 2023

georgefst Jul 31, 2023

brprice Jul 31, 2023

georgefst Jul 31, 2023

brprice Jul 31, 2023

georgefst Jul 31, 2023

brprice Jul 31, 2023

georgefst Jul 31, 2023

brprice left a comment

		\| TForall a TyVarName Kind (Type' a)
		\| TForall a TyVarName (Kind' ()) (Type' a)

		ConstructKType -> const $ throwError $ CustomFailure ConstructKType "type edits currently only allowed in typedefs"
		ConstructKFun -> const $ throwError $ CustomFailure ConstructKFun "type edits currently only allowed in typedefs"

Provide APIs for viewing and editing kinds of type parameters #1095

Provide APIs for viewing and editing kinds of type parameters #1095

Conversation

georgefst commented Jul 13, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

georgefst Aug 1, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dhess Jul 31, 2023 • edited Loading

Choose a reason for hiding this comment

georgefst Jul 26, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dhess commented Jul 27, 2023 • edited Loading

georgefst commented Jul 27, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

brprice left a comment

Choose a reason for hiding this comment

georgefst commented Jul 13, 2023 •

edited

Loading

georgefst Aug 1, 2023 •

edited

Loading

dhess Jul 31, 2023 •

edited

Loading

georgefst Jul 26, 2023 •

edited

Loading

dhess commented Jul 27, 2023 •

edited

Loading