Завершение проверки замены через (монадическое) соединение и fmap
Я использую типоразмеры и имею функцию подстановки для типизированных терминов, которая проверяет завершение, если я даю определение напрямую, а не если я делаю его через (монадное) соединение и fmap.
{-# OPTIONS --sized-types #-}
module Subst where
open import Size
Чтобы показать проблему, достаточно иметь единицу и суммы. У меня есть типы данных Trie а также Term, и я использую попытки с codomain Term внутри Term, как часть формы исключения для сумм.
data Type : Set where
: Type
_+_ : Type → Type → Type
postulate Cxt : Set → Set
-- Every value in the trie is typed in a context obtained by extending Γ.
data Trie (A : Cxt Type → Set) : {ι : Size} → Type → Cxt Type → Set where
〈〉 : ∀ {ι Γ} → A Γ → Trie A {↑ ι} Γ
〔_,_〕 : ∀ {ι τ₁ τ₂ Γ} →
Trie A {ι} τ₁ Γ → Trie A {ι} τ₂ Γ → Trie A {↑ ι} (τ₁ + τ₂) Γ
-- The elimination form for + types is a trie whose values are terms.
data Term (A : Cxt Type → Type → Set) : {ι : Size} →
Cxt Type → Type → Set where
var : ∀ {ι Γ τ} → A Γ τ → Term A {↑ ι} Γ τ
inl : ∀ {ι Γ τ₁ τ₂} → Term A {ι} Γ τ₁ → Term A {↑ ι} Γ (τ₁ + τ₂)
match_as_ : ∀ {ι Γ τ τ′} → Term A {ι} Γ τ →
Trie (λ Γ → Term A {ι} Γ τ′) {ι} τ Γ → Term A {↑ ι} Γ τ′
Теперь, если я определю замену в терминах напрямую (взаимно с заменой в попытки с кодоменом Term), тогда определение прекращается проверками даже без индексов размеров.
-- Define substitution directly.
_*_ : ∀ {A Γ Γ′ τ} → (∀ {τ} → A Γ τ → Term A Γ′ τ) → Term A Γ τ → Term A Γ′ τ
_*ᵀ_ : ∀ {A Γ Γ′ τ τ′} → (∀ {τ} → A Γ τ → Term A Γ′ τ) →
Trie (λ Γ → Term A Γ τ) τ′ Γ → Trie (λ Γ → Term A Γ τ) τ′ Γ′
θ * var x = θ x
θ * inl e = inl (θ * e)
θ * (match e as κ) = match (θ * e) as (θ *ᵀ κ)
θ *ᵀ 〈〉 x = 〈〉 (θ * x)
θ *ᵀ 〔 κ₁ , κ₂ 〕 = 〔 θ *ᵀ κ₁ , θ *ᵀ κ₂ 〕
Тем не мение, Trie а также Term являются функторами, поэтому естественно хотеть определить замену с точки зрения <$> (fmap) и joinгде последний сворачивает термин сроков в термин. Обратите внимание, что <$> и его аналог для попыток - сохранение размера, и нам действительно нужно использовать индексы размера, которые отражают это, чтобы Agda была довольна тем, что она завершается.
-- Size-preserving fmap.
_<$>ᵀ_ : ∀ {ι τ Γ Γ′} {A B : Cxt Type → Set } →
(A Γ → B Γ′) → Trie A {ι} τ Γ → Trie B {ι} τ Γ′
f <$>ᵀ (〈〉 x) = 〈〉 (f x)
f <$>ᵀ 〔 σ₁ , σ₂ 〕 = 〔 f <$>ᵀ σ₁ , f <$>ᵀ σ₂ 〕
_<$>_ : ∀ {ι A B Γ Γ′ τ} →
(∀ {τ} → A Γ τ → B Γ′ τ) → Term A {ι} Γ τ → Term B {ι} Γ′ τ
f <$> var x = var (f x)
f <$> inl e = inl (f <$> e)
f <$> match e as κ = match f <$> e as ((λ e → f <$> e) <$>ᵀ κ)
-- Monadic multiplication.
join : ∀ {A Γ τ} → Term (Term A) Γ τ → Term A Γ τ
join (var e) = e
join (inl e) = inl (join e)
join (match e as κ) = match join e as (join <$>ᵀ κ)
-- Now substitution is easily defined in terms of join and fmap.
_*′_ : ∀ {A Γ Γ′ τ} → (∀ {τ} → A Γ τ → Term A Γ′ τ) → Term A Γ τ → Term A Γ′ τ
θ *′ e = join (θ <$> e)
к несчастью join не завершает проверку, и я не уверен, что можно использовать индексы размера, чтобы убедить Агду в этом. Интуитивно понятно, что если у вас есть дерево с максимальной глубиной ι и вы заменяете его листья деревьями с максимальной глубиной ι', вы получаете дерево с максимальной глубиной (ι + ι'). Но я не думаю, что такие вещи можно установить с помощью типоразмеров, и поможет ли это, если вы сможете. Обратите внимание, что без взаимной рекурсии в попытки через join <$>ᵀ, завершение функции проверяет нормально.
Есть ли способ получить эту взаимно рекурсивную версию join проверка завершения, или я застрял с написанием замены явно?