Формулирование системы зависимых типов в Агде - PullRequest
Новая
       78

Формулирование системы зависимых типов в Агде

0 голосов
/ 27 февраля 2019

Как можно сформулировать логику с зависимой типизацией в Agda, но не «обманывать», повторно используя саму систему типов Агды?

Я вполне могу определить логику с независимой типизацией: 

infixr 5 _⇒_
data Type : Set where
    _⇒_ : Type → Type → Type

infix 4 _⊢_
data _⊢_ : List Type → Type → Set where
    var : {a : Type} → [ a ] ⊢ a
    λ'  : {a b : Type} {γ : _} → a ∷ γ ⊢ b → γ ⊢ a ⇒ b
    ply : {a b : Type} {γ δ : _} → γ ⊢ a ⇒ b → δ ⊢ a → γ ++ δ ⊢ b
    weak : {a b : Type} {γ : _} → γ ⊢ b → a ∷ γ ⊢ b
    cntr : {a b : Type} {γ : _} → a ∷ a ∷ γ ⊢ b → a ∷ γ ⊢ b
    xchg : {a : Type} {γ δ : _} → γ ↭ δ → γ ⊢ a → δ ⊢ a

Я также могу приблизительно следовать учебной реализации LambdaPi для λ-исчисления с зависимой типизацией в Haskell.Но он имплицитно-типизирован, в отличие от моего кода Agda, и я не уверен, где даже начинать изменять мой код, так как путь, который пришел на ум, привел к бесконечному регрессу: 

data _⊢_ : List (? ⊢ ?) → (? ⊢ ?) → Set where ...

Googleвыполняет поиск «встраивания зависимых типов в Agda» и т. п. просто возвращает совпадения для зависимо-типизированного программирования в Agda ...

1 Ответ

0 голосов
/ 27 февраля 2019

Мы сделали это в нашей статье о теории типов в теории типов, которая фактически формализована в Агде.Основная идея заключается в том, что вы определяете контексты, типы, термины и замены как взаимное индуктивное определение.Мы определяем только типизированные объекты, поэтому нам никогда не придется определять нетипизированные объекты или суждения о типизации.Типизация определяется через зависимость, поэтому, например, типы зависят от контекстов, а термины от типов и контекстов.Для формулировки определения равенства мы используем идеи из теории гомотопического типа и допускаем конструкторы равенства.Это означало, что мы должны были аксиоматизировать случаи более высоких индуктивных типов или быть точными частными индуктивными типами.Это должно быть скоро возможно из коробки в кубической Агде.

http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf

@article{altenkirch2016type,
  title={Type theory in type theory using quotient inductive types},
  author={Altenkirch, Thorsten and Kaposi, Ambrus},
  journal={ACM SIGPLAN Notices},
  volume={51},
  number={1},
  pages={18--29},
  year={2016},
  publisher={ACM}
}
...