On Jun 15, 2006, at 3:59 PM, Conor McBride wrote:
I think the problem is still about pattern coverage. It becomes
clearer that
pattern matching is different from case-spliting, and that is why the
majority function comes into our discussion.
As I have explained, functions such as the majority function
present no more difficulty (ie still none) for coverage checking in
the language with refutations and equations. The only issues with
such functions are pragmatic: firstly whether it's worth putting
effort into supporting their recognition (eg by expansion to case-
splits, as I'm given to believe is to happen in Agda 2)
Indeed. Our approach is to allow arbitrary pattern equations which
are compiled to case-splits before execution. In other words the
majority function will be allowed but it will have the strict
operational behaviour (Conor's alternative 3).
The pattern coverage problem is solved by requiring that the patterns
are decidably covering. That is, if the coverage checker can't see
that a function is total you have to do a better job explaining why
this is the case. To make this convenient we add a special pattern ()
which matches any element of an (obviously) empty type. Once you've
matched on an empty type you are free to omit the right-hand side.
Example:
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data Zero : Set where -- no constructors
Empty : Nat -> Set
Empty zero = Zero
Empty (suc n) = Zero
-- Not accepted, we can't see that Empty n is empty
f : (n:Nat) -> Empty n -> Nat
-- Ok, Empty zero and Empty (suc n) are both clearly empty.
f : (n:Nat) -> Empty n -> Nat
f zero ()
f (suc n) ()
You are allowed to omit clauses if any of the arguments is of empty
type. For instance:
data One : Set where one : One
NonZero : Nat -> Set
NonZero zero = Zero
NonZero (suc n) = One
pred : (n:Nat) -> NonZero n -> Nat
pred (suc n) one = n
Here the coverage checker will discover a missing clause 'pred zero
x', but since the type of x is NonZero zero, which is an empty type,
this is ok.
/ Ulf
