Первая попытка
Мы можем определить тип данных для этого:
data _>>=ᵗ_ {α β} {A : Set α} : (mx : Maybe A) -> (A -> Set β) -> Set (α ⊔ β) where
nothingᵗ : ∀ {B} -> nothing >>=ᵗ B
justᵗ : ∀ {B x} -> B x -> just x >>=ᵗ B
I.e. 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
Однако мы хотим быть abl е для отображения значений типа 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
Однако теперь мы также можем определить БПМЖ-как функцию:
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
Это связано с правилом эты для типа ⊤ данных.
Вот окончательный тест:
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.
code.
EDIT Оказалось, что эта версия не очень годны к употреблению. Я использую this сейчас:
data _>>=ᵀ_ {α β} {A : Set α} : (mx : Maybe A) -> (∀ x -> mx ≡ just x -> Set β) -> Set β where