I think that this convention is called Krivine's notation, at least that's how I know it.
4 messages were moved here from #Coq users > Status of universe polymorphism? by Robbert Krebbers.
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).
A message was moved here from #Coq users > Status of universe polymorphism? by Robbert Krebbers.
5 messages were moved here from #Coq users > Status of universe polymorphism? by Robbert Krebbers.
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)
Coq parser is (unfortunately?) Turing complete anyways, so we could hack this.
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.
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.
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
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))
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)
Except at least @@
clearly separates subexpressions.
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
you just have to learn to read fun
in the same way
Why would I want to do something that's not helping reading?
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)
.
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
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
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?
The let ... in ... end
syntax from ML drives me absolutely mad
Li-yao said:
It's much better to have a clear end to a binder.
Aren't both
let
and thex <- 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.
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"
a property it shares with other binders like \forall x, ...
, as well as let
and other operators with trailing arguments
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.
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?
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
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).
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.
(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)
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.
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
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.
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 fun
s 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.)
is the 0ary one actually useful? let* := t in f
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?
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..
@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.
(for example, submission to stdpp would be one one way to solve the issue)
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
the file itself claims the copyright, and I don't think people would bet their project's license on this threshold assessment
Last updated: Oct 13 2024 at 01:02 UTC