agda - 在类型级别消除可能

Question

有没有办法解开一个值，它在 Maybe 里面monad，在类型级别？例如，如何定义类型安全 tail为 Vec s 具有 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

IE。 mx >>=ᵗ B要么是 B x , 其中 just x ≡ mx ， 或者什么都没有”。然后我们可以定义 tail为 Vec s 如下:

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