Add partiality/delay monad

[eayus]

An implementation of the partiality monad. Because the name Delay is taken already I called it Partial, otherwise everything uses standard names.

I'm not sure where this should go to be honest - it is very general and there's not much room for alternative implementations so I've put it in base for now, but contrib might be more appropriate.

[gallais]

You're missing some public exports for the lib to be useful.
Other than that 👍

[eayus]

Ok I've done that and added some stuff for proving that a partial computation is actually total.

I've made a mess of these commits as I keep forgetting about the linter, but I think it's possible for you to squash them before merging?

[buzden]

This proof argument can be an auto-implicit argument with quantity 0, this simplifies function implementation, its usage, and actual runtime.

[eayus]

I agree it should be erased, but I'm not sure that making it an auto-implicit is the right choice as proving totality will often require case splitting on arguments (which the proof search won't do automatically I think).

[buzden]

Are you talking about implementation or calling to this function? I checked, and I agree that you'll need to pass the argument manually, but you can do this easily, say:

runPartial : (x : Partial a) -> (0 _ : Total x) => a
runPartial (Now v) = v
runPartial (Later x) @{TLater xx} = runPartial x @{xx}

But, if you consider this ugly -- then ok, leave it explicit. Anyway, I think, that callers of this function would like to pass this argument automatically -- do you agree?

[eayus]

I think that callers would still like to pass it explicitly most of the time, as most of the time you are proving totality for a function rather than a concrete value.

Here is an example of how I imagine this type being used. The function isn't actually useful but is the simplest example I could come up with:

toZeroP : Nat -> Partial Nat
toZeroP n = if n == 0 then pure n else Later $ toZeroP (pred n)

totality : (n : Nat) -> Total (toZeroP n)
totality Z = TNow
totality (S n) = TLater (totality n)

toZeroT : Nat -> Nat
toZeroT n = runPartial (toZeroP n) (totality n)

If we use an auto implicit then it will fail to find a solution as the totality proof is by induction.

[gallais]

I would probably write runPartial : {x : Partial a} -> (0 _ : Total x) -> a instead tbh. x is uniquely determined from Total x. :)

[buzden]

In base such proofs usually have name Is<Property>, like isJust for Maybe and IsYes for Dec. Maybe, this one should be names IsTotal to be coherent with the others

[eayus]

That naming pattern seems to be primarily used for proofs that a data type is a specific constructor, whereas I would argue that this type is more similar to something like Elem. (Though I don't really mind what it is named)

[gallais]

If you are looking for additional useful functions: http://agda.github.io/agda-stdlib/v2.0/Codata.Sized.Delay.html

[gallais]

I would probably write runPartial : {x : Partial a} -> (0 _ : Total x) -> a instead tbh. x is uniquely determined from Total x. :)

[eayus]

The main issue with this implementation atm is that chaining things together using >>= confuses the termination checker, which agda solves using sized types.

For example, defining never with either of the following equivalent definitions will fail termination checking.

undefined : Partial a
undefined = do
    x <- Later undefined
    pure x

undefined : Partial a
undefined = Later $ do
    x <- undefined
    pure x

I'm wondering if it's possible to index by a natural number or something to convince the type checker?

Also it doesn't help I don't fully understand the exact rules Idris uses to check these guarded coinductive functions.

[gallais]

https://arxiv.org/abs/1012.4898 should give you a few pointers as to what guardedness is and how to beat the checker
when defining something like _>>=_

[gallais]

Let's merge as is. We can always have a separate PR if you decide to implement a DSL for guarded corecursion.