Устранение Возможно на уровне типа

Question

Есть ли способ развернуть значение, которое находится внутри Maybe монада, на уровне типа? Например, как определить безопасный тип 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это определение, вероятно, может нарушить некоторые бета-равенства.

¡' можно определить таким же образом

¡' : ∀ {α β} {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})

но это определение нарушает необходимые бета-равенства:

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