On Wed, Oct 21, 1998 11:30 Uhr, Ch. A. Herrmann
<mailto:[EMAIL PROTECTED]> wrote:
>At the moment, I'm using special comments [Int,{-! 5 !-}], e.g.,
>to tell a preprocessor that a list always has length 5 but I don't
>like to use such methods for the far future.
>
Let's play with this one:
> property ConstantLength n :: Int l :: [a] where
> length l = n
By declaring a variable "x" to have property "ConstantLength 3"
it should be possible by the (definition of length) to infer:
a) x ~= _|_ /\ x ~= []
b) same for (tail x) and (tail tail x)
c) tail tail tail x == []
This would be a plenty of knowledge for the compiler.
Gabor