[Agda] Overloaded literals

[Dominique Devriese]

All,

On the last AIM, Andres Löh suggested to use instance arguments to
implement "overloaded literals" like in Haskell. So I have taken a
look over the weekend and I have a POC implementation and am looking
for feedback. I'm just looking at natural number literals at the
moment. The biggest issue is to make sure that 3 or 10 is not accepted
as a literal for "Fin 3", but 2 is accepted. My design is based on the
following type class:

  record HasNatLiterals (t : Set) : Set₁ where
    field ValidLiteral : ℕ → Set
	  decideValid : (n : ℕ) → Dec (ValidLiteral n)
	  fromℕ : (n : ℕ) → {valid : True (decideValid n)} → t

The literal 3 for example is then interpreted as a call "fromℕ 3" with
fromℕ imported from "HasNatLiterals {{...}}".

This means I can do the following:

  wnlℕ : HasNatLiterals ℕ
  wnlℕ = record { ValidLiteral = const ⊤;
		  decideValid = const $ yes tt;
		  fromℕ = λ x → x }

  wnlFin : {k : ℕ} → HasNatLiterals (Fin k)
  wnlFin {k} = record { ValidLiteral = λ n → n < k;
			 decideValid = λ n → suc n ≤? k;
			 fromℕ = fromℕ′ }
	  where fromℕ′ : (n : ℕ) → {valid : True (suc n ≤? k)} → Fin k
		fromℕ′ n {valid} with suc n ≤? k
		fromℕ′ n {tt} | yes n<k = fromℕ≤ n<k
		fromℕ′ n {} | no ¬n<k


  test₂′ : Fin 1000
  test₂′ = 2
    where wnl = wnlFin

(Note: in "Fin 1000", 1000 is interpreted as a ℕ, but "2" is
interpreted as a "Fin 1000"). If I do

  test₃′ : Fin 2
  test₃′ = 2
    where wnl = wnlFin

Then Agda will complain about a meta-variable of type Data.Empty that
it can't resolve and color the number 2 in yellow.

BTW, the current Agda lexer doesn't seem to lex negative numbers. The
idea seems to be that you use "-_" from Data.Integer if you want that.

I expect it to be easy to do something similar for floats and strings.
Doing it for strings seems neat, because the decideValid stuff would
allow compile-time checking of regexp's and the like.

This change wouldn't be backwards compatible by the way. Maybe it
should be only enabled if an extension is enabled?

I can put my current code online if someone would like to see it.

All feedback welcome.

Dominique