[Agda] tuple patterns

[Serge D. Mechveliani]

On Sat, Sep 22, 2012 at 01:36:21PM +0200, Nils Anders Danielsson wrote:
[..]
>> And if the first pattern  ``... | no p''  shoots at run time, I need
>> ``orderedList? (y :: xs)''  not to evaluate here -- by laziness
>> (which laziness is used here for optimization). Is this reliable in
>> Agda ?
>
> I'm not sure how parallel withs are translated into the internal
> language. The MAlonzo backend compiles via Haskell, which presumably
> gives you the right behaviour. Perhaps you get the right behaviour with
> the other backends as well; one option is to inspect the generated
> source.

I wonder whether this feature needs to be defined in the very  
                                                     language semantic.

For example, consider for Haskell the clause   f (x, y) = x + 1, 
and apply                                      f (2, last [0 ..]) 
(with taking last in an infinite list). 
The language is defined so that the result is predictable as  3,
other value is a language implementation error.
If Haskell allowed here to compute  y,  the result would occur different.
Hence the Haskell language was forced to specify this point.

But  Agda  does not allow non-termination, nor breaks. Hence the above 
value  3  for  f (x, y)  does not depend on this laziness point!
I have an impression that this is all right for the  language definition 
(is there possible a subtle example?).
But at least there is a danger for performance.
Depending on the taste of the compiler developer, the time cost may change 
million times for a simply looking innocent function.

What do people think of this?

Regards,

------
Sergei