edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

RFC: Generalised dot syntax for postfix application #342

Open ziman opened 4 years ago

ziman commented 4 years ago

Here's a more radical idea: .(expr) and .name are postfix applications of expr/name that bind tighter than application.

Some examples:

This patch did not require any changes to the existing code in the stdlib and tests (other than the recent record test).

One issue I see with this is that idiomatic functions put the main arguments last so you can't write myList.map (+1) and you have to write myList.(map (+1)) instead. There is myList.for printLn but that works only in Applicative contexts.

gallais commented 4 years ago

I have a love/hate relationship with this proposal. But mostly love.

ziman commented 4 years ago

If we do this, we should tell the elaborator not to generalise names after dots to avoid foo.n -> T being translated as {0 n : _} -> n foo -> T.

gallais commented 4 years ago

I expect foo is the one that would be implicitly bound as it is the one in argument position.

edwinb commented 4 years ago

I'm a bit scared of this one, although I do kind of like it... I think... maybe if we are going to have it, it should be hidden behind a %language pragma?

I think we've overdone syntactic trickery and experimentation in the past, but somehow I still want to play with this...

andylokandy commented 4 years ago

I'll feel a bit awkward if they're identical: