ide autocomplete instance methods

Stream: general

[Matthew Pocock]

When in an instance declaration, would it be possible to get the IDE to autocomplete unimplemented method names as you get to them, or to stub them all out with sorry?

[Kyle Miller]

If you do instance : Myclass := _ you should get a blue lightbulb appear in VS Code that gives you a code action to generate a skeleton

[Matthew Pocock]

Kyle Miller said:

If you do instance : Myclass := _ you should get a blue lightbulb appear in VS Code that gives you a code action to generate a skeleton

Thanks - that seems to work :D I would never have guessed it though, as I only knew of the where syntax for instance declarations.

[Patrick Massot]

Yes, we really need to figure out how to get this to work with where which is clearly the preferred syntax.

[Eric Wieser]

Well, it at least generates a where!

[Jireh Loreaux]

Speaking of where, why can't we nest it?

[Mario Carneiro]

nest it where?

[Jireh Loreaux]

structure Foo where
  x : Nat

structure Bar where
  f : Foo

def bar : Bar where
  f := { x := 0 }

def baz : Bar where
  f where -- unexpected token 'where'; expected ':=' or '|'
    x := 0

[Mario Carneiro]

you can do f.x := 0

[Jireh Loreaux]

I've never seen that, is it documented?

[Mario Carneiro]

inasmuch as anything is

[Eric Wieser]

Does it auto complete dotted names when you're in the where scope?

[Jireh Loreaux]

While that is convenient, it is less so when the name is long, e.g.

structure FooThatHasAReallyLongName where
  x : Nat
  y : Nat
  z : Nat

structure Bar where
  toFooThatHasAReallyLongName : FooThatHasAReallyLongName

def bar : Bar where
  toFooThatHasAReallyLongName := { x := 0, y := 1, z := 2 }

def baz : Bar where
  toFooThatHasAReallyLongName.x := 0
  toFooThatHasAReallyLongName.y := 1
  toFooThatHasAReallyLongName.z := 1

[Eric Wieser]

It also doesn't help if you have a function that takes a structure value

[Eric Wieser]

foo { x.y := 1 } is illegal, right?

[Eric Wieser]

(certainly foo { f x := x^2 } is)

[Kyle Miller]

Sometimes I wish where ... was a term as an alternative to { ... }. For example,

  return where
    x := 1
    y := 2

I've found returning { ... }'s awkward since "return" plus a space is seven characters, and you can't put the { on the next line.

Or in Jireh's case

def baz : Bar where
  toFooThatHasAReallyLongName := where
    x := 0
    y := 1
    z := 1

[Eric Wieser]

I'm torn on whether that second case should have a := before the where

[Mario Carneiro]

I agree, although that would be ambiguous with

def baz : Bar {
  toFooThatHasAReallyLongName := {
    x := 0
    y := 1
    z := 1
  }
}

[Eric Wieser]

Is that syntax legal?

[Kyle Miller]

I meant it with the :=

[Mario Carneiro]

It's an application of a structure instance to Bar

[Mario Carneiro]

and the first half of a definition

[Kyle Miller]

It needs a different keyword than where, since not only that, the where clause at the end of a definition would be ambiguous

[Mario Carneiro]

that could be fixed by whitespace sensitivity

[Mario Carneiro]

the where at the end of a declaration is also terribly ambiguous though

[Eric Wieser]

While we're wishing for syntax,

foo where
   x := 1

might be nice as sugar for foo (x := 1)

[Mario Carneiro]

I don't think where is a very good keyword to start a term with though

[Eric Wieser]

Though obviously that clashes with the above!

[Kyle Miller]

where is sort of nifty if you think of passing a structure to a function as being a way to pass keyword arguments, but except for that particular use it doesn't read well

[Mario Carneiro]

I think it makes sense in let declarations and other declaration-looking things, but I wouldn't make it a term

[Mario Carneiro]

although where is technically followed by a list of letDecl, so if let supported it then you could also do nested where

[Mario Carneiro]

There is also withForbidden for dealing with the ambiguity I mentioned above (which exists to deal with the issue that x do ... is x (do ...) but for _ in x do ... is not parsed in that way)

[Mac Malone]

One key problem is that any def can end with a where set of decls, so having a where anywhere inside a declaration (outside brackets) clashes with that.

[Mac Malone]

Eric Wieser said:

While we're wishing for syntax,

foo where
   x := 1

might be nice as sugar for foo (x := 1)

Back to David's old proposal, are we? :laughter_tears: