agda - Eliminating a Maybe at the type level

Question

Is there any way to unwrap a value, which is inside the Maybe monad, at the type level? For example, how to define type-safe tail for Vecs having this variant of pred:

pred : ? -> Maybe ?
pred  0      = nothing
pred (suc n) = just n

? Something like

tail : ? {n α} {A : Set α} -> Vec A n ->
  if isJust (pred n) then Vec A (from-just (pred n)) else ?

This example is totally artificial, but it's not always possible to get rid of some precondition, so you can write a correct by construction definition like the tail function from the standard library:

tail : ? {a n} {A : Set a} → Vec A (1 + n) → Vec A n
tail (x ∷ xs) = xs

Answer 1

A first attempt

We can define a data type for that:

data _>>=?_ {α β} {A : Set α} : (mx : Maybe A) -> (A -> Set β) -> Set (α ? β) where
  nothing? : ? {B}   ->        nothing >>=? B
  just?    : ? {B x} -> B x -> just x  >>=? B

I.e. mx >>=? B is either B x, where just x ≡ mx, or "nothing". We then can define tail for Vecs as follows:

pred : ? -> Maybe ?
pred  0      = nothing
pred (suc n) = just n

tail? : ? {α n} {A : Set α} -> Vec A n -> pred n >>=? Vec A 
tail?  []      = nothing?
tail? (x ∷ xs) = just? xs

In the [] case n is 0, so pred n reduces to nothing, and nothing? is the only value we can return.

In the x ∷ xs case n is suc n', so pred n reduces to just n', and we need to apply the just? constructor to a value of type Vec A n', i.e. xs.

We can define from-just? pretty much like from-just is defined in Data.Maybe.Base:

From-just? : ? {α β} {A : Set α} {B : A -> Set β} {mx : Maybe A} -> mx >>=? B -> Set β
From-just?  nothing?         = Lift ?
From-just? (just? {B} {x} y) = B x

from-just? : ? {α β} {A : Set α} {B : A -> Set β} {mx : Maybe A} -> (y? : mx >>=? B) -> From-just? y?
from-just?  nothing? = _
from-just? (just? y) = y

Then the actual tail function is

tail : ? {n α} {A : Set α} -> (xs : Vec A n) -> From-just? (tail? xs)
tail = from-just? ° tail?

Some tests:

test-nil : tail (Vec ? 0 ? []) ≡ lift tt
test-nil = refl

test-cons : tail (1 ∷ 2 ∷ 3 ∷ []) ≡ 2 ∷ 3 ∷ []
test-cons = refl

However we want to be able to map values of type mx >>=? B, so let's try to define a function for that:

_<$>?_ : ? {α β γ} {A : Set α} {B : A -> Set β} {C : ? {x} -> B x -> Set γ} {mx : Maybe A}
       -> (? {x} -> (y : B x) -> C y) -> (y? : mx >>=? B) -> mx >>=? λ x -> {!!}
g <$>? y? = {!!}

How to fill the holes? In the first hole we have

Goal: Set (_β_86 y?)
————————————————————————————————————————————————————————————
x  : A
y? : mx >>=? B
mx : Maybe A
C  : {x = x? : A} → B x? → Set γ
B  : A → Set β
A  : Set α

The equation just x ≡ mx should hold, but we can't prove that, so there is no way to turn y? : mx >>=? B into y : B x to make it possible to fill the hole with C y. We could instead define the type of _<$>?_ by pattern matching on y?, but then we couldn't map something, that was already mapped, using the same _<$>?_.

Actual solution

So we need to establish the property, that mx ≡ just x in mx >>=? λ x -> e. We can assign _>>=?_ this type signature:

data _>>=?_ {α β} {A : Set α} : (mx : Maybe A) -> (? {x} -> mx ≡ just x -> Set β) -> Set (α ? β)

but all we actually care is that mx is just in the just? case — from this we can recover the x part, if needed. Hence the definition:

Is-just : ? {α} {A : Set α} -> Maybe A -> Set
Is-just = T ° isJust

data _>>=?_ {α β} {A : Set α} : (mx : Maybe A) -> (Is-just mx -> Set β) -> Set (α ? β) where
  nothing? : ? {B}   ->        nothing >>=? B
  just?    : ? {B x} -> B _ -> just x  >>=? B

I don't use Is-just from the standard library, because it doesn't compute — it's crucial in this case.

But there is a problem with this definition:

tail? : ? {α n} {A : Set α} -> Vec A n -> pred n >>=? λ n' -> {!!}

the context in the hole looks like

Goal: Set _230
————————————————————————————————————————————————————————————
n' : Is-just (pred n)
A  : Set α
n  : ?

n' is not a number. It's possible to convert it to a number by pattern matching on n, but this is too verbose and ugly. Instead we can incorporate this pattern matching in an auxiliary function:

! : ? {α β} {A : Set α} {B : ? {mx} -> Is-just mx -> Set β} {mx : Maybe A}
  -> (? x {_ : mx ≡ just x} -> B {just x} _) -> (imx : Is-just mx) -> B imx
! {mx = nothing} f ()
! {mx = just x } f _  = f x {refl}

! makes from a function, that acts on A, a function, that acts on Is-just mx. The {_ : mx ≡ just x} part is not necessary, but it can be useful to have this property.

The definition of tail? then is

tail? : ? {α n} {A : Set α} -> Vec A n -> pred n >>=? ! λ pn -> Vec A pn
tail?  []      = nothing?
tail? (x ∷ xs) = just? xs

from-just? is almost the same as before:

From-just? : ? {α β} {A : Set α} {mx : Maybe A} {B : Is-just mx -> Set β}
           -> mx >>=? B -> Set β
From-just?  nothing?     = Lift ?
From-just? (just? {B} y) = B _

from-just? : ? {α β} {A : Set α} {mx : Maybe A} {B : Is-just mx -> Set β}
           -> (y? : mx >>=? B) -> From-just? y?
from-just?  nothing? = _
from-just? (just? y) = y

And tail is the same:

tail : ? {α n} {A : Set α} -> (xs : Vec A n) -> From-just? (tail? xs)
tail = from-just? ° tail?

Tests pass:

test-nil : tail (Vec ? 0 ? []) ≡ lift tt
test-nil = refl

test-cons : tail (1 ∷ 2 ∷ 3 ∷ []) ≡ 2 ∷ 3 ∷ []
test-cons = refl

However now we can also define a fmap-like function:

run? : ? {α β} {A : Set α} {mx : Maybe A} {B : Is-just mx -> Set β}
     -> mx >>=? B -> (imx : Is-just mx) -> B imx
run? {mx = nothing}  _        ()
run? {mx = just  x} (just? y) _  = y

_<$>?_ : ? {α β γ} {A : Set α} {mx : Maybe A} {B : Is-just mx -> Set β} {C : ? {x} -> B x -> Set γ}
       -> (? {x} -> (y : B x) -> C y) -> (y? : mx >>=? B) -> mx >>=? C ° run? y?
g <$>? nothing? = nothing?
g <$>? just? y  = just? (g y)

I.e. having imx : Is-just mx we can reduce mx >>=? B to B imx using the run? function. Applying C to the result gives the desired type signature.

Note that in the just x case

run? {mx = just  x} (just? y) _  = y

y : B tt, while Goal : B imx. We can treat B tt as B imx because all inhabitants of ? are indistinguishable, as witnessed by

indistinguishable : ? (x y : ?) -> x ≡ y
indistinguishable _ _ = refl

This is due to the eta rule for the ? data type.

Here is the final test:

test : from-just? ((0 ∷_) <$>? ((0 ∷_) <$>? tail? (1 ∷ 2 ∷ 3 ∷ []))) ≡ 0 ∷ 0 ∷ 2 ∷ 3 ∷ []
test = refl

Remarks

We can also introduce some syntactic sugar:

? : ? {α β} {A : Set α} {B : A -> Set β} {mx : Maybe A}
  -> (? x {_ : mx ≡ just x} -> B x) -> mx >>=? ! λ x -> B x
? {mx = nothing} f = nothing?
? {mx = just  x} f = just? (f x {refl})

And use it when unification is not needed, like in this example:

pred-replicate : ? {n} -> pred n >>=? ! λ pn -> Vec ? pn
pred-replicate = ? λ pn -> replicate {n = pn} 0

! alternatively can be defined as

is-just : ? {α} {A : Set α} {mx} {x : A} -> mx ≡ just x -> Is-just mx
is-just refl = _

!' : ? {α β} {A : Set α} {mx : Maybe A} {B : Is-just mx -> Set β}
   -> (? x {p : mx ≡ just x} -> B (is-just p)) -> (imx : Is-just mx) -> B imx
!' {mx = nothing} f ()
!' {mx = just x } f _  = f x {refl}

Since B now is of type Is-just mx -> Set β instead of ? {mx} -> Is-just mx -> Set β, this definition is more inference-friendly, but since there is pattern matching in is-just, this definition can probably break some beta equalities.

?' could be defined in this manner as well

?' : ? {α β} {A : Set α} {mx : Maybe A} {B : Is-just mx -> Set β}
   -> (? x {p : mx ≡ just x} -> B (is-just p)) -> mx >>=? B
?' {mx = nothing} f = nothing?
?' {mx = just  x} f = just? (f x {refl})

but this definition breaks needed beta equalities:

pred-replicate' : ? {n} -> pred n >>=? ! λ pn -> Vec ? pn
pred-replicate' = ?' λ pn {_} -> {!!}

The type of the hole is ! (λ pn? {._} → Vec ? pn?) (is-just p) instead of Vec ? pn.

---

The code.

---

EDIT It turned out that this version is not very usable. I'm using this now:

data _>>=?_ {α β} {A : Set α} : (mx : Maybe A) -> (? x -> mx ≡ just x -> Set β) -> Set β where