それでは、何がポイントですか？

Question

Soタイプの目的は何ですか？ Agdaに翻字：

data So : Bool → Set where 
    oh : So true 

Soは論理1までのブール提案を持ち上げます。 OuryとSwierstraの入門書The Power of Piは、テーブルの列によってインデックス付けされた関係代数の例を示しています。私は私が私のプログラムについて証明したいもののために証拠の用語を構築するために使用しています

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') 

：二つのテーブルの積を取ることは、彼らはSoを使用しているために異なる列を、持っていることが必要です。 disjointednessを確保するために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が努力を節約するとも懐疑的です。 So (disjoint s s')という値を与えるためには、実際には別の型チェッカーを満足させるには、まだ十分なパターンマッチングをsとs'で行う必要があります。このように生成された証拠を捨てるのは無駄だと思われる。

Soは、配備されたコードの作成者とユーザーの両方にとって扱いにくいようです。 「だから」、どのような状況でSoを使いたいですか？

Answer 1

すでにb : Boolがある場合は、​​という提案に変更することができます。これはb ≡ trueより少し短いです。時には（私は実際の事例を覚えていません）適切なデータタイプを気にする必要はなく、この迅速な解決策で十分です。

So「適切な」 証明期に比べて重大な欠点を持っているようだ：ohにパターンマッチングは、あなたが別の用語の型チェックを行う可能性があるとのあらゆる情報 を与えるものではありません。結果として、 So値は対話型証明に有効に参加できません。 Disjointの計算上の有用性と対照的に、これはs'の各列がsに現れていないという証明のリストとして表されている です。

は、Disjointと同じ情報を提供します。あなたはそれを抽出する必要があります。基本的に、disjointとDisjointの間に矛盾がなければ、So (disjoint s) -> Disjoint sファンクションはパターンマッチング、再帰および不可能なケース消去を使用して記述することができます。

あなたが定義を微調整する場合は、ビット：x : So trueは、直ちに原因⊤ためイータルールにttに減少するので

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

Soは、本当に便利なデータタイプになります。擬似Haskellで私たちは

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

を書くことができそしてnは正規形（すなわちsuc (suc (suc ... zero))）である場合、その後、n <=? 3は、コンパイラによって確認することができ、何の証拠が必要とされていない：これは、制約のようなSoを使用することができます。実際のAgdaでは、それは私が（それが{_ : False (m ≟ 0)}ある）thisの回答でこのトリックを使用し

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

です。そして、私は機械の使用可能なバージョンを書くことは不可能であろうと思う。この単純な定義なしにhereをdecribed：TはAgdaの標準ライブラリでSoある

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

。

また、So -as-データ型So -as-制約として使用することができるインスタンスの引数の存在下で：

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