Also, was ist der Punkt
Was ist der Verwendungszweck desSo
Art? Transkription in Agda:
data So : Bool → Set where
oh : So true
So
hebt einen Booleschen Satz auf einen logischen hoch. Einführungsbeitrag von Oury und Swierstra Die Kraft von Pi gibt ein Beispiel für eine relationale Algebra, die durch die Spalten der Tabellen indiziert wird. Um das Produkt von zwei Tabellen zu erhalten, müssen sie unterschiedliche Spalten haben, für die sie @ verwendeSo
:
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 bin es gewohnt, Beweisbegriffe für die Dinge zu konstruieren, die ich über meine Programme beweisen möchte. Es erscheint natürlicher, eine logische Beziehung auf @ zu konstruiereSchema
s um Disjunktheit zu gewährleisten:
Disjoint : Rel Schema _
Disjoint s s' = All (λ x -> x ∉ cols s) (cols s')
where cols = map proj₁
So
scheint gravierende Nachteile gegenüber einem "richtigen" Beweisbegriff zu haben: Pattern Matching aufoh
gibt Ihnen keine Informationen, mit denen Sie eine andere Begriffstypprüfung durchführen könnten (oder?) - was bedeuten würde,So
Werte können nicht sinnvoll an interaktiven Prüfungen teilnehmen. Vergleichen Sie dies mit der rechnerischen Nützlichkeit vonDisjoint
, das als eine Liste von Beweisen dargestellt wird, die jede Spalte in @ enthäs'
erscheint nicht ins
.
Ich glaube nicht wirklich, dass die SpezifikationSo (disjoint s s')
ist einfacher zu schreiben alsDisjoint s s'
- Sie müssen den Booleschen Wert definierendisjoint
Funktion ohne Hilfe der Typprüfung - und auf jeden FallDisjoint
zahlt sich aus, wenn Sie die darin enthaltenen Beweise manipulieren möchten.
Ich bin auch skeptisch, dassSo
spart Mühe beim Erstellen einesProduct
. Um einen Wert von @ zu gebSo (disjoint s s')
, Sie müssen noch genügend Mustervergleiche für @ durchführes
unds'
, um dem Typprüfer zu bestätigen, dass sie tatsächlich disjunkt sind. Es erscheint wie eine Verschwendung, die so erzeugten Beweise zu verwerfen.
So
scheint sowohl für Autoren als auch für Benutzer von Code, in dem es implementiert ist, unhandlich zu sein. 'Also', unter welchen Umständen würde ich @ verwenden wollSo
?