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

[Alan Jeffrey]

Adding:

   baz : Bool → String
   baz true = "true"
   baz false = "false"

   main = run (putStrLn (baz (foo 1 true)))

to your file and compiling with "agda -c" shows that MAlonzo agrees with 
your intuition.  The code generated by MAlonzo is essentially the direct 
translation of Agda pattern matching into Haskell pattern matching.

This looks like a bug to me.  (Personally I think the compiler is right 
and the interpreter is wrong, but there may be subtleties I'm not aware of.)

A.

On 06/16/2011 09:01 AM, Wojciech Jedynak wrote:
> 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