So: what's the point?

Question

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 Schemas 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?

score 14 · Accepted Answer · edited Jul 07 '17 at 16:13

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 on oh 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 of Disjoint, which is represented as a list of proofs that each column in s' doesn't appear in s.

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

Also, every proof of "So b" is propositionally equal to any other, which is not necessarily the case for the actual "evidence" of whatever property b is encoding. Sometimes you want that. — Saizan, Oct 22 '15 at 08:35
@Saizan, good point. This property is also exploited at the second link in my answer. Do you have some nice use case in mind? — effectfully, Oct 22 '15 at 09:14
I feel like there's something deeper here about the relationship between types defined inductively with `data` and those defined recursively in functions. Could you elaborate on why Agda is happy to infer a `So` value with your definition but not with mine? — Benjamin Hodgson, Oct 22 '15 at 15:26
@Benjamin Hodgson, that's about differences between `data`s and `record`s: the latter have etas, while the former don't. Any inhabitant of `⊤` is definitionally equal to `tt`: `eq : ∀ {x} -> x ≡ tt; eq = refl`, so when Agda meets `_x : ⊤`, where `_x` is a metavariable, `_x` gets instantiated to `tt`, and the unification problem is solved. But when Agda meets `_x : So true`, she can't unify `_x` with something, because this mechanism doesn't work for `data`. But you can force unification using instance arguments, as witnessed above. — effectfully, Oct 22 '15 at 19:57
@user3237465 I've used something similar here https://github.com/Saizan/miller/blob/master/Injections/Type.agda#L23 so that prop. equality of Inj corresponds to pointwise equality. — Saizan, Oct 23 '15 at 11:39
@Saizan, but inhabitants of `_∉_` are equal propositionally, wouldn't inductive definition give you [the same](http://lpaste.net/143692)? But the `False` part is really a nice use case. — effectfully, Oct 23 '15 at 12:32

So: what's the point?

1 Answers1

Linked