0 | ||| Module partially based on McBride's paper:
  1 | ||| Turing-Completeness Totally Free
  2 | |||
  3 | ||| It gives us a type to describe computation using general recursion
  4 | ||| and functions to run these computations for a while or to completion
  5 | ||| if we are able to prove them total.
  6 | |||
  7 | ||| The content of the Erased section is new. Instead of producing the
  8 | ||| domain/evaluation pair by computing a Dybjer-Setzer code we build a
  9 | ||| specialised structure that allows us to make the domain proof runtime
 10 | ||| irrelevant.
 11 |
 12 | module Data.Recursion.Free
 13 |
 14 | import Data.Late
 15 | import Data.InductionRecursion.DybjerSetzer
 16 |
 17 | %default total
 18 |
 19 | ------------------------------------------------------------------------
 20 | -- Type
 21 |
 22 | ||| Syntax for a program using general recursion
 23 | public export
 24 | data General : (a : Type) -> (b : a -> Type) -> (x : Type) -> Type where
 25 |   ||| We can return a value without performing any recursive call.
 26 |   Tell : x -> General a b x
 27 |   ||| Or we can pick an input and ask an oracle to give us a return value
 28 |   ||| for it. The second argument is a continuation explaining what we want
 29 |   ||| to do with the returned value.
 30 |   Ask  : (i : a) -> (b i -> General a b x) -> General a b x
 31 |
 32 | ||| Type of functions using general recursion
 33 | public export
 34 | PiG : (a : Type) -> (b : a -> Type) -> Type
 35 | PiG a b = (i : a) -> General a b (b i)
 36 |
 37 | ||| Recursor for General
 38 | public export
 39 | fold : (x -> y) -> ((i : a) -> (b i -> y) -> y) -> General a b x -> y
 40 | fold pure ask (Tell x) = pure x
 41 | fold pure ask (Ask i k) = ask i (\ o => fold pure ask (k o))
 42 |
 43 | ------------------------------------------------------------------------
 44 | -- Basic functions
 45 |
 46 | ||| Perform a recursive call and return the value provided by the oracle.
 47 | public export
 48 | call : PiG a b
 49 | call i = Ask i Tell
 50 |
 51 | ||| Monadic bind (defined outside of the interface to be able to use it for
 52 | ||| map and (<*>)).
 53 | public export
 54 | bind : General a b x -> (x -> General a b y) -> General a b y
 55 | bind m f = fold f Ask m
 56 |
 57 | ||| Given a monadic oracle we can give a monad morphism interpreting a
 58 | ||| function using general recursion as a monadic process.
 59 | public export
 60 | monadMorphism : Monad m => (t : (i : a) -> m (b i)) -> General a b x -> m x
 61 | monadMorphism t = fold pure (\ i => (t i >>=))
 62 |
 63 | ------------------------------------------------------------------------
 64 | -- Instances
 65 |
 66 | public export
 67 | Functor (General a b) where
 68 |   map f = fold (Tell . f) Ask
 69 |
 70 | public export
 71 | Applicative (General a b) where
 72 |   pure = Tell
 73 |   gf <*> gv = bind gf (\ f => map (f $) gv)
 74 |
 75 | public export
 76 | Monad (General a b) where
 77 |   (>>=) = bind
 78 |
 79 | ------------------------------------------------------------------------
 80 | -- Fuel-based (partial) evaluation
 81 |
 82 | ||| Check whether we are ready to return a value
 83 | public export
 84 | already : General a b x -> Maybe x
 85 | already = monadMorphism (\ i => Nothing)
 86 |
 87 | ||| Use a function using general recursion to expand all of the oracle calls.
 88 | public export
 89 | expand : PiG a b -> General a b x -> General a b x
 90 | expand f = monadMorphism f
 91 |
 92 | ||| Recursively call expand a set number of times.
 93 | public export
 94 | engine : PiG a b -> Nat -> General a b x -> General a b x
 95 | engine f Z     = id
 96 | engine f (S n) = engine f n . expand f
 97 |
 98 | ||| Check whether recursively calling expand a set number of times is enough
 99 | ||| to produce a value.
100 | public export
101 | petrol : PiG a b -> Nat -> (i : a) -> Maybe (b i)
102 | petrol f n i = already $ engine f n $ f i
103 |
104 | ------------------------------------------------------------------------
105 | -- Late-based evaluation
106 |
107 | ||| Rely on an oracle using general recursion to convert a function using
108 | ||| general recursion into a process returning a value in the (distant) future.
109 | public export
110 | late : PiG a b -> General a b x -> Late x
111 | late f = monadMorphism (\ i => Later (assert_total $ late f (f i)))
112 |
113 | ||| Interpret a function using general recursion as a process returning
114 | ||| a value in the (distant) future.
115 | public export
116 | lazy : PiG a b -> (i : a) -> Late (b i)
117 | lazy f i = late f (f i)
118 |
119 | ------------------------------------------------------------------------
120 | -- Domain as a Dybjer-Setzer code and total evaluation function
121 |
122 | namespace DybjerSetzer
123 |
124 |   ||| Compute, as a Dybjer-Setzer code for an inductive-recursive type, the domain
125 |   ||| of a function defined by general recursion.
126 |   public export
127 |   Domain : PiG a b -> (i : a) -> Code b (b i)
128 |   Domain f i = monadMorphism ask (f i) where
129 |
130 |     ask : (i : a) -> Code b (b i)
131 |     ask i = Branch () (const i) $ \ t => Yield (t ())
132 |
133 |   ||| If a given input is in the domain of the function then we may evaluate
134 |   ||| it fully on that input and obtain a pure return value.
135 |   public export
136 |   evaluate : (f : PiG a b) -> (i : a) -> Mu (Domain f) i -> b i
137 |   evaluate f i inDom = Decode inDom
138 |
139 |   ||| If every input value is in the domain then the function is total.
140 |   public export
141 |   totally : (f : PiG a b) -> ((i : a) -> Mu (Domain f) i) ->
142 |             (i : a) -> b i
143 |   totally f allInDomain i = evaluate f i (allInDomain i)
144 |
145 | ------------------------------------------------------------------------
146 | -- Runtime irrelevant domain and total evaluation function
147 |
148 | namespace Erased
149 |
150 |   ------------------------------------------------------------------------
151 |   -- Domain and evaluation functions
152 |
153 |   ||| What it means to describe a terminating computation
154 |   ||| @ f is the function used to answer questions put to the oracle
155 |   ||| @ d is the description of the computation
156 |   public export
157 |   data Layer : (f : PiG a b) -> (d : General a b (b i)) -> Type
158 |
159 |   ||| The domain of a function (i.e. the set of inputs for which it terminates)
160 |   ||| as a predicate on inputs
161 |   ||| @ f is the function whose domain is being described
162 |   ||| @ i is the input that is purported to be in the domain
163 |   Domain : (f : PiG a b) -> (i : a) -> Type
164 |
165 |   ||| Fully evaluate a computation known to be terminating.
166 |   ||| Because of the careful design of the inductive family Layer, we can make
167 |   ||| the proof runtime irrelevant.
168 |   evaluateLayer : (f : PiG a b) -> (d : General a b (b i)) -> (0 _ : Layer f d) -> b i
169 |
170 |   ||| Fully evaluate a function call for an input known to be in its domain.
171 |   evaluate : (f : PiG a b) -> (i : a) -> (0 _ : Domain f i) -> b i
172 |
173 |   -- In a classic Dybjer-Setzer situation this is computed by induction over the
174 |   -- index of type `General a b (b i)` and the fixpoint called `Domain` is the
175 |   -- one thing defined as an inductive type.
176 |   -- Here we have to flip the script because Idris will only trust inductive data
177 |   -- as a legitimate source of termination metric for a recursive function. This
178 |   -- makes our definition of `evaluateLayer` obviously terminating.
179 |   data Layer : PiG a b -> General a b (b i) -> Type where
180 |     ||| A computation returning a value is trivially terminating
181 |     MkTell : {0 a : Type} -> {0 b : a -> Type} -> {0 f : PiG a b} -> {0 i : a} ->
182 |              (o : b i) -> Layer f (Tell o)
183 |
184 |     ||| Performing a call to the oracle is termnating if the input is in its
185 |     ||| domain and if the rest of the computation is also finite.
186 |     MkAsk  : {0 a : Type} -> {0 b : a -> Type} -> {0 f : PiG a b} -> {0 i : a} ->
187 |              (j : a) -> (jprf : Domain f j) ->
188 |              (k : b j -> General a b (b i)) -> Layer f (k (evaluate f j jprf)) ->
189 |              Layer f (Ask j k)
190 |
191 |   -- Domain is simply defined as the top layer leading to a terminating
192 |   -- computation with the function used as its own oracle.
193 |   Domain f i = Layer f (f i)
194 |
195 |   ||| A view that gives us a pattern-matching friendly presentation of the
196 |   ||| @ d computation known to be terminating
197 |   ||| @ l proof that it is
198 |   ||| This may seem like a useless definition but the function `view`
199 |   ||| demonstrates a very important use case: even if the proof is runtime
200 |   ||| irrelevant, we can manufacture a satisfying view of it.
201 |   data View : {d : General a b (b i)} -> (l : Layer f d) -> Type where
202 |     TView : {0 b : a -> Type} -> {0 f : PiG a b} -> (o : b i) -> View (MkTell {b} {f} o)
203 |     AView : {0 f : PiG a b} ->
204 |             (j : a) -> (0 jprf : Domain f j) ->
205 |             (k : b j -> General a b (b i)) -> (0 kprf : Layer f (k (evaluate f j jprf))) ->
206 |             View (MkAsk j jprf k kprf)
207 |
208 |   ||| Function computing the view by pattern-matching on the computation and
209 |   ||| inverting the proof. Note that the proof is runtime irrelevant even though
210 |   ||| the resulting view is not: this is possible because the relevant constructor
211 |   ||| is uniquely determined by the shape of `d`.
212 |   public export
213 |   view : (d : General a b (b i)) -> (0 l : Layer f d) -> View l
214 |   view (Tell o)  (MkTell o)            = TView o
215 |   view (Ask j k) (MkAsk j jprf k kprf) = AView j jprf k kprf
216 |
217 |   -- Just like `Domain` is defined in terms of `Layer`, the evaluation of a
218 |   -- function call for an input in its domain can be reduced to the evaluation
219 |   -- of a layer.
220 |   evaluate f i l = evaluateLayer f (f i) l
221 |
222 |   -- The view defined earlier allows us to pattern on the runtime irrelevant
223 |   -- proof that the layer describes a terminating computation and therefore
224 |   -- define `evaluateLayer` in a way that is purely structural.
225 |   -- This becomes obvious if one spells out the (forced) pattern corresponding
226 |   -- to `d` in each branch of the case.
227 |   evaluateLayer f d l = case view d l of
228 |     TView o => o
229 |     AView j jprf k kprf => evaluateLayer f (k (evaluate f j jprf)) kprf
230 |
231 |   ||| If a function's domain is total then it is a pure function.
232 |   public export
233 |   totally : (f : PiG a b) -> (0 _ : (i : a) -> Domain f i) ->
234 |             (i : a) -> b i
235 |   totally f dom i = evaluate f i (dom i)
236 |
237 |   ------------------------------------------------------------------------
238 |   -- Proofs
239 |
240 |   ||| Domain is a singleton type
241 |   export
242 |   irrelevantDomain : (f : PiG a b) -> (i : a) -> (p, q : Domain f i) -> p === q
243 |
244 |   ||| Layer is a singleton type
245 |   irrelevantLayer
246 |     : (f : PiG a b) -> (d : General a b (b i)) -> (l, m : Layer f d) -> l === m
247 |
248 |   irrelevantDomain f i p q = irrelevantLayer f (f i) p q
249 |
250 |   irrelevantLayer f (Tell o)
251 |     (MkTell o) (MkTell o) = Refl
252 |   irrelevantLayer f (Ask j k)
253 |     (MkAsk j jprf1 k kprf1) (MkAsk j jprf2 k kprf2)
254 |     with (irrelevantDomain f j jprf1 jprf2)
255 |       irrelevantLayer f (Ask j k)
256 |         (MkAsk j jprf k kprf1) (MkAsk j jprf k kprf2)
257 |         | Refl = cong (MkAsk j jprf k)
258 |                $ irrelevantLayer f (k (evaluate f j jprf)) kprf1 kprf2
259 |
260 |   ||| The result of `evaluateLayer` does not depend on the specific proof that
261 |   ||| `i` is in the domain of the layer of computation at hand.
262 |   export
263 |   evaluateLayerIrrelevance
264 |     : (f : PiG a b) -> (d : General a b (b i)) -> (0 p, q : Layer f d) ->
265 |       evaluateLayer f d p === evaluateLayer f d q
266 |   evaluateLayerIrrelevance f d p q
267 |     = rewrite irrelevantLayer f d p q in Refl
268 |
269 |   ||| The result of `evaluate` does not depend on the specific proof that `i`
270 |   ||| is in the domain of the function at hand.
271 |   export
272 |   evaluateIrrelevance
273 |     : (f : PiG a b) -> (i : a) -> (0 p, q : Domain f i) ->
274 |       evaluate f i p === evaluate f i q
275 |   evaluateIrrelevance f i p q
276 |     = evaluateLayerIrrelevance f (f i) p q
277 |
278 |   ||| The result computed by a total function is independent from the proof
279 |   ||| that it is total.
280 |   export
281 |   totallyIrrelevance
282 |     : (f : PiG a b) -> (0 p, q : (i : a) -> Domain f i) ->
283 |       (i : a) -> totally f p i === totally f q i
284 |   totallyIrrelevance f p q i = evaluateIrrelevance f i (p i) (q i)
285 |