[Agda] Two best practice questions

[Andreas Abel]

Hi Edsko,

concerning you first question, I do not see much difference between 
EqOrNot and a ≡ b ⊎ b ≡ not a.  The advantage of the first is that you 
have more telling constructor names (same/diff instead of inj1/2 refl). 
  The advantage of the second is that you can use library functions for 
the disjoint union.  I would say the situation is not much different 
from Haskell or ML where you can choose to roll your own data type or 
compose it from existing ones.

In case of the second question, you do not have much of a choice.  Since 
the data type is negative, you are forced to use the encoding as a 
recursive type-valued function instead.  The fundamental difference is 
that you can do induction over data types but not over types constructed 
by cases and recursion.  Of course, you can still do induction over 
Assn, and I guess this is what you will need anyway.

Cheers,
Andreas

On 12/3/10 4:05 PM, Edsko de Vries wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/