消除类型级别的Maybe

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

即mx >>=? B是B x,在哪里just x ? mx,或"没有".然后我们可以tail为Vecs 定义如下:

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.

该代码.

编辑原来这个版本不是很实用.我现在正在使用它:

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