must write arg types if ret type specified

Stream: lean4

[James Gallicchio]

What is the reason for def type holes being filled in before processing the body, when a return type is specified?

I find myself doing stuff like

def myFun (something) := show Id MyType from ...

to get around it, which is honestly quite clean for a workaround. But wondering why the restriction is in place / if there are examples where this workaround doesn't actually work.

[Mario Carneiro]

it is to prevent large scale instability when you change the body of a proof. It's the same reason Rust requires full function signatures even though it is quite capable of performing whole program type inference, it is a hard won lesson from languages like ML and Haskell that allow it but have to have conventions saying you really shouldn't

[James Gallicchio]

Okay... but that's the sort of thing linters are for, no? And with the do notation requiring an expected type, I frequently want to write def myThing (x) : IO _ := do ... and let type inference fill in the otherwise easily inferrable signature.

[James Gallicchio]

It's definitely fine, since the workaround is pretty easy, but sometimes it feels like the compiler getting in the way unnecessarily

[James Gallicchio]

(Is there a thread discussing the choice? I couldn't find any from zulip searching)

[Mario Carneiro]

Okay but then in the next file over it's rather confusing to see a function called myThing with type IO _

[Mario Carneiro]

like, I wouldn't recommend the workaround either

[Mario Carneiro]

I do that for #eval blocks but never for def

[James Gallicchio]

The hole is standing for a concrete type that I just don't want to write out, not a polymorphic type

[Mario Carneiro]

right, so what type is it? the next file wants to know

[Mario Carneiro]

that kind of thing is why I hate reading ML code

[James Gallicchio]

hm, I guess I am biased by always reading lean code in editor, where i can just hover to see the type :thinking:

[James Gallicchio]

ML code without types does become unreadable

[Alex Keizer]

I would argue that even in-editor it's valuable to write the type. Then you can just see it at a glance, rather than having to hover. Especially if there's many such holes