Итак: какой смысл?
Какова цельSo
тип? Транслитерация в Агду:
data So : Bool → Set where
oh : So true
So
поднимает логическое предложение до логического. Вступительная статья Уери и СвиерстрыСила Пи приводит пример реляционной алгебры, проиндексированной по столбцам таблиц. Взятие произведения двух таблиц требует, чтобы у них были разные столбцы, для которых они используют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
s для обеспечения разобщенности:
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'
- вы должны определить логическое значениеdisjoint
функционировать без помощи проверки типов - и в любом случаеDisjoint
окупается, когда вы хотите манипулировать содержащимися в нем доказательствами.
Я также скептически отношусь к тому, чтоSo
экономит усилия при созданииProduct
, Для того, чтобы дать значениеSo (disjoint s s')
, вы все равно должны сделать достаточно сопоставления с образцом наs
а такжеs'
чтобы удовлетворить проверки типа, что они на самом деле не пересекаются. Это кажется пустой тратой на то, чтобы отбросить полученные таким образом доказательства.
So
кажется неудобным как для авторов, так и для пользователей кода, в котором он развернут. «Итак», при каких обстоятельствах я бы хотел использоватьSo
?