[Agda] Overloaded literals

[Dominique Devriese]

All,

2011/7/5 Nils Anders Danielsson <nad at chalmers.se>:
> On 2011-06-27 08:37, Dominique Devriese wrote:
>> My design is based on the following type class:
>>
>>   record HasNatLiterals (t : Set) : Set₁ where
> Do you use BUILTIN pragmas to "bless" this type?

Yes.

> fromℕ′ is available (more or less) in the standard library as
> Data.Fin.#_. The following code is accepted:
>
>  i : Fin 1000
>  i = # 2

Thanks for the pointer. My fromℕ is an ad hoc overloaded version of
this #_ function.

> With your suggested feature we can write the following instead:
>
>>   test₂′ : Fin 1000
>>   test₂′ = 2
>>     where wnl = wnlFin
> The difference seems small to me. Do you have a killer application in
> mind?

Yes, the difference is small...

The motivation for the feature would be:
* bring Agda closer to Haskell (at least for integer and float
  literals). As far as I can tell, overloaded literals are generally
  liked in the Haskell community.
* allow "native" syntax for library types, instead of requiring the
  slight extra verbosity of an operator like '#_'

The main downside of the proposed change is that it weakens type
inference a bit: E.g. '3 : ℕ' can no longer be automatically inferenced...

I agree though that the motivation for overloaded literals in Agda is
weaker than in Haskell, because the choice between e.g. Int and
Integer cannot be so easily decided there. In Agda, I have a sense
that ℕ is 'more fundamental' than Integer in Haskell.

By the way, the idea would be to do the same thing for floats and
strings as done for ℕ above.

Still, the feature is actually more powerful in Agda, because we can
do compile-time checking of the literal values (as for Fin k above).
As I said, if I add overloadedstrings (exists as a GHC extension to
Haskell), this would allow for automatic compile-time checking and
compilation of regular expressions provided as strings (or SQL
commands or ...), which I would find neat. Still, you can do the same
thing now with a /_/ operator similar to your #_ operator above, but
it would have slightly more verbose syntax... If this is not clear, I
can cook up an example. I need to check if I can find an Agda RegEx
library somewhere.

Dominique