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">&lt;<a href="mailto:dominique.devriese@cs.kuleuven.be">dominique.devriese@cs.kuleuven.be</a>&gt;</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 &quot;overloaded literals&quot; 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&#39;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 &quot;Fin 3&quot;, 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 &quot;fromℕ 3&quot; with<br>
fromℕ imported from &quot;HasNatLiterals {{...}}&quot;.<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 &lt; 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&lt;k = fromℕ≤ n&lt;k<br>
                fromℕ′ n {} | no ¬n&lt;k<br>
<br>
<br>
  test₂′ : Fin 1000<br>
  test₂′ = 2<br>
    where wnl = wnlFin<br>
<br>
(Note: in &quot;Fin 1000&quot;, 1000 is interpreted as a ℕ, but &quot;2&quot; is<br>
interpreted as a &quot;Fin 1000&quot;). 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&#39;t resolve and color the number 2 in yellow.<br>
<br>
BTW, the current Agda lexer doesn&#39;t seem to lex negative numbers. The<br>
idea seems to be that you use &quot;-_&quot; 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&#39;s and the like.<br>
<br>
This change wouldn&#39;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>