0 | module Data.Late
 1 |
 2 | %default total
 3 |
 4 | ------------------------------------------------------------------------
 5 | -- Type
 6 |
 7 | public export
 8 | data Late : Type -> Type where
 9 |   Now : a -> Late a
10 |   Later : Inf (Late a) -> Late a
11 |
12 | ------------------------------------------------------------------------
13 | -- Creating late values
14 |
15 | ||| Never return
16 | public export
17 | never : Late a
18 | never = Later never
19 |
20 | ||| Run a small state machine until it reaches a final state and yields a value.
21 | public export
22 | unfold : (seed -> Either seed value) -> seed -> Late value
23 | unfold f s = case f s of
24 |   Left s' => Later (unfold f s')
25 |   Right v => Now v
26 |
27 | ||| It's easier to define map and (<*>) in terms of bind so let's start
28 | ||| by defining it.
29 | public export
30 | bind : Late a -> (a -> Late b) -> Late b
31 | bind (Now v) f = f v
32 | bind (Later d) f = Later (bind d f)
33 |
34 | ------------------------------------------------------------------------
35 | -- Inspecting late values
36 |
37 | ||| Check whether we already have a value.
38 | public export
39 | isNow : Late a -> Maybe a
40 | isNow (Now v) = Just v
41 | isNow (Later d) = Nothing
42 |
43 | ||| Wait for one tick, hoping to get a value.
44 | public export
45 | wait : Late a -> Late a
46 | wait (Later d) = d
47 | wait d = d
48 |
49 | ||| Wait for a set number of ticks.
50 | public export
51 | engine : Nat -> Late a -> Late a
52 | engine Z = id
53 | engine (S n) = engine n . wait
54 |
55 | ||| Wait for a set number of ticks, hoping to get a value.
56 | public export
57 | petrol : Nat -> Late a -> Maybe a
58 | petrol n = isNow . engine n
59 |
60 | ||| Accelerate makes things happen twice as fast.
61 | public export
62 | accelerate : Late a -> Late a
63 | accelerate (Later (Later d)) = Later (accelerate d)
64 | accelerate (Later (Now v)) = Now v
65 | accelerate d = d
66 |
67 | ------------------------------------------------------------------------
68 | -- Instances
69 |
70 | public export
71 | Functor Late where
72 |   map f d = bind d (Now . f)
73 |
74 | public export
75 | Applicative Late where
76 |   pure = Now
77 |   df <*> dx = bind df (\ f => map (f $) dx)
78 |
79 | public export
80 | Monad Late where
81 |   (>>=) = bind
82 |