[Agda] Two best practice questions

[Edsko de Vries]

Hi,

I have two questions about best practice in Agda. The Agda tutorial
spends some time on the use of views; here is one example (from
another tutorial, on Epigram in fact):

data EqOrNot : Bool -> Bool -> Set where
  same : {b : Bool} -> EqOrNot b b
  diff : {b : Bool} -> EqOrNot b (not b)

eqOrNot : (a b : Bool) -> EqOrNot a b
eqOrNot true  true  = same
eqOrNot true  false = diff
eqOrNot false true  = diff
eqOrNot false false = same

Such a view allows us to define a function such as xor easily:

xor : (x y : Bool) -> Bool
xor x y with eqOrNot x y
xor x .x       | same = false
xor x .(not x) | diff = true

However, why is it useful to define a custom datatype for such a view?
We could just as easily define:

eqOrNot' : (a b : Bool) -> a ≡ b ⊎ b ≡ not a
eqOrNot' true  true  = inj₁ refl
eqOrNot' true  false = inj₂ refl
eqOrNot' false true  = inj₂ refl
eqOrNot' false false = inj₁ refl

without using a special datatype, and we can still define xor just as
easily too:

xor' : (x y : Bool) -> Bool
xor' x y with eqOrNot' x y
xor' x .x       | inj₁ refl = false
xor' x .(not x) | inj₂ refl = true

What is the advantage of the first approach over the second? (From a
pure readability perspective, to understand the type of eqOrNot we
need to know the constructors of EqOrNot, whereas we can understand
the type of eqOrNot' directly.)

In a related question (one that motivates the first, in fact),
consider the definition of a type that describes when an assertion is
satisfied:

_⊨_ : State -> Assn -> Set
σ ⊨ true        = ⊤
σ ⊨ false       = ⊥
σ ⊨ (! P)       = (σ I ⊨ P) -> ⊥
-- and more clauses.. --

It seems that it would be more in line with Agda practice to define
this as a datatype instead:

data _⊨_ : State -> Assn -> Set where
  sat-true : {σ : State} -> σ ⊨ true
  -- no constructor for σ ⊨ false
  sat-not : {σ : State} -> {P : Assn} -> ((σ ⊨ P) -> ⊥) -> σ ⊨ (! P)
  -- and more constructors.. --

but this datatype definition is rejected, since there is a negative
occurrence in the definition for ! P -- even though this datatype is
clearly well-founded (defined by induction on the assertion). If there
are good reasons, above, to choose eqOrNot (using a special datatype)
over eqOrNot', then is a definition for ⊨ as a function instead of a
datatype going to get me into trouble later?

Thanks,

Edsko