<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Hi<br>
<br>
You are right in so far as the floating point primitives
implementation needs to exactly match the Haskell implementation
used by Agda. Do you have a concrete example where this poses a
problem?<br>
<br>
There are people taking advantage of the fact that Floats can be
reasoned about [1]. I do think that is a valid use case. This would
no longer work if Floats were postulates. Note that Agda does not
stop you from defining your own Float type with postulates. You are
also not required to implement the float primitives if there is no
reasonable way to support them.<br>
<br>
I feel my comment from #3749 also applies here:<br>
<p>
<blockquote type="cite">Is this actually an issue Agda itself
needs to solve? Maybe this is a problem libraries should solve,
as it already today is possible to package the Float
implementation in a record and provide different
implementations. Maybe Agda should just provide the single-nan
primitives <em>for now</em> because they are the most portable
ones and let libraries experiment with packaging it up or adding
different implementations? [2]<br>
</blockquote>
</p>
<br>
Cheers<br>
Philipp<br>
<br>
[1] <a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/2194#issuecomment-251525747">https://github.com/agda/agda/issues/2194#issuecomment-251525747</a><br>
[2] <a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/3749#issuecomment-489795629">https://github.com/agda/agda/issues/3749#issuecomment-489795629</a><br>
<p><br>
</p>
<div class="moz-cite-prefix">On 5/23/19 1:22 AM, Apostolis
Xekoukoulotakis wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAFEV_-hx50y76QwvkUkaeypVzstz8nk8TXQyzLg8ki3-XVrQDA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>I was trying to support floats in agda-ocaml when I
realized that this is a lost cause and a very dangerous one.</div>
<div><br>
</div>
<div>If I didn't match the exact computational results of
haskell, then I could get proofs that typechecked in agda that
were completely wrong in OCaml.</div>
<div><br>
</div>
<div>But there is also a theoretical error in all of this. Right
now, we do not have universal proofs like in Mathematics. We
have platform dependent proofs.</div>
<div><br>
</div>
<div>In other words, we should write explicitly that this proof
is correct for this specific version of the CPU, this specific
version of haskell etc.</div>
<div><br>
</div>
<div>Is it the job of agda to check whether two hardware or
software versions have the same computational results? Of
course not.</div>
<div><br>
</div>
<div>In my opinion, all platform dependent computations should
be inserted as postulates. This way, agda will do exactly what
it was programmed to do.</div>
<div><br>
</div>
<div>And we can still prove things for postulates.</div>
<div><br>
</div>
<div>```</div>
<div>open import Common.Integer<br>
open import Agda.Builtin.Equality<br>
<br>
postulate<br>
Float : Set<br>
d : Float<br>
round : Float → Integer<br>
<br>
f : round d ≡ round d<br>
f = refl<br>
</div>
<div>```<br>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>