Какова цель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')

Я привык строить термины доказательств того, что я хочу доказать в своих программах. Кажется более естественным построить логическое соотношениеSchemas для обеспечения разобщенности:

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?