Oh, I wasn't suggesting tying ourselves to a particular bignum implementation. I just meant coming up with a common set of primitive types and operations on those types that compiler backends expose directly, without using pragmas. <div>
<br></div><div>The primitive module would have no actual source code, and would contain things like Integer and addInteger : Integer -> Integer -> Integer, and compiler backends might be expected to provide some of them (and others might be optional?), a bit like how GHC's primitives work. The compiler could choose on how to implement each of them in a way that's best suited to it, but we'd also have a built-in module with a bunch of postulated properties about the primitives, so we could rely on consistent behavior and prove things about them.</div>
<div><br></div><div>I just think this might be better as we go forward and more backends appear. Otherwise we can't really be sure which functions/types have primitive bindings in what backends and it's really hard to make assumptions about anything much.</div>
<div><br><div class="gmail_quote">On Tue, Dec 6, 2011 at 10:33 AM, Alan Jeffrey <span dir="ltr"><<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
I'm going to be a broken record here, but I'm not very excited about hard-wiring a particular implementation of bignums into the Agda compiler. I'd like to keep this level of hackery in a library and out of the compiler.<br>
<br>
That said, the current situation where FFI bindings have to be in the same file as the declaration is problematic, particularly for the standard library, which would end up needing pragmas for every primitive type for every back end. Perhaps we should look at allowing pragmas to be declared in different files?<span class="HOEnZb"><font color="#888888"><br>
<br>
A.</font></span><div class="im"><br>
<br>
On 12/05/2011 11:31 PM, Daniel Peebles wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
Might it pay to think about a common interface (à la GHC.Prim) that all<br>
compiler back-ends should implement (instead of having a bunch of<br>
pragmas for each of them) and that would help us get consistent<br>
semantics for our programs? I'm still not sure what to do about the<br>
strict vs. non-strict issues, but this might help us go in the right<br>
direction.<br>
<br>
<br>
On Mon, Dec 5, 2011 at 2:22 PM, Alan Jeffrey <<a href="mailto:ajeffrey@bell-labs.com" target="_blank">ajeffrey@bell-labs.com</a><br></div><div class="im">
<mailto:<a href="mailto:ajeffrey@bell-labs.com" target="_blank">ajeffrey@bell-labs.com</a><u></u>>> wrote:<br>
<br>
On 12/05/2011 01:19 PM, Nils Anders Danielsson wrote:<br>
<br>
On 2011-12-05 19:02, Nils Anders Danielsson wrote:<br>
<br>
Note that with this approach the type-checker is free to<br>
reduce seqs,<br>
because the reduction removes the thunk.<br>
<br>
<br>
This argument seems to be incorrect. Besides, does anyone use<br>
seq in a<br>
strict language?<br>
<br>
<br>
I think the idea is to allow interoperability between strict and<br>
lazy implementations of Agda. In a strict implementation, seq would<br>
be a no-op.<br>
<br>
A.<br>
<br></div><div class="im">
______________________________<u></u>___________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>><br>
<br>
<br>
</div></blockquote>
</blockquote></div><br></div>