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

[Alan Jeffrey]

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>
>
>