I would love to see this!<br><br><div class="gmail_quote">On Mon, Jun 27, 2011 at 2:37 AM, Dominique Devriese <span dir="ltr"><<a href="mailto:dominique.devriese@cs.kuleuven.be">dominique.devriese@cs.kuleuven.be</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">All,<br>
<br>
On the last AIM, Andres Löh suggested to use instance arguments to<br>
implement "overloaded literals" like in Haskell. So I have taken a<br>
look over the weekend and I have a POC implementation and am looking<br>
for feedback. I'm just looking at natural number literals at the<br>
moment. The biggest issue is to make sure that 3 or 10 is not accepted<br>
as a literal for "Fin 3", but 2 is accepted. My design is based on the<br>
following type class:<br>
<br>
record HasNatLiterals (t : Set) : Set₁ where<br>
field ValidLiteral : ℕ → Set<br>
decideValid : (n : ℕ) → Dec (ValidLiteral n)<br>
fromℕ : (n : ℕ) → {valid : True (decideValid n)} → t<br>
<br>
The literal 3 for example is then interpreted as a call "fromℕ 3" with<br>
fromℕ imported from "HasNatLiterals {{...}}".<br>
<br>
This means I can do the following:<br>
<br>
wnlℕ : HasNatLiterals ℕ<br>
wnlℕ = record { ValidLiteral = const ⊤;<br>
decideValid = const $ yes tt;<br>
fromℕ = λ x → x }<br>
<br>
wnlFin : {k : ℕ} → HasNatLiterals (Fin k)<br>
wnlFin {k} = record { ValidLiteral = λ n → n < k;<br>
decideValid = λ n → suc n ≤? k;<br>
fromℕ = fromℕ′ }<br>
where fromℕ′ : (n : ℕ) → {valid : True (suc n ≤? k)} → Fin k<br>
fromℕ′ n {valid} with suc n ≤? k<br>
fromℕ′ n {tt} | yes n<k = fromℕ≤ n<k<br>
fromℕ′ n {} | no ¬n<k<br>
<br>
<br>
test₂′ : Fin 1000<br>
test₂′ = 2<br>
where wnl = wnlFin<br>
<br>
(Note: in "Fin 1000", 1000 is interpreted as a ℕ, but "2" is<br>
interpreted as a "Fin 1000"). If I do<br>
<br>
test₃′ : Fin 2<br>
test₃′ = 2<br>
where wnl = wnlFin<br>
<br>
Then Agda will complain about a meta-variable of type Data.Empty that<br>
it can't resolve and color the number 2 in yellow.<br>
<br>
BTW, the current Agda lexer doesn't seem to lex negative numbers. The<br>
idea seems to be that you use "-_" from Data.Integer if you want that.<br>
<br>
I expect it to be easy to do something similar for floats and strings.<br>
Doing it for strings seems neat, because the decideValid stuff would<br>
allow compile-time checking of regexp's and the like.<br>
<br>
This change wouldn't be backwards compatible by the way. Maybe it<br>
should be only enabled if an extension is enabled?<br>
<br>
I can put my current code online if someone would like to see it.<br>
<br>
All feedback welcome.<br>
<br>
Dominique<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br>