Могу ли я использовать индуктивные семейства в Cubical Agda? - PullRequest
Новая
       48

Могу ли я использовать индуктивные семейства в Cubical Agda?

2 голосов
/ 28 января 2020

Я заметил, что стандартная кубическая библиотека определяет Fin как зависимую пару вместо индексированного индуктивного типа. Причина в том, что Cubical Agda не полностью поддерживает индексируемые индуктивные типы: https://github.com/agda/cubical/pull/104#discussion_r268476220

Связанная проблема утверждает, что сопоставление с образцом не работает на индуктивных семействах, поскольку hcomp и transp не было определено для них: https://github.com/agda/cubical/pull/57#issuecomment -461174095

Я определил Fin и Vec и написал функцию сопоставления с образцом, и, похоже, она работает нормально : 

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat using (ℕ; zero; suc)

private
  variable
    ℓ : Level
    A : Type ℓ
    n : ℕ

data Fin : ℕ → Type₀ where
  fzero : Fin (suc n)
  fsuc : Fin n → Fin (suc n)

data Vec (A : Type ℓ) : ℕ → Type ℓ where
  [] : Vec A zero
  _∷_ : A → Vec A n → Vec A (suc n)

_[_] : Vec A n → Fin n → A
(x ∷ _) [ fzero ] = x
(_ ∷ xs) [ fsuc n ] = xs [ n ]

p : (1 ∷ (2 ∷ [])) [ fzero ] ≡ 1
p = refl

Тем не менее, этот вопрос все еще открыт: https://github.com/agda/agda/issues/3733

Я хочу использовать Cubical Agda на тот случай, если мне понадобятся более высокие индуктивные типы или расширенные функции, но я не хочу отказываться от Vec или индексированного определения Fin. Я не знаком с деталями кубической теории типов, поэтому не знаю, где будут вызываться hcomp и transp. Каково текущее состояние индуктивных семей в Кубической Агде? Могу ли я использовать их, если избегаю определенных операций?

1 Ответ

3 голосов
/ 29 января 2020

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

Ограничение, которое будет устранено https://github.com/agda/agda/issues/3733 является следующим:

Термин типа subst Fin refl fzero не будет вычисляться для fzero или любого другого конструктора, что также означает, что 

(x ∷ _) [ subst Fin refl fzero ]

не будет вычисляться на x.

Мы все еще можем доказать subst Fin refl fzero ≡ fzero на substRefl из библиотеки, поэтому мы можем также доказать (x ∷ _) [ subst Fin refl fzero ] ≡ x.

Так что в настоящее время это выбор между использованием индуктивные семейства и работа с subst и transport застреванием на них, или иным образом кодирование всего с путями и потеря правильного сопоставления с образцом.

...