Should we prevent annotations of type 'hole'?

[hmac]

Annotations of the form e : ? are basically equivalent in behaviour to a non-empty hole {? e ?}. They often seem to appear as tricky special cases and in some examples of bugs in our system. Would it simplify things if we banned annotations of this form?

Right now, when you add an annotation to an expression, the type is defaulted to ?. This change would mean that we instead default the type to be whatever the type of e actually is. More precisely, if e synthesises T then we would produce e : T, otherwise if e is successfully checked against S during typechecking, we would produce e : S. Since a successful typechecking pass must synthesise or check every expression, this approach will always find a type.

This change doesn't completely prevent holes appearing in annotations. For example, if we add an annotation to a hole we will get ? : ?, since holes synthesise the hole type. The same applies to non-empty holes: adding an annotation to {? Zero ?} will yield {? Zero ?} : ?.

To deal with these two cases, we could disallow annotations on holes. The type of a hole is always ?, so we can argue that annotations are never necessary. But they can be useful if you know what the type of the expression should be, but haven't finished constructing it yet.

So I'm not sure if there's a clear path here, but I think it's worth thinking about.

[dhess]

Right now, when you add an annotation to an expression, the type is defaulted to ?. This change would mean that we instead default the type to be whatever the type of e actually is. More precisely, if e synthesises T then we would produce e : T, otherwise if e is successfully checked against S during typechecking, we would produce e : S. Since a successful typechecking pass must synthesise or check every expression, this approach will always find a type.

I was just about to submit an issue on this particular point right here, but I was coming at it from the user's perspective, rather than the implementation's — i.e., if the user wants to add an annotation, the new annotation should be as specific as it can be given the information that the typechecker has available. I think this is consistent with our principle of being explicit rather than implicit. It might also help users develop their ability to determine types "by eye," by giving them an oracle by which to test their theories.

Therefore, obviously, I support this idea.

To deal with these two cases, we could disallow annotations on holes. The type of a hole is always ?, so we can argue that annotations are never necessary. But they can be useful if you know what the type of the expression should be, but haven't finished constructing it yet.

Disallowing annotations on holes, this I am less sure about. If we're taking a types-first approach, then I can imagine this is the very first thing you want to do with the initial hole: I know the program/function I want to build, so let's start by specifying its type. What if we only allowed an annotation on a hole if it refines the type? By "refine" here I mean, "makes the type more specific."

So here I'm imagining something like: you click the "Add annotation" button on the initial hole and you're given a modal dialog[*] where you can only proceed once you've specified at least one concrete type (or parameterized type, for any parameterized type that might be in scope at this particular hole).

Does that make sense?

[*] edit Maybe not actually a modal dialog, as that might be weird if you're trying to construct, say, a function type.

[brprice]

I'm generally in favour, but...

Right now, when you add an annotation to an expression, the type is defaulted to ?. This change would mean that we instead default the type to be whatever the type of e actually is. More precisely, if e synthesises T then we would produce e : T, otherwise if e is successfully checked against S during typechecking, we would produce e : S. Since a successful typechecking pass must synthesise or check every expression, this approach will always find a type.

... it's not this easy. Sure, for "add an annotation" action, let's do this. But what about the annotations added by smart holes because you want to put something checkable where we need synthesis? E.g. in ? x, try adding a lambda in the hole: this needs to give an annotation also, currently (λx. ? :: ?) x. Certainly in this case we could annotate with ? -> ?, but can we always do something non-trivial?

Similarly, what about if we have a non-trivial annotation and the user trivialises it: ? :: S -> T and hit "delete" on the arrow which currently leaves ? :: ?, but if we do this change should presumably just leave ? and would "delete the thing under the cursor".

Certainly these issues are not insurmountable! They may even shed some light on the smart holes deletion thing that we have been considering lately as well: hackworthltd/vonnegut#194.