有没有办法在类型级别解开 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
最佳答案
第一次尝试
我们可以为此定义一个数据类型:
data _>>=ᵗ_ {α β} {A : Set α} : (mx : Maybe A) -> (A -> Set β) -> Set (α ⊔ β) where
nothingᵗ : ∀ {B} -> nothing >>=ᵗ B
justᵗ : ∀ {B x} -> B x -> just x >>=ᵗ B
IE。
mx >>=ᵗ B 要么是 B x ，其中 just x ≡ mx 要么是“nothing”。然后我们可以为 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)
IE。有了
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 。
编辑 原来这个版本不太好用。我现在正在使用 this:
data _>>=ᵀ_ {α β} {A : Set α} : (mx : Maybe A) -> (∀ x -> mx ≡ just x -> Set β) -> Set β where
关于agda - 消除类型级别的 Maybe，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/31105947/