[Agda] Overlapping patterns in function definition -- strange behavior

[Anthony de Almeida Lopes]

I was thinking about this the other day as well. I can't comment on
Agda but older FP languages (before Haskell) used to take the the most
specific patterns first. So, in your case they could be ordered by
specificity zero, (suc n), n. In that case "n" wouldn't match
anything. I think Hope is the languae I'm thinking of. Haskell on the
other hand uses what's defined first. Anyone want to explain Agda to
us?

- Anthony

2011/6/16 Wojciech Jedynak <wjedynak at gmail.com>:
> Hello everybody!
>
> This post is a literate Agda file. It was tested with Agda 2.2.10.
> I noticed a strange behavior when I defined a function with
> overlapping patterns.
> Please look below.
>
> \begin{code}
>
> module Test where
>
> open import Data.Nat
> open import Data.Bool
> open import Relation.Binary.PropositionalEquality
>
> foo : ℕ → Bool → Bool
> foo zero b = b
> foo n true = true
> foo (suc n) b = false
>
> bar : ℕ → Bool → Bool
> bar zero b = b
> bar (suc n) b = false
>
> fooBarEquiv : ∀ (n : ℕ)(b : Bool) → foo n b ≡ bar n b
> fooBarEquiv zero b = refl
> fooBarEquiv (suc n) b = refl
>
> \end{code}
> I was very surprised that it's possible to prove fooBarEquiv.
>
> The difference between foo and bar is that foo has an extra clause in
> the middle.
> According to my intuition, foo 1 true should reduce to true, but when
> I check it with
> C-c C-n I get false. At least it's consistent.
>
> Porting this code to Haskell:
>
> data Nat = Zero | Suc Nat deriving Show
>
> foo :: Nat -> Bool -> Bool
> foo Zero b = b
> foo n True = True
> foo (Suc n) b = False
>
> We get:
>
> ghci> foo (Suc Zero) True
> True
>
> I run into this issue, because I wanted to define two (extensionally)
> equivalent
> functions, with one being an optimized version of the other, and the
> optimization
> was to yield result in a particular, concrete case without doing matching one of
> the arguments at all. When I was working on the proof that the
> equivalence indeed
> holds, I saw that Agda didn't care for the "missing" pattern. So please tell me,
> is it a bug or a feature?
>
> On a similar topic: when patterns are compiled, is the order preserved?
>
> These questions may sound silly, but I have this one function that I really want
> to actually run, not only type-check :-) And the unoptimized version
> needs around
> 70 minutes to evaluate :-) [It's much better when I compile it with MAlonzo, but
> at some point I will want to write a theorem
> lem-certified-result : my-function 0 ≡ result
> lem-certified-result = refl
> ]
>
> Greetings,
> Wojciech Jedynak
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>