- data Late : Type -> Type
- Totality: total
Constructors:
- Now : a -> Late a
- Later : Inf (Late a) -> Late a
- accelerate : Late a -> Late a
Accelerate makes things happen twice as fast.
Totality: total- bind : Late a -> (a -> Late b) -> Late b
It's easier to define map and (<*>) in terms of bind so let's start
by defining it.
Totality: total- engine : Nat -> Late a -> Late a
Wait for a set number of ticks.
Totality: total- isNow : Late a -> Maybe a
Check whether we already have a value.
Totality: total- petrol : Nat -> Late a -> Maybe a
Wait for a set number of ticks, hoping to get a value.
Totality: total- unfold : (seed -> Either seed value) -> seed -> Late value
Run a small state machine until it reaches a final state and yields a value.
Totality: total- wait : Late a -> Late a
Wait for one tick, hoping to get a value.
Totality: total