[Agda] Overloaded literals

[Daniel Peebles]

I would love to see this!

On Mon, Jun 27, 2011 at 2:37 AM, Dominique Devriese <
dominique.devriese at cs.kuleuven.be> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110701/90ced03a/attachment.html