Also: was ist der Sinn?

Question

Welchen Zweck hat der Typ So? Transliteration in Agda:

data So : Bool → Set where 
    oh : So true 

So hebt eine Boolesche Aussage auf eine logische Eins auf. Oury und Swierstras Einführungspapier The Power of Pi gibt ein Beispiel für eine relationale Algebra, die durch die Spalten der Tabellen indiziert wird. Das Produkt aus zwei Tabellen erfordert, dass sie unterschiedliche Spalten haben, für die sie So verwenden:

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

ich zu konstruieren Beweise Bedingungen für die Dinge gewöhnt bin ich über meine Programme beweisen will. Es scheint natürlich, eine logische Beziehung auf Schema s zu konstruieren Zusammenhanglosigkeit zu gewährleisten:

Disjoint : Rel Schema _ 
Disjoint s s' = All (λ x -> x ∉ cols s) (cols s') 
    where cols = map proj₁ 

So gravierende Nachteile im Vergleich zu einem „richtigen“ proof-Begriff zu haben scheint: Muster auf oh Anpassung nicht gibt Sie keine Informationen mit dem Sie einen anderen Begriff Typ-Check (Does it?) machen könnte - was würde bedeuten, So Werte können nicht sinnvoll in interaktive Prüfung teilnehmen. Vergleichen Sie dies mit der rechnerischen Nützlichkeit von Disjoint, die als eine Liste von Beweisen dargestellt wird, dass jede Spalte in s' nicht in s erscheint.

Ich glaube nicht wirklich, dass die Spezifikation So (disjoint s s') einfacher ist als Disjoint s s' zu schreiben - Sie können die Booleschen disjoint Funktion ohne Hilfe von der Typprüfung definieren - und in jedem Fall bezahlt Disjoint für sich selbst, wenn Sie bearbeiten möchten die darin enthaltenen Beweise.

Ich bin auch skeptisch, dass So Aufwand spart, wenn Sie eine Product konstruieren. Um einen Wert von So (disjoint s s') zu erhalten, müssen Sie immer noch genug Mustervergleich auf s und s' machen, um den Typüberprüfer zu erfüllen, dass sie tatsächlich disjunkt sind. Es scheint eine Verschwendung zu sein, die so erzeugten Beweise zu verwerfen.

So scheint sowohl für Autoren als auch Benutzer von Code, in dem es bereitgestellt wird, unhandlich. 'Also', unter welchen Umständen möchte ich So verwenden?

Answer 1

Wenn Sie bereits einen b : Bool haben, können Sie ihn in einen Vorschlag verwandeln: So b, was ein bisschen kürzer ist als b ≡ true. Manchmal (ich erinnere mich an keinen konkreten Fall) muss man sich nicht mit einem geeigneten Datentyp beschäftigen, und diese schnelle Lösung ist genug.

So scheint zu einem „richtigen“ Beweis Zeit gravierende Nachteile im Vergleich zu haben: Muster auf oh passender nicht Sie geben keine Informationen , mit dem Sie einen anderen Begriff Typ-Check machen könnte. Als Konsequenz können So Werte nicht sinnvoll an interaktiven Tests teilnehmen. Vergleichen Sie dies mit der Rechenleistung von Disjoint, die ist als eine Liste von Beweisen dargestellt, dass jede Spalte in s' nicht in s erscheint.

So tut Ihnen die gleichen Informationen wie Disjoint geben - Sie brauchen nur zu extrahieren.Wenn zwischen disjoint und Disjoint keine Inkonsistenz besteht, sollten Sie in der Lage sein, eine Funktion So (disjoint s) -> Disjoint s zu schreiben, die Mustererkennung, Rekursion und die Eliminierung unmöglicher Fälle verwendet.

Wenn Sie jedoch die Definition ein wenig zwicken:

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

So wird ein wirklich nützlicher Datentyp, da x : So true sofort tt aufgrund der für ⊤ eta-Regel reduziert. Dies ermöglicht So wie eine Einschränkung zu verwenden: in pseudo-Haskell wir

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

schreiben könnte und wenn n in kanonischer Form (das heißt suc (suc (suc ... zero))), dann n <=? 3 kann durch den Compiler und keine Beweise nötig sind, um überprüft werden. In der tatsächlichen Agda ist es

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

ich diesen Trick in this Antwort (es ist {_ : False (m ≟ 0)} dort). Und ich denke, es wäre unmöglich, eine brauchbare Version der Maschine zu schreiben decribed here ohne diese einfache Definition:

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

wo T ist So in der Standardbibliothek Agda.

Auch in Gegenwart von Beispiel Argumenten So -as-a-Daten-Typ kann als So -as-a-Einschränkung verwendet werden:

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