Stream: Coq users

Topic: lambda notation Lean vs Coq


view this post on Zulip Pierre-Marie Pédrot (May 02 2024 at 18:06):

I think that this convention is called Krivine's notation, at least that's how I know it.

view this post on Zulip Notification Bot (May 02 2024 at 18:09):

4 messages were moved here from #Coq users > Status of universe polymorphism? by Robbert Krebbers.

view this post on Zulip Robbert Krebbers (May 02 2024 at 18:10):

Is Coq's parser just not smart enough to allow omitting the parentheses around lambdas when they appear as the last argument, or would it cause ambiguities (and require parentheses in other situations).

view this post on Zulip Notification Bot (May 02 2024 at 18:11):

A message was moved here from #Coq users > Status of universe polymorphism? by Robbert Krebbers.

view this post on Zulip Notification Bot (May 02 2024 at 18:12):

5 messages were moved here from #Coq users > Status of universe polymorphism? by Robbert Krebbers.

view this post on Zulip Mario Carneiro (May 02 2024 at 18:14):

One aspect of this that I think was not possible with the old (lean) parser is that lambdas don't just have one precedence, they have a "leading precedence" which is high (allowing them to be used in an application without parentheses) and a "trailing precedence" which is low (allowing other things with low precedence to be used in the body of the lambda without parentheses). I don't think you can get both of these at once if you just have a single precedence on each notational element (I don't know where Coq lands on this though)

view this post on Zulip Pierre-Marie Pédrot (May 02 2024 at 18:17):

Coq parser is (unfortunately?) Turing complete anyways, so we could hack this.

view this post on Zulip Pierre-Marie Pédrot (May 02 2024 at 18:18):

Krivine's notation is the trademark of the franco-italian λ-calculus school, so I'm not legally allowed to complain, but still, I cannot be forced to say I appreciate it.

view this post on Zulip Théo Winterhalter (May 02 2024 at 18:28):

Robbert Krebbers said:

Is Coq's parser just not smart enough to allow omitting the parentheses around lambdas when they appear as the last argument, or would it cause ambiguities (and require parentheses in other situations).

I don't think it matters, I would be against such a change. It's much better to have a clear end to a binder. This applies to programs on paper that I always find confusing when they use this convention.

I think Agda uses it too though.

view this post on Zulip Gaëtan Gilbert (May 02 2024 at 18:42):

the ocaml parser is like coq in this (ie does not parse x fun ...), but we can get close by writing x @@ fun ...
where a @@ b is application a b

view this post on Zulip Gaëtan Gilbert (May 02 2024 at 18:46):

and can also be used for nested applications at the last argument, ie not @@ Foo.equal x y is not (Foo.equal x y), f a @@ g b @@ h c x is f a (g b (h c x))

view this post on Zulip Mario Carneiro (May 02 2024 at 19:27):

I find f fun x => y exactly as confusing as f @@ g (which is to say, a little unfamiliar, until you realize it is so useful that you use it on every other line)

view this post on Zulip Théo Winterhalter (May 02 2024 at 19:29):

Except at least @@ clearly separates subexpressions.

view this post on Zulip Mario Carneiro (May 02 2024 at 19:29):

Being strict with the parentheses here and not having these kind of "trailing notations" just leads to the lisp style "truckload of close parens" issue at the end

view this post on Zulip Mario Carneiro (May 02 2024 at 19:29):

you just have to learn to read fun in the same way

view this post on Zulip Théo Winterhalter (May 02 2024 at 19:31):

Why would I want to do something that's not helping reading?

view this post on Zulip Théo Winterhalter (May 02 2024 at 19:34):

I almost never have to write functions like that anyway so the lisp hell you mention never occurs.
And in cases where I do want to chain continuations like with monadic code then I would have a notation that's easy to read like x ← e ;; k for bind e (λx. k).

view this post on Zulip Mario Carneiro (May 02 2024 at 19:38):

Perhaps. But it's a bit difficult to ask for people to make notations for every function with a continuation-based interface, and lean metaprogramming has quite a lot of such functions (because anything that makes changes to the read-only part of the monad has to work inside a new scope). Of course you can do what you like, but when I'm reading lean code I have to learn the rules regardless of my own feelings on the situation. Having done so though I can see that there are lots and lots of occurrences of f $ fun x => ... in existing lean code that were simplified by this change

view this post on Zulip Mario Carneiro (May 02 2024 at 19:39):

ultimately, it's not something that takes more than a few minutes to get used to. It's a pretty minor difference in the grand scheme of things

view this post on Zulip Li-yao (May 02 2024 at 19:40):

It's much better to have a clear end to a binder.

Aren't both let and the x <- e ;; k notations counterexamples of that?

view this post on Zulip Mario Carneiro (May 02 2024 at 19:41):

The let ... in ... end syntax from ML drives me absolutely mad

view this post on Zulip Théo Winterhalter (May 02 2024 at 20:42):

Li-yao said:

It's much better to have a clear end to a binder.

Aren't both let and the x <- e ;; k notations counterexamples of that?

You're right. I guess my problem is more that f λx,x u could be either f (λ x, x) u or f (λ x, x u) but with the bind notation it's always clear that whatever appears on the right has to be part of the continuation. So I'll take the version that's never ambiguous.
I think that always having a meaning for the version without parentheses is wrong. Like if you have two operators which are not typically associated, then I want parentheses.

But well, whatever floats your boat.

view this post on Zulip Mario Carneiro (May 02 2024 at 20:57):

Note that in lean, because lambda has lower right precedence than application, the first interpretation is never considered. The usual way this is explained is that fun binds "as far to the right as possible"

view this post on Zulip Mario Carneiro (May 02 2024 at 20:57):

a property it shares with other binders like \forall x, ..., as well as let and other operators with trailing arguments

view this post on Zulip Ralf Jung (May 03 2024 at 05:40):

I'm occasionally using f $ λ x, ..., so far it hasn't bothered me too much... but I can see how it is tempting to optimize away the $, especially when the term otherwise wouldnt parse and this way we can make it useful.

view this post on Zulip Ralf Jung (May 03 2024 at 05:41):

lean metaprogramming has quite a lot of such functions (because anything that makes changes to the read-only part of the monad has to work inside a new scope)

that sounds like a good usecase for monadic notation, though?

view this post on Zulip Mario Carneiro (May 03 2024 at 05:46):

This is in a monadic context. The bind operation here cannot be used to express the subscope because in haskell-speak this is a ReaderT monad and the functions in question are wrappers around withReader. The bind operation in this monad by design cannot change the context, so the context can only be changed inside a sub-scope like withReader's second argument

view this post on Zulip Mario Carneiro (May 03 2024 at 05:52):

Here is a typical example. The forallTelescopeReducing function takes a type which is a sequence of forall expressions (a telescope), and runs the callback on the body of the forall, in a local context extended with free variables for each binder. Once the callback is completed, the local context is restored to the original state (and in fact, because this context is part of the Reader state nothing is actually done to perform this restoration, it is not exposed in such a way that it could change in the first place).

view this post on Zulip Mario Carneiro (May 03 2024 at 05:56):

It is possible to make these be expressible using bind by moving the local context to the "mutable state" part of the monad state (i.e. the StateT monad), but then you would lose the structural property that functions cannot change the local context and more work would be needed to make sure that the context is saved and restored at appropriate points. My impression was that this design was considered and rejected as being too error-prone.

view this post on Zulip Mario Carneiro (May 03 2024 at 06:18):

(To use a rust example, this is like how Mutex::lock can be a regular function in the "rust IO monad" sequenced with let like everything else, but std::thread::scope has to be a callback function, for API design reasons)

view this post on Zulip Théo Winterhalter (May 03 2024 at 06:21):

Mario Carneiro said:

Note that in lean, because lambda has lower right precedence than application, the first interpretation is never considered. The usual way this is explained is that fun binds "as far to the right as possible"

I'm not a parser with built-in precedence. That's my whole point.

view this post on Zulip Mario Carneiro (May 03 2024 at 06:22):

Ultimately, you always have to learn the precedence rules for the language you are writing in. I'm sure you didn't know that @@ was lower precedence than + before you started writing Coq

view this post on Zulip Mario Carneiro (May 03 2024 at 06:26):

There are some precedence relations that you can get away not learning for a long time and/or impose that people use parentheses to disambiguate. IMO, this lambda/application example, in lean, is not one of those cases, it's something you learn within the first few days because it is ubiquitous, and if you insist on putting in the parentheses your code will appear non-idiomatic. Obviously this is not the case in Coq not least because it's a parse error to do so, and I am in no position to make any changes in this regard in Coq. But from my experience in going through this exact transition between lean 3 and lean 4, I think it was a positive change.

view this post on Zulip Janno (May 03 2024 at 09:03):

For writing actual CPS programs (as opposed to one-liners where a fun at the end isn't that bad) I cannot recommend https://github.com/bedrocksystems/BRiCk/blob/master/theories/prelude/letstar.v strongly enough. Writing CPS code using this has been a complete game changer to me. No more unnecessary nesting, no stray funs floating around, no ambiguity about scopes (because we all know how the scope of let binding works), binders at the start of the line instead of at the end, etc. The advantages are endless! (I am only mildly exaggerating.)

view this post on Zulip Gaëtan Gilbert (May 03 2024 at 09:13):

is the 0ary one actually useful? let* := t in f

view this post on Zulip Janno (May 03 2024 at 09:15):

It seems people do like to use it. Maybe just for consistency in a long block of let* where a single let (no star) would look weird?

view this post on Zulip Janno (May 03 2024 at 09:18):

Actually, I don't think that sentence makes any sense. I wasn't the one to add that version and I haven't ever used it so I can't really say why it is useful right now..

view this post on Zulip Karl Palmskog (May 03 2024 at 10:31):

@Janno unfortunately, due to the licensing terms, that piece of code in letstar.v is going to be very difficult for anyone to reuse. As I think I pointed out to Paolo in the past, some easier-to-adhere-to license would be very welcome for generic code the community could benefit from.

view this post on Zulip Karl Palmskog (May 03 2024 at 10:34):

(for example, submission to stdpp would be one one way to solve the issue)

view this post on Zulip Claude Stolze (May 03 2024 at 14:05):

I don't think these few lines of code can be copyrighted, as they don't satisfy the threshold of originality. https://en.wikipedia.org/wiki/Threshold_of_originality

view this post on Zulip Karl Palmskog (May 03 2024 at 14:58):

the file itself claims the copyright, and I don't think people would bet their project's license on this threshold assessment


Last updated: Jun 13 2024 at 19:02 UTC