0 | module Control.Monad.Partial
 1 |
 2 | import Data.Nat
 3 |
 4 | %default total
 5 |
 6 |
 7 | ||| Delay/partiality monad. Represents partial computations which may not
 8 | ||| terminate or cover all inputs. This can be preferable to defining a partial
 9 | ||| Idris function as it allows termination to be proven as an external proof.
10 | public export
11 | data Partial : Type -> Type where
12 |     Now : a -> Partial a
13 |     Later : Inf (Partial a) -> Partial a
14 |
15 |
16 | public export
17 | Functor Partial where
18 |     map f (Now x) = Now (f x)
19 |     map f (Later x) = Later (map f x)
20 |
21 |
22 | public export
23 | Applicative Partial where
24 |     pure = Now
25 |
26 |     Now f <*> x = map f x
27 |     Later f <*> x = Later (f <*> x)
28 |
29 |
30 | public export
31 | Monad Partial where
32 |     Now x >>= f = f x
33 |     Later x >>= f = Later (x >>= f)
34 |
35 |
36 | ||| A partial computation which never terminates (aka. undefined/bottom).
37 | public export
38 | never : Partial a
39 | never = Later never
40 |
41 |
42 | public export
43 | data Total : Partial a -> Type where
44 |     TNow : (x : a) -> Total (Now x)
45 |     TLater : Total (Force x) -> Total (Later x)
46 |
47 |
48 | ||| Extract the value from a partial computation if you have a proof it is
49 | ||| actually total.
50 | public export
51 | runPartial : {x : Partial a} -> (0 _ : Total x) -> a
52 | runPartial (TNow x) = x
53 | runPartial (TLater t) = runPartial t
54 |