Какова цель назначения So
типа? Транслитерация в Агда:
data So : Bool → Set where
oh : So true
So
поднимает логическое предложение до логического. Oury и Swierstra Сила Pi дает пример реляционной алгебры, индексированной столбцами таблиц. Для получения двух таблиц требуется, чтобы они имели разные столбцы, для которых они используют So
:
Schema = List (String × U) -- U is the universe of SQL types
-- false iff the schemas share any column names
disjoint : Schema -> Schema -> Bool
disjoint = ...
data RA : Schema → Set where
-- ...
Product : ∀ {s s'} → {So (disjoint s s')} → RA s → RA s' → RA (append s s')
Я использую построение доказательств для вещей, которые я хочу доказать о своих программах. Кажется более естественным построить логическое соотношение на Schema
для обеспечения несвязности:
Disjoint : Rel Schema _
Disjoint s s' = All (λ x -> x ∉ cols s) (cols s')
where cols = map proj₁
So
, по-видимому, имеет серьезные недостатки по сравнению с "правильным" доказательством: соответствие шаблонов на oh
не дает вам никакой информации, с помощью которой вы могли бы сделать еще одну проверку типа термина (это так?) - что означает, что значения So
не могут с пользой участвовать в интерактивной проверке. Сравните это с вычислительной полезностью Disjoint
, которая представлена в виде списка доказательств того, что каждый столбец в s'
не отображается в s
.
Я действительно не верю, что спецификация So (disjoint s s')
проще писать, чем Disjoint s s'
- вам нужно определить функцию Boolean Disjoint
без помощи проверки типа - и в любом случае Disjoint
платит для себя, когда вы хотите манипулировать доказательствами, содержащимися в нем.
Я также скептически отношусь к тому, что So
экономит усилия, когда вы создаете Product
. Чтобы дать значение So (disjoint s s')
, вам все равно нужно выполнить достаточное сопоставление шаблонов на s
и s'
, чтобы убедиться, что они действительно не пересекаются. Кажется, что отходы отбрасывают полученные таким образом доказательства.
So
кажется громоздким как для авторов, так и для пользователей кода, в котором он был развернут. "Итак", при каких обстоятельствах я бы хотел использовать So
?