Re: [Haskell-cafe] Signature for non-empty filter

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