所以：有什麼意義？

Question

So類型的預期用途是什麼？音譯成阿格達：

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個邏輯關係，以確保脫節：

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，你可以把它變成主張：​​，這比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可以被編譯器檢查，不需要證明。在實際阿格達是

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

我this答案（這是{_ : False (m ≟ 0)}有）使用這一招。我想這是不可能寫出機器的可用版本的描述下here沒有這個簡單的定義：

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

其中T是在阿格達的標準庫So。

而且，在實例參數存在So -as-A-數據類型可被用作So -as-A-約束：

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