Zulip Chat Archive

Stream: lean4

Topic: Ignore expected type for ▸


Parth Shastri (Nov 03 2022 at 01:48):

Is there a nice way to prevent a ▸ b from searching the expected type to determine the substitution and instead only search b? Here's my current workaround in a minimal example:

def add (x y : Nat) := x + y

example (h₁ : z = x + y) (h₂ : w = z) : w = add x y :=
  have := h₁  h₂; by exact this

Relying on by exact not influencing the expected type of thisfeels brittle, but removing it results in an error:

invalid `▸` notation, expected result type of cast is
  w = add x y
however, the equality
  h₁
of type
  z = x + y
does not contain the expected result type on either the left or the right hand side

Reid Barton (Nov 03 2022 at 06:57):

Does this work?

example (h₁ : z = x + y) (h₂ : w = z) : w = add x y :=
  (h₁  h₂ : _)

Mario Carneiro (Nov 03 2022 at 07:19):

No, that doesn't work any more in lean 4. I made a (e :) elaborator for this use case in a post somewhere, but I don't think it's been added to mathlib yet

Mario Carneiro (Nov 03 2022 at 12:20):

lean4#1797

Mario Carneiro (Nov 03 2022 at 13:40):

/poll What should the syntax for "elaborate e without expected type" be?
(e :) (implemented in lean4#1797)
(e : _) (used in lean 3, doesn't work without a special case in lean 4)

Mario Carneiro (Nov 03 2022 at 13:42):

Leo wants to know how people feel about the new syntax for elaborating without an expected type. The (e :) syntax is a little unusual, but you can think of it as a "type ascription with no type" since that's the intended effect.

Arthur Paulino (Nov 03 2022 at 13:45):

Writing nothing after ":" looks a bit out of place within the world of Lean 4 syntax

Mario Carneiro (Nov 03 2022 at 13:46):

it helps signal that this is different from other type ascriptions. In the original version the :) part was actually a token

Mario Carneiro (Nov 03 2022 at 13:48):

What I don't like about (e : _) is that we can't just make it work, the elaborator is too smart and sees around it. This has to be a special case which means that (e : _) and (e : ?_) won't act the same

Mario Carneiro (Nov 03 2022 at 13:49):

There is also the unstated "something else" alternative if you have a better idea for a type-ascription-ish syntax that signposts this behavior

James Gallicchio (Nov 03 2022 at 14:12):

I actually like the ( ... :) syntax... if I saw it without knowing about it, I'd almost certainly look it up / ask on Zulip, which seems like a good thing IMO

  • it's fun to have little smilies in our codebases :)

Mario Carneiro (Nov 03 2022 at 14:14):

It is mentioned in the docstring when you hover on it BTW

Mario Carneiro (Nov 03 2022 at 14:16):

although the docstring for parentheses is unfortunately very overloaded, having to describe all the syntaxes:

  • ()
  • (e)
  • (e :)
  • (e : ty)
  • (e1, e2)
  • (· + ·)

Jannis Limperg (Nov 03 2022 at 16:19):

I would make it a keyword, i.e. elab_without_expected_type e or something. This situation is hopefully not common enough to warrant short (and very mysterious) notation.

Mario Carneiro (Nov 03 2022 at 17:00):

If it's longer than have' := e; exact this then it's not really worth it

Mario Carneiro (Nov 03 2022 at 17:02):

It doesn't come up that often but in the places I have wanted it I also wanted a syntax that felt "built-in" for it

James Gallicchio (Nov 03 2022 at 17:02):

not sure it's about length but rather clarity of intent, right? if anything (e :) is more clearly "we're doing something weird" than using exact e in this weird way

James Gallicchio (Nov 03 2022 at 17:02):

and some keyword like elab_without_expected_type is very clear in intent

Mario Carneiro (Nov 03 2022 at 17:11):

yes, but it's also so obnoxiously long that I would never want to use it outside a macro

Gabriel Ebner (Nov 03 2022 at 17:35):

Jannis Limperg said:

This situation is hopefully not common enough to warrant short (and very mysterious) notation.

$ cd mathlib
$ rg ' : _\)' | wc -l
391

Jannis Limperg (Nov 03 2022 at 18:21):

Why does additional information make the elaborator fail so often? Does Lean 4 also have this sort of issue?

Mario Carneiro (Nov 03 2022 at 18:22):

Elaborator decisions are not always "confluent". For example it might make the difference between putting the coercions in one place or another

Mario Carneiro (Nov 03 2022 at 18:23):

combine this with the fact that lean tries not to backtrack during elaboration and you get occasional failures in edge cases

Mario Carneiro (Nov 03 2022 at 18:23):

The issues here are usually not that the elaborator has made an unambiguously wrong decision, it is just making a different decision

Mario Carneiro (Nov 03 2022 at 18:26):

We want the elaborator to have reasonably predictable behavior so that limits how smart we can make the heuristics, and we also don't want it to timeout or re-elaborate things many times so that limits the ability to recover. This is one way among many to nudge the elaborator in the right direction in specific situations

Jannis Limperg (Nov 03 2022 at 19:00):

All right, interesting.


Last updated: Dec 20 2023 at 11:08 UTC