Data.Numerals

Illustration of the 2-order lambda-calculus, using Church numerals as an example. The example shows limited impredicativity

http://okmij.org/ftp/Haskell/types.html#some-impredicativity

Documentation

newtype N

Constructors

N (forall a. (a -> a) -> a -> a)

zero :: N

succ :: N -> N

one :: N

mul :: N -> N -> N

add :: N -> N -> N

exp :: N -> N -> N

exp2 :: N -> N -> N

f1 :: (forall a. a -> a) -> b -> b

Simpler illustrations of impredicativity

foo :: forall c notimportant. (c -> c) -> notimportant

newtype W

Constructors

W

Fields

unW :: forall a. a -> a

f2 :: W -> b -> b