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

[Alan Jeffrey]

Lennart also said "Also, as a compiler writer I love the idea that 
evaluation order is left up to me rather than the language spec."

Since Agda is total (ignoring for now code which switches off 
termination checking) the difference between strict and lazy ordering is 
just space and time usage. Should the Agda language specification say 
anything about space/time complexity? Or is that implementation-specific?

If we're going to address higher-order combinators, then I think there 
are bigger issues (cough cough nested uses of combinators cough sized 
types cough) than short-circuiting.

A.

On 12/06/2011 11:08 AM, Nils Anders Danielsson wrote:
> On 2011-12-05 19:35, Alan Jeffrey wrote:
>> Yes, I can see how such a library could be used, but I can also imagine
>> it getting pretty hairy pretty quickly. It's not obvious to me that the
>> benefit outweighs the cost though, given that users can always write:
>>
>>      f xs with b
>>      ... | true = g
>>      ... | false = h
>>
>> instead of (if b then g else h) and get laziness without any explicit
>> thunking.
>
> I wonder if the thunking needs to be explicit—could one use some kind of
> implicit coercions? I don't think Coq's implicit coercion mechanism can
> handle coercions of type
>
>     {A : Set} → A → Thunk A.
>
> Lennart Augustsson describes some of the drawbacks of working in a
> strict language:
>
>     More points for lazy evaluation
>     http://augustss.blogspot.com/2011/05/more-points-for-lazy-evaluation-in.html
>
> His main point is that you can't write things like
>
>     any p = or ∘ map p,
>
> because this definition doesn't short-circuit in the right way.
>
> With a Thunk type we could handle this situation:
>
>     data Thunked-list (A : Set) : Set where
>       []  : Thunked-list A
>       _∷_ : A → Thunk (Thunked-list A) → Thunked-list A
>
>     or  : Thunked-list Bool → Bool
>     map : {A B : Set} → (A → B) → Thunked-list A → Thunked-list B
>
> The standard library already contains a large number of variants of
> lists, so I'm not too keen on adding another dimension—strictness—to the
> design space. However, being able to control the strictness on a
> case-by-case basis seems to be quite important, so we should probably
> support this in some way.
>