[Agda] Getting codata right

[Dan Licata]

Hi everyone,

Thanks for the interesting thread!

On Jun08, Anton Setzer wrote:
> Concerning pattern matching I suggest that
> for instance
> 
> f : coNat -> Bool
> f (~ Z) = tt
> f (~ (S n)) = ff
> 
> is an abbreviation for
> 
> f : coNat -> Bool
> f x with x *
> ... | Z' = tt
> ... | (S' n) = ff

This notation is actually a lot like something I implemented in GHC last
summer.  We called it "view patterns"; the idea is that you get to call
a function in the middle of pattern matching and then continue matching
on the result.  What you're writing here specializes the notation to ~,
the "unroll and force evaluation" function for the coalg.

In the above code for 'f', the (with x *) version is in some sense more
honest, because it admits that reaching 'x' is a natural pattern
matching boundary (a polarity shift), and that unrolling-and-forcing the
coalgebra is a different sort of thing.  And the with-version is precise
about where and how many times the forcing happens.

The ~ version is less explicit, and, in terms of the operational
behavior, it can actually be a little subtle to get ~ to do the right
thing, or even to decide what the right thing should be.  For example:

=== Is the coNat forced by f? ===

f : coNat -> Bool
f _ = tt

I.e., do you insert the 'with' if there are no ~ patterns?  I'd hope
not, since you sometimes want to write a function that doesn't force its
argument.

=== How many times is the coNat forced by ... ===

f : (Bool * coNat) -> Integer
f (True , ~ Zero)  = 0
f (False , _ ) = 1
f (True , ~ (Succ Zero))  = 2 

... calling f (False , whatever) ?  
    My GHC impl runs it 0 times.  

... calling f (True , Succ Zero) ?  
    My GHC impl runs it 2 times (the two calls to the view don't get
    coalesced because there is another kind of pattern--in this case a
    wildcard--in between them). But one could hope it would only get run
    once in this case.

I.e., how do you decide which ~ patterns on the same argument to group
into a subsidiary case-analysis of a 'with', like you've done in the
example above?  

Since all you want is ~, and there's no way to pattern-match a colagebra
other than ~, it might be reasonable to insist that a given column is
either all ~'s or no ~'s (precluding examples like this one), in which
case it's clear what to do.

Of course, in a pure language like Agda, these difference won't affect
the behavior of a program.  But they will affect (a) run-time
performance and (b) coverage checking, so a programmer needs to know
exactly how the ~'s get desugared.  

-Dan