[Agda] how does BUILTIN work - practical programming in Agda

[Daniel Peebles]

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.

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.

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.

On Tue, Dec 6, 2011 at 10:33 AM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

> 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.
>
> 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?
>
> A.
>
>
> On 12/05/2011 11:31 PM, Daniel Peebles wrote:
>
>> Might it pay to think about a common interface (à la GHC.Prim) that all
>> compiler back-ends should implement (instead of having a bunch of
>> pragmas for each of them) and that would help us get consistent
>> semantics for our programs? I'm still not sure what to do about the
>> strict vs. non-strict issues, but this might help us go in the right
>> direction.
>>
>>
>> On Mon, Dec 5, 2011 at 2:22 PM, Alan Jeffrey <ajeffrey at bell-labs.com
>> <mailto:ajeffrey at bell-labs.com**>> wrote:
>>
>>    On 12/05/2011 01:19 PM, Nils Anders Danielsson wrote:
>>
>>        On 2011-12-05 19:02, Nils Anders Danielsson wrote:
>>
>>            Note that with this approach the type-checker is free to
>>            reduce seqs,
>>            because the reduction removes the thunk.
>>
>>
>>        This argument seems to be incorrect. Besides, does anyone use
>>        seq in a
>>        strict language?
>>
>>
>>    I think the idea is to allow interoperability between strict and
>>    lazy implementations of Agda. In a strict implementation, seq would
>>    be a no-op.
>>
>>    A.
>>
>>    ______________________________**___________________
>>    Agda mailing list
>>    Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se**>
>>    https://lists.chalmers.se/__**mailman/listinfo/agda<https://lists.chalmers.se/__mailman/listinfo/agda>
>>    <https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>> >
>>
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111206/f313cd8b/attachment.html