消除类型级别的Maybe

Question

是否有任何方法可以在类型级别解开Maybe monad内部的值？例如，如何为具有tail变体的Vec定义类型安全的pred：

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

Answer 1

第一次尝试

我们可以为此定义数据类型：

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

即mx >>=ᵗ B是B x（其中just x ≡ mx）或“无”。然后，我们可以为tail定义Vec，如下所示：

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

在[]情况下，n为0，因此pred n降为nothing，并且nothingᵗ是我们唯一可以返回的值。

在x ∷ xs情况下，n为suc n'，因此pred n简化为just n'，我们需要将justᵗ构造函数应用于类型为Vec A n'的值，即xs。

我们可以定义from-justᵗ就像在from-just中定义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

然后，实际的tail功能是

tail : ∀ {n α} {A : Set α} -> (xs : Vec A n) -> From-justᵗ (tailᵗ xs)
tail = from-justᵗ ∘ tailᵗ

一些测试：

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

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

但是我们希望能够映射类型为mx >>=ᵗ B的值，所以让我们尝试为此定义一个函数：

_<$>ᵗ_ : ∀ {α β γ} {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ᵗ = {!!}

如何填充孔？在第一个孔中，我们有

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

等式just x ≡ mx应该成立，但我们无法证明这一点，因此无法将yᵗ : mx >>=ᵗ B转换为y : B x以使用C y填充孔成为可能。相反，我们可以通过在_<$>ᵗ_上进行模式匹配来定义yᵗ的类型，但是我们无法使用相同的_<$>ᵗ_映射已经映射的内容。

实际解决方案

因此，我们需要在mx ≡ just x中建立mx >>=ᵗ λ x -> e的属性。我们可以为_>>=ᵗ_分配这种类型的签名：

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

但是我们真正关心的是，在mx情况下just是justᵗ-从此我们可以根据需要恢复x部分。因此定义：

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

我不使用标准库中的Is-just，因为它不计算-在这种情况下至关重要。

但是此定义存在问题：

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

洞中的上下文看起来像

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

n'不是数字。可以通过n上的模式匹配将其转换为数字，但这太冗长和丑陋。相反，我们可以将此模式匹配合并到辅助功能中：

! : ∀ {α β} {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}

!由作用于A的函数构成，作用于Is-just mx的函数。 {_ : mx ≡ just x}部分不是必需的，但是具有此属性可能很有用。

tailᵗ的定义是

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

from-justᵗ与以前几乎相同：

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

并且tail相同：

tail : ∀ {α n} {A : Set α} -> (xs : Vec A n) -> From-justᵗ (tailᵗ xs)
tail = from-justᵗ ∘ tailᵗ

测试通过：

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

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

但是现在我们也可以定义类似fmap的函数：

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)

即具有imx : Is-just mx，我们可以使用mx >>=ᵗ B功能将B imx还原为runᵗ。将C应用于结果将提供所需的类型签名。

注意，在just x情况下>

runᵗ {mx = just  x} (justᵗ y) _  = y
y : B tt，而Goal : B imx。我们可以将B tt视为B imx，因为⊤的所有居民都无法区分，如[]所见
indistinguishable : ∀ (x y : ⊤) -> x ≡ y
indistinguishable _ _ = refl
这是由于⊤数据类型的eta规则。
这里是最终测试：

test : from-justᵗ ((0 ∷_) <$>ᵗ ((0 ∷_) <$>ᵗ tailᵗ (1 ∷ 2 ∷ 3 ∷ []))) ≡ 0 ∷ 0 ∷ 2 ∷ 3 ∷ []
test = refl
备注
我们还可以引入一些语法糖：

¡ : ∀ {α β} {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})
并在不需要统一时使用它，如本示例中所示：
pred-replicate : ∀ {n} -> pred n >>=ᵗ ! λ pn -> Vec ℕ pn
pred-replicate = ¡ λ pn -> replicate {n = pn} 0
[!或者可以定义为
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}
因为B现在是Is-just mx -> Set β类型，而不是∀ {mx} -> Is-just mx -> Set β，所以此定义更易于推理，但是由于is-just中存在模式匹配，因此该定义可能会破坏一些beta相等性。
[¡'也可以以此方式定义

¡' : ∀ {α β} {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})
但是此定义破坏了所需的beta等同性：
pred-replicate' : ∀ {n} -> pred n >>=ᵗ ! λ pn -> Vec ℕ pn
pred-replicate' = ¡' λ pn {_} -> {!!}
孔的类型是! (λ pn₁ {._} → Vec ℕ pn₁) (is-just p)而不是Vec ℕ pn。
code。

---

EDIT

原来，该版本不是很有用。我现在正在使用this：

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