Idris2-boot
Idris2-boot copied to clipboard
RFC: Generalised dot syntax for postfix application
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.
I have a love/hate relationship with this proposal. But mostly love.
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
.
I expect foo
is the one that would be implicitly bound as it is the one
in argument position.
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...
I'll feel a bit awkward if they're identical:
-
"hello".(printLn . (+3) . length)
-
"hello".length.(printLn . (+3))
-
"hello".length.(+3).printLn