在类型级别消除 Maybe
Eliminating a Maybe at the type level
有没有什么方法可以在类型级别解包 Maybe monad 中的值？例如，如何为具有 pred:
变体的 Vec 定义类型安全的 tail
pred : ℕ -> Maybe ℕ
pred 0 = nothing
pred (suc n) = just n
？像
tail : ∀ {n α} {A : Set α} -> Vec A n ->
if isJust (pred n) then Vec A (from-just (pred n)) else ⊤
这个例子完全是人为的，但并不总是可以摆脱一些先决条件，所以你可以通过构造定义编写一个正确的，比如标准库中的 tail 函数：
tail : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
tail (x ∷ xs) = xs
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 属性, 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 属性.
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
有没有什么方法可以在类型级别解包 Maybe monad 中的值？例如，如何为具有 pred:
Vec 定义类型安全的 tail
pred : ℕ -> Maybe ℕ
pred 0 = nothing
pred (suc n) = just n
？像
tail : ∀ {n α} {A : Set α} -> Vec A n ->
if isJust (pred n) then Vec A (from-just (pred n)) else ⊤
这个例子完全是人为的，但并不总是可以摆脱一些先决条件，所以你可以通过构造定义编写一个正确的，比如标准库中的 tail 函数：
tail : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
tail (x ∷ xs) = xs
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 属性, 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 属性.
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