Почему более новые языки с независимой типизацией не приняли подход SSReflect?

Question

Есть два соглашения, которые я нашел в расширении SSReflect Coq, которые кажутся особенно полезными, но которые я не видел широко принятыми в новых языках с зависимой типизацией (Lean, Agda, Idris).

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

Во-вторых, типы данных с инвариантами определяются как зависимые записи, содержащие простой тип данных плюс доказательство инварианта. Например, последовательности с фиксированной длиной определены в SSReflect как:

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

seq и доказательство того, что длина этой последовательности является определенным значением. Это противоположно тому, как, например, Идрис определяет этот тип:

data Vect : (len : Nat) -> (elem : Type) -> Type 

Типизированная структура данных с зависимым типом, в которой инвариант является частью своего типа. Одним из преимуществ подхода SSReflect является то, что он позволяет использовать повторно, так что, например, многие функции, определенные для seq и доказательства о них все еще могут быть использованы с tuple (работая на основе seq), тогда как с подходом Идриса такие функции, как reverse, append и тому подобное нужно переписать для Vect, У Lean фактически есть эквивалент стиля SSReflect в его стандартной библиотеке, vector, но он также имеет стиль Идрис array который, кажется, имеет оптимизированную реализацию во время выполнения.

Одна книга, ориентированная на SSReflect, даже претендует на Vect n A Стиль подхода антипаттерн:

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

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

Answer 1

Я могу высказать некоторые соображения по первому пункту (определяя предикаты как функции, возвращающие логические значения). Моя самая большая проблема с этим подходом заключается в том, что функция по определению не может иметь ошибок, даже если оказывается, что она рассчитывает не то, что вы намеревались рассчитать. Во многих случаях будет также затруднено понимание того, что вы на самом деле имеете в виду под предикатом, если вам нужно будет включить в его определение детали реализации процедуры принятия решения для предиката.

В математических приложениях также будут проблемы, если вы захотите определить предикат, который является специализацией чего-то, что вообще не поддается разрешению, даже если это случается в вашем конкретном случае. Одним из примеров того, о чем я говорю здесь, было бы определение группы с заданным представлением: в Coq распространенным способом определения этого является setoid с базовым множеством, являющимся формальными выражениями в генераторах, и равенством, данным как "word эквивалентность". В общем, это отношение не является разрешимым, хотя во многих конкретных случаях это так. Однако, если вы ограничены определением групп с презентациями, где проблема слова разрешима, то вы теряете способность определять объединяющую концепцию, которая связывает все различные примеры вместе, и в общих чертах доказывать вещи о конечных презентациях или о конечно представленных группах. С другой стороны, определение отношения эквивалентности слов как абстрактного Prop или эквивалент прост (если возможно, немного долго).

Лично я предпочитаю сначала дать максимально прозрачное определение предиката, а затем по возможности предоставить процедуры принятия решения (функции, возвращающие значения типа {P} + {~P} мое предпочтение здесь, хотя функции с логическим возвратом тоже будут работать хорошо). Механизм классов типов Coq может обеспечить удобный способ регистрации таких процедур принятия решений; например:

Class Decision (P : Prop) : Set :=
decide : {P} + {~P}.
Arguments decide P [Decision].

Instance True_dec : Decision True := left _ I.
Instance and_dec (P Q : Prop) `{Decision P} `{Decision Q} :
  Decision (P /\ Q) := ...

(* Recap standard library definition of Forall *)
Inductive Forall {A : Type} (P : A->Prop) : list A -> Prop :=
| Forall_nil : Forall P nil
| Forall_cons : forall h t, P h -> Forall P t -> Forall P (cons h t).
(* Or, if you prefer:
Fixpoint Forall {A : Type} (P : A->Prop) (l : list A) : Prop :=
match l with
| nil => True
| cons h t => P h /\ Forall P t
end. *)

Program Fixpoint Forall_dec {A : Type} (P : A->Prop)
  `{forall x:A, Decision (P x)} (l : list A) :
  Decision (Forall P l) :=
  match l with
  | nil => left _ _
  | cons h t => if decide (P h) then
                  if Forall_dec P t then
                    left _ _
                  else
                    right _ _
                else
                  right _ _
  end.
(* resolve obligations here *)
Existing Instance Forall_dec.

Answer 2

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

Вам не нужно носить с собой большие термины, как описано в тезисе Эдвина Брейди, под названием "принудительная оптимизация". У Agda есть форсирование, которое влияет на проверку типов (особенно важно то, как вычисляются юниверсы), но я не уверен, действительно ли материал, используемый только во время проверки типов, будет удален до времени выполнения. Во всяком случае, Агда имеет два понятия неактуальности: .(eq : p ≡ q) это обычная неуместность (смысл eq не имеет значения во время проверки типа, поэтому он определенно равен любому другому члену такого типа) и ..(x : A) это неуместность позвоночника (не уверен, что это правильный термин. Я думаю, что источники в Агде называют такую ​​вещь "нестрогая нерелевантность"), что буквально означает удаление не относящихся к вычислениям, но не совершенно не относящихся к делу терминов. Таким образом, вы можете определить

data Vec {α} (A : Set α) : ..(n : ℕ) -> Set α where
  [] : Vec A 0
  _∷_ : ∀ ..{n} -> A -> Vec A n -> Vec A (suc n)

а также n будут стерты до времени выполнения. Или, по крайней мере, кажется, что он спроектирован так, что трудно быть уверенным, потому что Agda имеет множество плохо документированных функций.

И вы можете написать эти доказательства с нулевой стоимостью в Coq, просто потому, что он также реализует неактуальность для вещей, которые живут в Prop, Но нерелевантность встроена в теорию Coq очень глубоко, в то время как в Agda это отдельная особенность, поэтому совершенно понятно, почему люди находят использование неактуальности в Coq с большей готовностью, чем в Agda.

Одним из преимуществ подхода SSReflect является то, что он позволяет использовать повторно, так что, например, многие функции, определенные для seq и доказательства о них все еще могут быть использованы с tuple (работая на основе seq), в то время как с подходом Идриса функции, такие как reverse, append и т.п., должны быть переписаны для Vect,

Это не реальное повторное использование, если вам все равно придется доказывать свойства, и эти доказательства имеют ту же сложность, что и функции, определенные для индексированных данных. Кроме того, неудобно выполнять работу механизма объединения, раздавать явные доказательства и применять леммы, чтобы получить length xs ≡ n от suc (length xs) ≡ n (а также sym, trans, subst и все другие леммы, от которых механизм объединения может спасти вас во многих случаях). Более того, вы теряете некоторую ясность, злоупотребляя пропозициональным равенством: xs : List A; length xs ≡ n + m вместо xs : Vec A (n + m) не улучшает читаемость ваших контекстов, особенно если они огромные, что часто имеет место. И есть другая проблема: иногда просто сложнее определить функцию, используя подход SSReflect: вы упомянули reverse за Vect, Я призываю вас определить эту функцию с нуля (с reverse за List в качестве "повторно используемой" части под капотом), а затем сравните свое решение с определением в Data.Vec из стандартной библиотеки Agda. И если у вас не включена неактуальность для предложений по умолчанию (как в случае с Agda), то вам также необходимо доказать свойства доказательств, если вы хотите доказать, скажем, reverse (reverse xs) ≡ xs что много нетривиальных шаблонов.

Так что подход SSReflect не идеален. Другой тоже. Есть что-нибудь, что улучшает оба? Да, Орнаменты (см. Орнаментальные алгебры, Алгебраические орнаменты и Сущность орнаментов). Вы можете легко получить Vec от List применив соответствующую орнаментальную алгебру, но я не могу сказать, сколько кода вы будете использовать повторно, и будут ли типы сводить вас с ума или нет. Я слышал, что люди на самом деле используют украшения где-то.

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

ОБНОВИТЬ

Антон Трунов в своем комментарии заставил меня осознать, что я слишком агдонист, и у людей в Coq есть тактика, которая может значительно упростить доказательства, поэтому доказательство в Coq обычно проще (при условии, что у вас есть такое оружие, как crush из книги CPDT), чем определение функций над данными. Что ж, тогда я предполагаю, что доказательства несоответствия по умолчанию и тяжелая тактика - вот что делает подход SSReflect эффективным в Coq.