Student-defined types about primer HOT 20 CLOSED

I've put down some preliminary thoughts on this here (editor's note: the link that was referred to no longer works).

from primer.

Notes from the 2020-12-02 priorities meeting:

• @brprice says we have enough in the backend to do this, and it's mostly a matter of UI/frontend at this point.

from primer.

Notes from the 2020-12-02 priorities meeting:

* @brprice says we have enough in the backend to do this, and it's mostly a matter of UI/frontend at this point.

Well, in the typechecker. We will need to add actions to the backend though.

from primer.

Note that it may be worth changing the representation of typedefs (in particular, value constructors) before exposing it to users.

from primer.

Rather than invent a new editing language for this, I think it might be simpler to present the user with a form-like UI to construct a type, which we then submit to the backend in one go.

from primer.

As long as we can edit a type definition sanely, I'm all for just shoving it into a form (with embedded bits to construct types as usual).

I'm imagining a form where there are buttons for "add ctor"; "add argument to this ctor"; all names are textboxes and each argument to each constructor is an embedded type-construction widget (as we have for annotations in normal program code). Then to create a new type we bring up a blank form, to edit a type we pre-populate with the current definition.

from primer.

A form-based UI seems like a good idea for sum and product types, as long as it can handle recursive definitions.

What about more complicated types, like GADTs or rank N types?

from primer.

I think it would extend fairly smoothly to support GADTs, by letting the user edit the type params in the result type of each constructor. Higher rank types, just syntactically, are a bit more of a pain because we need to allow you to insert foralls wherever you want.

from primer.

Do we want to allow type holes inside types, something like

data Result where
  Good :: Int -> Result
  Error :: ? -> Result

i.e. "I know I need an error case, but don't yet know what data I want to return in that case"

from primer.

We may want to tackle hackworthltd/vonnegut#135 before this

from primer.

One more thought on doing this in a simplified UI, and I think it applies generally and not just to this particular issue: we should have a first-class "escape hatch" for more complicated forms that can't be captured in a simpler UI.

For example, one thing that block-based programming environments struggle with is representing code that wasn't originally written in the block representation. [1] Microsoft has done a bit of work on this in their MakeCode JavaScript block programming environment: https://makecode.microbit.org/blocks/javascript-blocks

With respect to this particular issue, a form-based UI for building types is good, but (assuming we ever need it) users should also be able to represent/build types that don't work well with this approach. I wouldn't want them to have to write these more complicated types outside the editor and then "import" them as black boxes, for example.

[1] Here I do not mean primitives like arithmetic operations; I don't think we should go out of our way to make those appear identical to user-defined functions, though it would be nice if they at least have surface similarities: e.g., function parameters to these primitive functions should ideally be rendered the same as function parameters to user-defined functions.

from primer.

I think it would extend fairly smoothly to support GADTs, by letting the user edit the type params in the result type of each constructor. Higher rank types, just syntactically, are a bit more of a pain because we need to allow you to insert foralls wherever you want.

Cool, if your design incorporates GADTs from the start, I think that's a great fit.

With Alpha, we decided to require explicit foralls for its (textual) representation of polymorphic types. What are your thoughts on that in the context of a form-based UI? If I recall correctly, we did this to help distinguish type parameters from function parameters, so perhaps it isn't necessary in a graphical representation?

from primer.

[Note: I wrote this earlier today before we'd discussed the mockup in more detail, but figure it's still useful info]

With ordinary rank 1 types, we can easily render an explicit forall around each constructor, like this:

Nil : ∀ a. List a
Cons : ∀ a. a → List a → List a

The foralls would not be editable, they'd just be generated by whatever set of type parameters you specify for your type. I think this might be a good idea to show how the type parameters of the type affect the constructors. But we can switch this on and off easily and see how each option feels to use.

For higher rank types, we would need some way to let you wrap any type (sub)expression in a forall. For example consider this constructor:

MkFunctor : ∀ f. (∀ a b. (a → b) → f a →  f b) → Functor f

The inner ∀ a b wraps just the argument of the constructor, not its whole type.

from primer.

I think this is done (closed by hackworthltd/vonnegut#226), yes? It's not hooked up to the backend, but we have a way to define the types, at least.

from primer.

We'll keep this open for now, as it sounds like @hmac would like to continue using this issue to track the state of user-defined types in general, and not just "what is the UI for defining them?", which is what I had in mind when I suggested that it had been closed by hackworthltd/vonnegut#226.

from primer.

This is now a tracking issue for the overarching project. Smaller tasks have been split into

• Hook up the "define a type" form hackworthltd/vonnegut#369
• Editing type defs #99
• Viewing type defs (in the canvas) hackworthltd/vonnegut#371

from primer.

I'm going to move this back to high priority, as I'd like to see if we can get this enabled for student testing this summer. As we are advocating a "types first" approach, we'd better have good support for defining types!

from primer.

I should clarify my previous comment: for the demo and initial summer testing, we can't do this properly as there are many semantic and UX issues to work out about how to change an existing type. But we will need some way to at least "fake" the student creating a new type.

For example, in the beginner testing script, we will ask students to define a few types. They can do this in the existing type definition form with no problems, and even see a (text-only) representation of the type they're creating. So that should all work fine.

The question to resolve for this initial implementation is, what's the next step?

• Do we create the type in the program and say it's read-only after definition, i.e., can't be changed? What if they defined it incorrectly? At the very least, we'd want them to be able to delete the existing type and try again. This seems pretty rubbish, though.

* Do we not actually create the type and fake it by loading up a session with the type properly defined and ready for use? This will skirt a lot of the UX problems, but what if the student's type wasn't correct and it's substantially different than the type we pre-defined for them? We may be able to hand-wave this away by saying, "OK, imagine you created that type slightly differently, like so." But then, shouldn't they be able to inspect the type and its constructors? It's a bit much to ask them to write a function on a type that they didn't define and different substantially from the one they did define in the "new type" UI.

It seems to me at the very least we'll need a way to inspect a type's constructors once it's been created. Currently, we don't support that and it's actually a pretty big oversight!

Once hackworthltd/vonnegut#654 is merged, students will be able to create their own types, but won't be able to delete them. I think this is good enough for initial testing.

If they define them incorrectly, maybe we should just allow them to go with it and see how far they can get anyway. Perhaps they'll even realize that they've done something incorrectly and go create a new version of that type. (We'll have to explain to them that, due to it being a prototype, they can't delete the old type, so they should just ignore it and create a new version.)

from primer.

Note: I removed this from the "UX for beginners" and "Demo" trackers, because it's clear we won't be able to solve the really difficult problem of how to edit existing types in time.

We'll continue to use this to track this and other student-defined type issues, however.

from primer.

I think issue has outlasted its usefulness and should now be closed. There's more work to be done on editing typedefs and investigating a tree-based typedef editing UI, but those can be tracked separately (and in the case of editing typedefs, already is in #401 and #402).

from primer.