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

[Daniel Peebles]

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> 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
> 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/d6481b26/attachment.html