[Agda] Two best practice questions

[Conor McBride]

Hi Edsko

On 3 Dec 2010, at 15:05, 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

There's a specific reason why this choice suits Epigram, and it's
to do with the fact that Epigram does not natively have dependent
pattern matching but rather supports programming with arbitrary
eliminators. Compare the Agda

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

with the Epigram-style

xor : (x y : Bool) -> Bool
xor x y <= view eqOrNot x y
   xor x x        = false
   xor x (not x)  = true

The datatype expresses exactly the intended mode of pattern
analysis. McKinna's point (for it is his, not mine) is that
datatype definition is the ideal (initial!) mechanism for
specifying a mode of pattern matching and recursion. Epigram
was set up to support that way of working.

The same analysis is clearly derivable from sums and equality,
but you have to work a little harder and be rather more explicit
to invoke it. One pays for exploiting compositionality in the
types by loss of abstraction in one's patterns. (Standard FP
blindspot: abstraction is popular in expressions, but strangely
never missed in patterns, except by weirdos like me.)

> However, why is it useful to define a custom datatype for such a view?

On the one hand, I'd say whyever not? Introducing a "custom
datatype" which neatly suits a specific purpose is a good
thing to do, unless you lose modularity by doing so. Of course,
it's possible that here, one might. The general picture for
concrete types is that two terms are either equal or have, say,
a leftmost discrepancy.

On the other hand, I'd say that custom datatypes should be
abolished altogether and reintroduced by reflection. That's to
say, one should be able to combine calculability with the fact
that one's datatype is constructed to capture a mode of
pattern matching and recursion.

> 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

What should its induction principle be?

> well-founded (defined by induction on the assertion).

Right, so induction on the assertion is the explanation of why
the structure is meaningful. One could, of course, use a datatype
to define a case analysis principle for derivations of sigma |- P
which packaged up the business of matchinng on P then killing the
false case, and whatever other rearrangement you typically do.

As for best practice in Agda, I don't know. Hardwiring pattern
matching as primitive does rather change one's options. There are
times, when I'm trying to express a subtle case analysis neatly,
or a recursion that's too weird for the hardwired oracle, that I
really miss Epigram's <= construct and the corresponding freedom
to explain myself.

All the best

Conor