В конце раздела "5. Полный OTT"На пути к теории наблюдений авторы показывают, как определять индексируемые типы данных coercible-under-constructors в 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

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

Решение, конечно, заключается в том, чтобы делать то, что делали люди из ГАДТ, и четко определять индуктивные семьи вплоть до пропозиционального равенства. И тогда, конечно, вы можете транспортировать их транзитивностью.

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

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

В теории типов это не работает, так как недостаточно иметь доказательствоa ~ b по объему, чтобы иметь возможность переписать с помощью этого уравнения: это доказательство также должно бытьreflпотому что в присутствии ложной гипотезы проверка типа становится неразрешимой из-за проблем с завершением (что-то вродеэтот). Так что, когда вы образец соответствия наFin m в Хаскеле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? Если это действительно проблема, есть ли способы ее смягчить?