Idris2-boot icon indicating copy to clipboard operation
Idris2-boot copied to clipboard

RFC: Generalised dot syntax for postfix application

Open ziman opened this issue 4 years ago • 5 comments

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

Some examples:

  • printLn user.name.length
  • "hello".length.(+3).printLn
  • map (.length.show) ["foo", "booo"]
  • mySet.(insert "hello").(insert "world") <+> otherSet
  • 5 .div 3
  • 5 .(div {ty=Int}) 3
  • foo .(NS.(>>=) {lin = True}) bar

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.

ziman avatar Apr 30 '20 11:04 ziman

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

gallais avatar May 01 '20 13:05 gallais

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.

ziman avatar May 03 '20 16:05 ziman

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

gallais avatar May 03 '20 21:05 gallais

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...

edwinb avatar May 09 '20 11:05 edwinb

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

  • "hello".(printLn . (+3) . length)
  • "hello".length.(printLn . (+3))
  • "hello".length.(+3).printLn

andylokandy avatar May 12 '20 17:05 andylokandy