What is the intended purpose of the So
type? Transliterating into Agda:
data So : Bool → Set where oh : So true
So
lifts a Boolean proposition up to a logical one. Oury and Swierstra's introductory paper The Power of Pi gives an example of a relational algebra indexed by the tables' columns. Taking the product of two tables requires that they have different columns, for which they use 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')
I'm used to constructing evidence terms for the things I want to prove about my programs. It seems more natural to construct a logical relation on Schema
s to ensure disjointedness:
Disjoint : Rel Schema _ Disjoint s s' = All (λ x -> x ∉ cols s) (cols s') where cols = map proj₁
So
seems to have serious disadvantages compared to a "proper" proof-term: pattern matching on oh
doesn't give you any information with which you could make another term type-check (Does it?) - which would mean So
values can't usefully participate in interactive proving. Contrast this with the computational usefulness of Disjoint
, which is represented as a list of proofs that each column in s'
doesn't appear in s
.
I don't really believe that the specification So (disjoint s s')
is simpler to write than Disjoint s s'
- you have to define the Boolean disjoint
function without help from the type-checker - and in any case Disjoint
pays for itself when you want to manipulate the evidence contained therein.
I am also sceptical that So
saves effort when you're constructing a Product
. In order to give a value of So (disjoint s s')
, you still have to do enough pattern matching on s
and s'
to satisfy the type checker that they are in fact disjoint. It seems like a waste to discard the evidence thus generated.
So
seems unwieldy for both authors and users of code in which it's deployed. 'So', under what circumstances would I want to use So
?
If you already have a b : Bool
, you can turn it into proposition: So b
, which is a bit shorther than b ≡ true
. Sometimes (I don't remember any actual case) there is no need to bother with a proper data type, and this quick solution is enough.
So
seems to have serious disadvantages compared to a "proper" proof-term: pattern matching onoh
doesn't give you any information with which you could make another term type-check. As a corollary,So
values can't usefully participate in interactive proving. Contrast this with the computational usefulness ofDisjoint
, which is represented as a list of proofs that each column ins'
doesn't appear ins
.
So
does give you the same information as Disjoint
— you just need to extract it. Basically, if there is no inconsistency between disjoint
and Disjoint
, then you should be able to write a function So (disjoint s) -> Disjoint s
using pattern matching, recursion and impossible cases elimination.
However, if you tweak the definition a bit:
So : Bool -> Set So true = ⊤ So false = ⊥
So
becomes a really useful data type, because x : So true
immediately reduces to tt
due to the eta-rule for ⊤
. This allows to use So
like a constraint: in pseudo-Haskell we could write
forall n. (n <=? 3) => Vec A n
and if n
is in canonical form (i.e. suc (suc (suc ... zero))
), then n <=? 3
can be checked by the compiler and no proofs are needed. In actual Agda it is
∀ {n} {_ : n <=? 3} -> Vec A n
I used this trick in this answer (it is {_ : False (m ≟ 0)}
there). And I guess it would be impossible to write a usable version of the machinery decribed here without this simple definition:
Is-just : ∀ {α} {A : Set α} -> Maybe A -> Set Is-just = T ∘ isJust
where T
is So
in the Agda's standard library.
Also, in the presence of instance arguments So
-as-a-data-type can be used as So
-as-a-constraint:
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With