[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[Will Sonnex]

> However:
>> You can express a property such as "takeWhile p xs ++ dropWhile p xs
>> === xs" and it will prove it to be true for all values of p :: a ->
>> Bool and xs :: [a], over all types a, using only the function
>> definitions.
>
> That is surprising, given that this property does not seem to be true
> for p = const undefined and xs /= [].
>
>   Tillmann
>

This is a very interesting observation. When Zeno does
induction/case-splitting it does not consider the value _|_ as a
potential inhabitant of a type. This could be a feature I might add in
a later version or some option for being able to turn this behaviour
on/off but thanks for spotting it.

Infinite values (lazy-evaluation in general) also give Zeno a problem,
since you can no longer use structure as a well-defined ordering for
induction. A property such as "reverse (reverse xs) === xs" does not
work for infinite lists, since you can successfully case-analyse
values from "xs" but case-analysing "reverse (reverse xs)" will give
an infinite loop. You could say the values are equal in some sense
(maybe given infinite computation time) but they do not behave in the
same way.


Cheers,

Will