[Haskell-cafe] bottom case in proof by induction

Martijn van Steenbergen martijn at van.steenbergen.nl
Wed Dec 31 20:16:39 EST 2008


Luke Palmer wrote:
> First, by simple definition, id _|_ = _|_.  Now let's consider foo _|_.  
> The Haskell semantics say that pattern matching on _|_ yields _|_, so 
> foo _|_ = _|_. So they are equivalent on _|_ also.  Thus foo and id are 
> exactly the same function.

Would it in general also be interesting to look at foo == id for input 
(_|_:xs) and all other possible positions and combinations of positions 
for bottom? I wonder how many cases you need to take into consideration 
to have covered every possible situation.

Martijn.


More information about the Haskell-Cafe mailing list