Итак: какой смысл?

Какова цель назначения 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?

Ответы

Ответ 1

Если у вас уже есть b : Bool, вы можете включить его в предложение: So b, что немного короче, чем b ≡ true. Иногда (я не помню никакого реального случая) нет необходимости беспокоиться о правильном типе данных, и этого быстрого решения достаточно.

So, по-видимому, имеет серьезные недостатки по сравнению с "правильным" term-term: соответствие шаблонов на oh не дает вам никакой информации с помощью которого вы можете сделать еще один тип проверки типа. В качестве следствия, Значения So не могут с пользой участвовать в интерактивной проверке. Сравните это с вычислительной полезностью Disjoint, которая представляется в виде списка доказательств того, что каждый столбец в s' не появляются в s.

So дает вам ту же информацию, что и Disjoint - вам просто нужно извлечь ее. В принципе, если между Disjoint и Disjoint нет несогласованности, тогда вы должны иметь возможность написать функцию So (disjoint s) -> Disjoint s с помощью устранения совпадения шаблонов, рекурсии и невозможности исключения.

Однако, если вы немного измените определение:

So : Bool -> Set
So true  = ⊤
So false = ⊥

So становится действительно полезным типом данных, потому что x : So true сразу сводится к tt из-за eta-правила для ⊤. Это позволяет использовать So как ограничение: в псевдо-Haskell мы могли бы написать

forall n. (n <=? 3) => Vec A n

и если n находится в канонической форме (т.е. suc (suc (suc ... zero))), то n <=? 3 может быть проверен компилятором и никаких доказательств не требуется. В действительности Агда это

∀ {n} {_ : n <=? 3} -> Vec A n

Я использовал этот трюк в ответе this (там {_ : False (m ≟ 0)}). И я думаю, что без этого простого определения невозможно было бы написать полезную версию машины :

Is-just : ∀ {α} {A : Set α} -> Maybe A -> Set
Is-just = T ∘ isJust

где T - So в стандартной библиотеке Agda.

Кроме того, при наличии аргументов экземпляра So -as-a-data-type может использоваться как So -as-a-constraint:

open import Data.Bool.Base
open import Data.Nat.Base
open import Data.Vec

data So : Bool -> Set where
  oh : So true

instance
  oh-instance : So true
  oh-instance = oh

_<=_ : ℕ -> ℕ -> Bool
0     <= m     = true
suc n <= 0     = false
suc n <= suc m = n <= m

vec : ∀ {n} {{_ : So (n <= 3)}} -> Vec ℕ n
vec = replicate 0

ok : Vec ℕ 2
ok = vec

fail : Vec ℕ 4
fail = vec