search

edwinb / Idris2-boot

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

`with` expressions for name disambiguation #359

Closed ziman closed 4 years ago

ziman commented 4 years ago

In https://github.com/edwinb/Idris2/pull/308, we talked about restricting disambiguation for better error messages. (See that pull request for a motivating example.)

While some aspects of the original proposal were controversial, it seems that most people were okay with notation like with Prelude.(>>=) do ....

This patch adds new syntax with NS.name <term> and with [NS.name1, NS.name2, ...] <term> to determine disambiguation for the specified names in <term> without search.

The names given need not be fully qualified, so with Vect.Nil will work for Data.Vect.Nil, as long as that's the only possible disambiguation, and you can even say with Nil [] if there's only one Nil in scope.

BTW, the syntax allows with Prelude.pure the (Maybe _) (pure 4) without parenthesising the RHS. Not sure if I should restrict it; it's syntactically unambiguous because the list of identifiers is unambiguous but it looks kind of strange to me. However, I definitely want to support with ... do ... without parenthesising the do expression so I decided to leave it at this for now. Suggestions welcome.

ziman commented 4 years ago

This patch has been ported to the self-hosted version of Idris2.