Сравнение шаблонов в теории наблюдательного типа

В конце раздела "5. Full OTT" В отношении теории типов наблюдений авторы показывают, как определять индексированные типы данных с коэрцибел-под-конструкторами в OTT, Идея состоит в том, чтобы превратить индексированные типы данных в параметры следующим образом:

data IFin : ℕ -> Set where
  zero : ∀ {n} -> IFin (suc n)
  suc  : ∀ {n} -> IFin n -> IFin (suc n)

data PFin (m : ℕ) : Set where
  zero : ∀ {n} -> suc n ≡ m -> PFin m
  suc  : ∀ {n} -> suc n ≡ m -> PFin n -> PFin m

Конор также упоминает этот метод в нижней части теории наблюдательного типа (доставка):

Исправить, конечно же, сделать то, что сделали люди GADT, и определить индуктивных семейств явно до пропозиционального равенства. И затем конечно, вы можете их транспортировать, с помощью транзитивности.

Однако проверка типа в Haskell знает о ограничениях равенства в области видимости и фактически использует их во время проверки типов. Например. мы можем написать

f :: a ~ b => a -> b
f x = x

Это не работает так в теории типов, так как недостаточно иметь доказательство a ~ b в области возможностей, чтобы иметь возможность переписать это уравнение: это доказательство также должно быть refl, поскольку в присутствии проверка типа ложных гипотез становится неразрешимой из-за проблем с завершением (что-то вроде this). Поэтому, когда совпадение шаблона на Fin m в Haskell m переписывается на suc n в каждой ветки, но этого не может быть в теории типов, вместо этого вы получите явное доказательство suc n ~ m. В OTT вообще невозможно сопоставить совпадение на доказательствах, поэтому вы не можете притворяться, что доказательство refl и не требует этого. Это возможно только для доказательства coerce или просто игнорировать его.

Это очень затрудняет запись всего, что связано с индексированными типами данных. Например. обычными тремя строками (включая сигнатуру типа) lookup для векторов становится этот зверь:

vlookupₑ : ∀ {n m a} {α : Level a} {A : Univ α} -> ⟦ n ≅ m ⇒ fin n ⇒ vec A m ⇒ A ⟧
vlookupₑ         p (fzeroₑ q)       (vconsₑ r x xs)      = x
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vconsₑ {m′} r x xs) =
  vlookupₑ (left (suc n′) {m} {suc m′} (trans (suc n′) {n} {m} q p) r) i xs
vlookupₑ {n} {m} p (fzeroₑ {n′} q)  (vnilₑ r)            =
  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vnilₑ r)            =
  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r

vlookup : ∀ {n a} {α : Level a} {A : Univ α} -> Fin n -> Vec A n -> ⟦ A ⟧
vlookup {n} = vlookupₑ (refl n)

Это может быть немного упрощено, так как если два элемента типа данных, которые имеют разрешимое равенство, наблюдаются равными, то они также равны в обычном интенсиональном смысле, а натуральные числа имеют разрешимое равенство, поэтому мы можем принуждать всех уравнения к их интенсиональным аналогам и шаблону соответствуют им, но это нарушит некоторые вычислительные свойства vlookup и в любом случае является подробным. Практически невозможно заниматься более сложными делами с индексами, решение которых невозможно решить.

Я правильно ли рассуждаю? Как должно выполняться сопоставление шаблонов в OTT? Если это действительно проблема, есть ли способы смягчить ее?

Ответ 1

Я предполагаю, что я поставлю этот. Я нахожу это странным вопросом, но это из-за моего собственного путешествия. Короткий ответ: не выполняйте сопоставление образцов в OTT или в любой теории типов ядер. Это не то же самое, что никогда не выполнять сопоставление шаблонов.

Длинный ответ - это в основном моя кандидатская диссертация.

В своей докторской диссертации я расскажу, как разрабатывать программы высокого уровня, написанные в стиле соответствия шаблонов, в теорию типа ядра, которая имеет только индукционные принципы для индуктивных типов данных и подходящее отношение к пропозициональному равенству. Разработка сопоставления шаблонов вводит пропозициональные уравнения по индексам типов данных, а затем решает их путем унификации. В то время я использовал интенсиональное равенство, но наблюдательное равенство дает вам хотя бы одну силу. То есть: моя технология для разработки сопоставления шаблонов (и, таким образом, сохранения ее из теории ядра), скрывающей все эквациональные свинарники, предшествует обновлению до наблюдательного равенства. Ужасный vlookup, который вы использовали для иллюстрации вашей точки, может соответствовать выходному процессу разработки, но входной сигнал не должен быть таким уж плохим. Хорошее определение

vlookup : Fin n -> Vec X n -> X
vlookup fz     (vcons x xs) = x
vlookup (fs i) (vcons x xs) = vlookup i xs

развивается просто отлично. Решение уравнения, которое происходит по пути, - это то же самое решение уравнений, которое Агда делает на метауровне при проверке определения путем сопоставления с образцом или что Haskell делает. Не обманывайте себя такими программами, как

f :: a ~ b => a -> b
f x = x

В ядре Haskell, который разрабатывает какой-то

f {q} x = coerce q x

но это не в твоем лице. И это не в скомпилированном коде. Доказательства равенства OTT, такие как доказательства равенства Хаскеля, можно стереть перед вычислением с замкнутыми членами.

Отступление. Чтобы быть понятным о статусе данных равенства в Haskell, GADT

data Eq :: k -> k -> * where
  Refl :: Eq x x

действительно дает вам

Refl :: x ~ y -> Eq x y

но поскольку система типов не является логически звуковой, тип безопасности зависит от строгого соответствия шаблонов в этом типе: вы не можете стереть Refl, и вы действительно должны вычислить его и сопоставить его во время выполнения, но вы можете стереть данные, соответствующие доказательству x~y. В OTT весь пропозициональный фрагмент является доказательством, не имеющим отношения к открытым терминам и стираемым для закрытых вычислений. Конец отступления.

Разрешимость равенства по тому или иному типу данных не имеет особого значения (по крайней мере, если у вас есть уникальность доказательств идентичности, если у вас не всегда есть UIP, разрешимость - это один из способов получить его иногда). Эквациональные проблемы, возникающие при сопоставлении шаблонов, относятся к произвольным открытым выражениям. Это много веревки. Но машина, безусловно, может решить фрагмент, состоящий из выражений первого порядка, построенных из переменных и полностью применяемых конструкторов (и того, что делает Agda при раздельном случае: если ограничения слишком странные, вещь просто barfs). OTT должен позволить нам немного продвинуться в разрешимые фрагменты унификации высшего порядка. Если вы знаете (forall x. f x = t[x]) для неизвестного f, что эквивалентно f = \ x -> t[x].

Таким образом, "отсутствие сопоставления шаблонов в OTT" всегда было преднамеренным выбором дизайна, поскольку мы всегда намеревались стать целью разработки для перевода, который мы уже знали, как это сделать. Скорее, это строгое обновление в теории ядра.