[Haskell-cafe] bottom case in proof by induction

Derek Elkins derek.a.elkins at gmail.com
Wed Dec 31 20:39:30 EST 2008

On Thu, 2009-01-01 at 02:16 +0100, Martijn van Steenbergen wrote:
> 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.

That case is already covered by the (x:xs) case.  The interesting,
potentially "extra", case is an infinite list.

More information about the Haskell-Cafe mailing list