Итак: в чем смысл?

Question

Какова цель назначения типа So? Транслитерации в Agda:

data So : Bool → Set where 
    oh : So true 

So поднимает логическое суждение до логической единицы. В вводной статье Oury и Swierstra The Power of 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 с для обеспечения disjointedness:

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?

Answer 1

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

So, кажется, имеет серьезные недостатки по сравнению с «правильным» корректора термином: сопоставление с образцом на 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 вследствие ЭТА-правила для ⊤. Это позволяет использовать So как ограничение: в псевдо-Haskell можно написать

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

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

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

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

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

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

Кроме того, при наличии аргументов экземпляра So их а-тип данных может быть использован в качестве So -В-а-ограничения:

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