[Haskell-cafe] bottom case in proof by induction
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