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

[Nils Anders Danielsson]

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.

-- 
/NAD