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

[Nils Anders Danielsson]

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

-- 
/NAD