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

[Alan Jeffrey]

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.

A.

On 12/05/2011 12:02 PM, Nils Anders Danielsson wrote:
> On 2011-12-05 18:06, Alan Jeffrey wrote:
>> I'm not sure coinduction is the way to give laziness hints to the
>> compiler, as that might impact the semantics of the terms (e.g. lazy
>> lists would become co-lists even if the laziness was only intended to
>> be for efficiency reasons, not for coinduction).
>
> It is easy to imagine using a dedicated type constructor for laziness
> (as is often done in strict languages):
>
>     data Thunk (A : Set) : Set where  -- /Not/ a record type.
>       thunk : (x : A) → Thunk A
>
>     {-# BUILTIN LAZY thunk #-}
>
>     force : {A : Set} → Thunk A → A
>     force (thunk x) = x
>
>     seq : {A B : Set} → Thunk A → B → B
>     seq (thunk _) x = x
>
>     if_then_else_ : {A : Set} → Bool → Thunk A → Thunk A → A
>     if true  then x else y = force x
>     if false then x else y = force y
>
> Note that with this approach the type-checker is free to reduce seqs,
> because the reduction removes the thunk. Occurrences of seq may be
> present in types, but we can prove the following lemma:
>
>     seq-vanishes : {A B : Set} (x : Thunk A) (y : B) → seq x y ≡ y
>     seq-vanishes (thunk _) _ = refl
>
> Something like this would be /very/ easy to implement, at least in the
> MAlonzo backend.
>
> I wonder how awkward it is to program with explicit laziness. My
> experience is that the explicit distinction between inductive and
> coinductive types make it easier for me to understand the programs I'm
> writing.
>
> Aside: I once designed a library for keeping track of amortised time
> complexity of non-strict programs. This library used a Thunk monad
> annotated with an upper bound on the number of steps needed to compute
> the thunk to weak head normal form (more or less; see the paper for
> details):
>
>     Lightweight Semiformal Time Complexity Analysis for Purely Functional
>       Data Structures
>     http://www.cse.chalmers.se/~nad/publications/danielsson-popl2008.html
>