[Haskell-cafe] Signature for non-empty filter

[Wolfgang Jeltsch]

Am Mittwoch, 6. Februar 2008 18:39 schrieb Bulat Ziganshin:
> […]

> this means that answer to original question - one can ensure that
> argument for filter is non-terminating function only if these
> functions are written using some special notation which doesn't allow
> to write arbitrary turing-complete algorithms

And this is exactly what Agda, Epigram, Coq, etc. do.  Note however that those 
systems are not very restrictive.  It’s possible, for example, to define 
Ackermann’s function in Agda:

> module Ackermann where
>
>     data Nat : Set where
>
>         O  : Nat
>
>         ↑_ : Nat -> Nat
>
>     ackermann : Nat -> Nat -> Nat
>     ackermann O    m    = ↑ m
>     ackermann (↑ n) O    = ackermann n (↑ O)
>     ackermann (↑ n) (↑ m) = ackermann n (ackermann (↑ n) m)

Best wishes,
Wolfgang